Theorem bi2.04 388

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

Assertion

Ref	Expression
bi2.04	⊢ ((𝜑 → (𝜓 → 𝜒)) ↔ (𝜓 → (𝜑 → 𝜒)))

Proof of Theorem bi2.04

Step	Hyp	Ref	Expression
1		pm2.04 90	. 2 ⊢ ((𝜑 → (𝜓 → 𝜒)) → (𝜓 → (𝜑 → 𝜒)))
2		pm2.04 90	. 2 ⊢ ((𝜓 → (𝜑 → 𝜒)) → (𝜑 → (𝜓 → 𝜒)))
3	1, 2	impbii 208	1 ⊢ ((𝜑 → (𝜓 → 𝜒)) ↔ (𝜓 → (𝜑 → 𝜒)))

Syntax hints:   → wi 4   ↔ wb 205

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 206

This theorem is referenced by:  imim21b  394  pm4.87  839  imimorb  947  sbrimvlem  2095  r19.21v  3100  r19.21t  3137  elabgt  3596  reu8  3663  unissb  4870  reusv3  5323  fun11  6492  oeordi  8380  marypha1lem  9122  aceq1  9804  pwfseqlem3  10347  prime  12331  raluz2  12566  rlimresb  15202  isprm3  16316  isprm4  16317  acsfn  17285  pgpfac1  19598  pgpfac  19602  fbfinnfr  22900  wilthlem3  26124  isch3  29504  elat2  30603  fvineqsneq  35510  isat3  37248  cdleme32fva  38378  isdomn5  40099  elmapintrab  41073  ntrneik2  41591  ntrneix2  41592  ntrneikb  41593  pm10.541  41874  pm10.542  41875