Metamath Proof Explorer

Theorem pm4.39

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

Ref Expression
Assertion pm4.39 
|- ( ( ( ph <-> ch ) /\ ( ps <-> th ) ) -> ( ( ph \/ ps ) <-> ( ch \/ th ) ) )

Proof

Step Hyp Ref Expression
1 simpl 
 |-  ( ( ( ph <-> ch ) /\ ( ps <-> th ) ) -> ( ph <-> ch ) )
2 simpr 
 |-  ( ( ( ph <-> ch ) /\ ( ps <-> th ) ) -> ( ps <-> th ) )
3 1 2 orbi12d 
 |-  ( ( ( ph <-> ch ) /\ ( ps <-> th ) ) -> ( ( ph \/ ps ) <-> ( ch \/ th ) ) )