Theorem prlem1

A specialized lemma for set theory (to derive the Axiom of Pairing). (Contributed by NM, 18-Oct-1995.) (Proof shortened by Andrew Salmon, 13-May-2011.) (Proof shortened by Wolf Lammen, 5-Jan-2013.)

Hypotheses
prlem1.1
\( \vdash \varphi \rightarrow (\eta \leftrightarrow \chi) \)
prlem1.2
\( \vdash \psi \rightarrow \neg \theta \)
Conclusion
\( \vdash \varphi \rightarrow \psi \rightarrow \psi \wedge \chi \vee \theta \wedge \tau \rightarrow \eta \)
Proof
prlem1.1
biimprd _
l2
adantld _
prlem1.2
pm2.21d _
adantrd _
jaao l2 _
ex _