Metamath Proof Explorer

Theorem pm5.63

Description: Theorem *5.63 of WhiteheadRussell p. 125. (Contributed by NM, 3-Jan-2005) (Proof shortened by Wolf Lammen, 25-Dec-2012)

Ref Expression
Assertion pm5.63 
|- ( ( ph \/ ps ) <-> ( ph \/ ( -. ph /\ ps ) ) )

Proof

Step Hyp Ref Expression
1 exmid 
 |-  ( ph \/ -. ph )
2 ordi 
 |-  ( ( ph \/ ( -. ph /\ ps ) ) <-> ( ( ph \/ -. ph ) /\ ( ph \/ ps ) ) )
3 1 2 mpbiran 
 |-  ( ( ph \/ ( -. ph /\ ps ) ) <-> ( ph \/ ps ) )
4 3 bicomi 
 |-  ( ( ph \/ ps ) <-> ( ph \/ ( -. ph /\ ps ) ) )