Theorem bi2.04 247

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 125	1 |- ( ( ph -> ( ps -> ch ) ) <-> ( ps -> ( ph -> ch ) ) )

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

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

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  imim21b  251  pm4.87  547  imimorbdc  882  sbcom2v  1961  mor  2042  r19.21t  2510  reu8  2884  ra5  3001  unissb  3774  reusv3  4389  zfregfr  4496  tfi  4504  fun11  5198  prime  9174  raluz2  9401  isprm3  11835  isprm4  11836  bj-inf2vnlem2  13340