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 
|- ( ph -> ( ps \/ ch ) )
oplem1.2 
|- ( ph -> ( th \/ ta ) )
oplem1.3 
|- ( ps <-> th )
oplem1.4 
|- ( ch -> ( th <-> ta ) )
Assertion oplem1 
|- ( ph -> ps )

Proof

Step Hyp Ref Expression
1 oplem1.1 
 |-  ( ph -> ( ps \/ ch ) )
2 oplem1.2 
 |-  ( ph -> ( th \/ ta ) )
3 oplem1.3 
 |-  ( ps <-> th )
4 oplem1.4 
 |-  ( ch -> ( th <-> ta ) )
5 3 notbii 
 |-  ( -. ps <-> -. th )
6 1 ord 
 |-  ( ph -> ( -. ps -> ch ) )
7 5 6 biimtrrid 
 |-  ( ph -> ( -. th -> ch ) )
8 2 ord 
 |-  ( ph -> ( -. th -> ta ) )
9 7 8 jcad 
 |-  ( ph -> ( -. th -> ( ch /\ ta ) ) )
10 4 biimpar 
 |-  ( ( ch /\ ta ) -> th )
11 9 10 syl6 
 |-  ( ph -> ( -. th -> th ) )
12 11 pm2.18d 
 |-  ( ph -> th )
13 12 3 sylibr 
 |-  ( ph -> ps )