This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⊢ φ ∧ ψ ∨ χ ∧ θ ↔ φ ∨ χ ∧ φ ∧ ψ ∨ χ ∧ θ

Proof

Step Hyp Ref Expression
1 simpl ⊢ φ ∧ ψ → φ
2 simpl ⊢ χ ∧ θ → χ
3 1 2 orim12i ⊢ φ ∧ ψ ∨ χ ∧ θ → φ ∨ χ
4 3 pm4.71ri ⊢ φ ∧ ψ ∨ χ ∧ θ ↔ φ ∨ χ ∧ φ ∧ ψ ∨ χ ∧ θ