Metamath Proof Explorer

Theorem bi2.04

Description: Logical equivalence of commuted antecedents. Part of Theorem *4.87 of WhiteheadRussell p. 122. (Contributed by NM, 11-May-1993)

Ref Expression
Assertion bi2.04 
|- ( ( ph -> ( ps -> ch ) ) <-> ( ps -> ( ph -> ch ) ) )

Proof

Step Hyp Ref Expression
1 pm2.04 
 |-  ( ( ph -> ( ps -> ch ) ) -> ( ps -> ( ph -> ch ) ) )
2 pm2.04 
 |-  ( ( ps -> ( ph -> ch ) ) -> ( ph -> ( ps -> ch ) ) )
3 1 2 impbii 
 |-  ( ( ph -> ( ps -> ch ) ) <-> ( ps -> ( ph -> ch ) ) )