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  546  imimorbdc  881  sbcom2v  1960  mor  2041  r19.21t  2507  reu8  2880  ra5  2997  unissb  3766  reusv3  4381  zfregfr  4488  tfi  4496  fun11  5190  prime  9150  raluz2  9374  isprm3  11799  isprm4  11800  bj-inf2vnlem2  13169