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  886  sbcom2v  1973  mor  2056  r19.21t  2541  reu8  2922  ra5  3039  unissb  3819  reusv3  4438  zfregfr  4551  tfi  4559  fun11  5255  prime  9290  raluz2  9517  isprm3  12050  isprm4  12051  bj-inf2vnlem2  13853