Theorem oplem1

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

	Ref	Expression
Hypotheses	oplem1.1	$$⊢\phi \to \left(\psi \vee \chi \right)$$
	oplem1.2	$$⊢\phi \to \left(\theta \vee \tau \right)$$
	oplem1.3	$$⊢\psi \leftrightarrow \theta$$
	oplem1.4	$$⊢\chi \to \left(\theta \leftrightarrow \tau \right)$$
Assertion	oplem1	$$⊢\phi \to \psi$$

Proof

Step	Hyp	Ref	Expression
1		oplem1.1	$$⊢\phi \to \left(\psi \vee \chi \right)$$
2		oplem1.2	$$⊢\phi \to \left(\theta \vee \tau \right)$$
3		oplem1.3	$$⊢\psi \leftrightarrow \theta$$
4		oplem1.4	$$⊢\chi \to \left(\theta \leftrightarrow \tau \right)$$
5	3	notbii	$$⊢\neg \psi \leftrightarrow \neg \theta$$
6	1	ord	$$⊢\phi \to \left(\neg \psi \to \chi \right)$$
7	5 6	syl5bir	$$⊢\phi \to \left(\neg \theta \to \chi \right)$$
8	2	ord	$$⊢\phi \to \left(\neg \theta \to \tau \right)$$
9	7 8	jcad	$$⊢\phi \to \left(\neg \theta \to \left(\chi \wedge \tau \right)\right)$$
10	4	biimpar	$$⊢\left(\chi \wedge \tau \right)\to \theta$$
11	9 10	syl6	$$⊢\phi \to \left(\neg \theta \to \theta \right)$$
12	11	pm2.18d	$$⊢\phi \to \theta$$
13	12 3	sylibr	$$⊢\phi \to \psi$$