This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 biimtrrid ⊢ ( 𝜑 → ( ¬ 𝜃 → 𝜒 ) )
8 2 ord ⊢ ( 𝜑 → ( ¬ 𝜃 → 𝜏 ) )
9 7 8 jcad ⊢ ( 𝜑 → ( ¬ 𝜃 → ( 𝜒 ∧ 𝜏 ) ) )
10 4 biimpar ⊢ ( ( 𝜒 ∧ 𝜏 ) → 𝜃 )
11 9 10 syl6 ⊢ ( 𝜑 → ( ¬ 𝜃 → 𝜃 ) )
12 11 pm2.18d ⊢ ( 𝜑 → 𝜃 )
13 12 3 sylibr ⊢ ( 𝜑 → 𝜓 )