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 φ ψ χ θ φ χ φ ψ χ θ