Theorem prlem2

A specialized lemma for set theory (to derive the Axiom of Pairing). (Contributed by NM, 21-Jun-1993.) (Proof shortened by Andrew Salmon, 13-May-2011.) (Proof shortened by Wolf Lammen, 9-Dec-2012.)

Conclusion
\( \vdash \varphi \wedge \psi \vee \chi \wedge \theta \leftrightarrow (\varphi \vee \chi) \wedge (\varphi \wedge \psi \vee \chi \wedge \theta) \)
Proof
l0
simpl
simpl
orim12i l0 _
pm4.71ri _