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	⊢ ( 𝜑 → ( 𝜓 ∨ 𝜒 ) )
	oplem1.2	⊢ ( 𝜑 → ( 𝜃 ∨ 𝜏 ) )
	oplem1.3	⊢ ( 𝜓 ↔ 𝜃 )
	oplem1.4	⊢ ( 𝜒 → ( 𝜃 ↔ 𝜏 ) )
Assertion	oplem1	⊢ ( 𝜑 → 𝜓 )

Proof

Step	Hyp	Ref	Expression
1		oplem1.1	⊢ ( 𝜑 → ( 𝜓 ∨ 𝜒 ) )
2		oplem1.2	⊢ ( 𝜑 → ( 𝜃 ∨ 𝜏 ) )
3		oplem1.3	⊢ ( 𝜓 ↔ 𝜃 )
4		oplem1.4	⊢ ( 𝜒 → ( 𝜃 ↔ 𝜏 ) )
5	3	notbii	⊢ ( ¬ 𝜓 ↔ ¬ 𝜃 )
6	1	ord	⊢ ( 𝜑 → ( ¬ 𝜓 → 𝜒 ) )
7	5 6	syl5bir	⊢ ( 𝜑 → ( ¬ 𝜃 → 𝜒 ) )
8	2	ord	⊢ ( 𝜑 → ( ¬ 𝜃 → 𝜏 ) )
9	7 8	jcad	⊢ ( 𝜑 → ( ¬ 𝜃 → ( 𝜒 ∧ 𝜏 ) ) )
10	4	biimpar	⊢ ( ( 𝜒 ∧ 𝜏 ) → 𝜃 )
11	9 10	syl6	⊢ ( 𝜑 → ( ¬ 𝜃 → 𝜃 ) )
12	11	pm2.18d	⊢ ( 𝜑 → 𝜃 )
13	12 3	sylibr	⊢ ( 𝜑 → 𝜓 )