Metamath Proof Explorer

Theorem pm4.43

Description: Theorem *4.43 of WhiteheadRussell p. 119. (Contributed by NM, 3-Jan-2005) (Proof shortened by Wolf Lammen, 26-Nov-2012)

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

Proof

Step Hyp Ref Expression
1 pm3.24 
 |-  -. ( ps /\ -. ps )
2 1 biorfi 
 |-  ( ph <-> ( ph \/ ( ps /\ -. ps ) ) )
3 ordi 
 |-  ( ( ph \/ ( ps /\ -. ps ) ) <-> ( ( ph \/ ps ) /\ ( ph \/ -. ps ) ) )
4 2 3 bitri 
 |-  ( ph <-> ( ( ph \/ ps ) /\ ( ph \/ -. ps ) ) )