Theorem bi2.04 248

Description: Logical equivalence of commuted antecedents. Part of Theorem *4.87 of [WhiteheadRussell] p. 122. (Contributed by NM, 5-Aug-1993.)

Assertion

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

Proof of Theorem bi2.04

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

Syntax hints:   -> wi 4   <-> wb 105

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia2 107  ax-ia3 108

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  imim21b  253  pm4.87  557  imimorbdc  897  sbcom2v  2004  mor  2087  r19.21t  2572  reu8  2960  ra5  3078  unissb  3870  reusv3  4496  zfregfr  4611  tfi  4619  fun11  5326  prime  9427  raluz2  9655  isprm3  12296  isprm4  12297  bj-inf2vnlem2  15627