Metamath Proof Explorer

Theorem pm4.83

Description: Theorem *4.83 of WhiteheadRussell p. 122. (Contributed by NM, 3-Jan-2005)

Ref Expression
Assertion pm4.83 
|- ( ( ( ph -> ps ) /\ ( -. ph -> ps ) ) <-> ps )

Proof

Step Hyp Ref Expression
1 exmid 
 |-  ( ph \/ -. ph )
2 1 a1bi 
 |-  ( ps <-> ( ( ph \/ -. ph ) -> ps ) )
3 jaob 
 |-  ( ( ( ph \/ -. ph ) -> ps ) <-> ( ( ph -> ps ) /\ ( -. ph -> ps ) ) )
4 2 3 bitr2i 
 |-  ( ( ( ph -> ps ) /\ ( -. ph -> ps ) ) <-> ps )