Theorem prlem2

Description: 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)

	Ref	Expression
Assertion	prlem2	$$⊢\left(\left(\phi \wedge \psi \right)\vee \left(\chi \wedge \theta \right)\right)\leftrightarrow \left(\left(\phi \vee \chi \right)\wedge \left(\left(\phi \wedge \psi \right)\vee \left(\chi \wedge \theta \right)\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		simpl	$$⊢\left(\phi \wedge \psi \right)\to \phi$$
2		simpl	$$⊢\left(\chi \wedge \theta \right)\to \chi$$
3	1 2	orim12i	$$⊢\left(\left(\phi \wedge \psi \right)\vee \left(\chi \wedge \theta \right)\right)\to \left(\phi \vee \chi \right)$$
4	3	pm4.71ri	$$⊢\left(\left(\phi \wedge \psi \right)\vee \left(\chi \wedge \theta \right)\right)\leftrightarrow \left(\left(\phi \vee \chi \right)\wedge \left(\left(\phi \wedge \psi \right)\vee \left(\chi \wedge \theta \right)\right)\right)$$