Metamath Proof Explorer

Theorem pm4.45

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

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

Proof

Step Hyp Ref Expression
1 orc 
 |-  ( ph -> ( ph \/ ps ) )
2 1 pm4.71i 
 |-  ( ph <-> ( ph /\ ( ph \/ ps ) ) )