Theorem oplem1

A specialized lemma for set theory (ordered pair theorem). (Contributed by NM, 18-Oct-1995.) (Proof shortened by Wolf Lammen, 8-Dec-2012.)

Hypotheses
oplem1.1
\( \vdash \varphi \rightarrow \psi \vee \chi \)
oplem1.2
\( \vdash \varphi \rightarrow \theta \vee \tau \)
oplem1.3
\( \vdash \psi \leftrightarrow \theta \)
oplem1.4
\( \vdash \chi \rightarrow (\theta \leftrightarrow \tau) \)
Conclusion
\( \vdash \varphi \rightarrow \psi \)
Proof
oplem1.3
l1
notbii _
\( \vdash \neg \psi \leftrightarrow \neg \theta \)
oplem1.1
ord _
\( \vdash \varphi \rightarrow \neg \psi \rightarrow \chi \)
l4
biimtrrid l1 _
oplem1.2
ord _
l7
jcad l4 _
\( \vdash \varphi \rightarrow \neg \theta \rightarrow \chi \wedge \tau \)
oplem1.4
biimpar _
\( \vdash \chi \wedge \tau \rightarrow \theta \)
syl6 l7 _
l11
pm2.18d _
\( \vdash \varphi \rightarrow \theta \)
oplem1.3
\( \vdash \psi \leftrightarrow \theta \)
sylibr l11 _