Metamath Proof Explorer

Theorem pm5.44

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

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

Proof

Step Hyp Ref Expression
1 jcab 
 |-  ( ( ph -> ( ps /\ ch ) ) <-> ( ( ph -> ps ) /\ ( ph -> ch ) ) )
2 1 baibr 
 |-  ( ( ph -> ps ) -> ( ( ph -> ch ) <-> ( ph -> ( ps /\ ch ) ) ) )