Theorem bi2.04 392

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 212	1 ⊢ ((𝜑 → (𝜓 → 𝜒)) ↔ (𝜓 → (𝜑 → 𝜒)))

Syntax hints:   → wi 4   ↔ wb 209

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 210

This theorem is referenced by:  imim21b  398  pm4.87  840  imimorb  948  sbrimvlem  2098  r19.21v  3142  r19.21t  3178  reu8  3672  unissb  4832  reusv3  5271  fun11  6398  oeordi  8196  marypha1lem  8881  aceq1  9528  pwfseqlem3  10071  prime  12051  raluz2  12285  rlimresb  14914  isprm3  16017  isprm4  16018  acsfn  16922  pgpfac1  19195  pgpfac  19199  fbfinnfr  22446  wilthlem3  25655  isch3  29024  elat2  30123  fvineqsneq  34829  wl-dfralflem  35003  isat3  36603  cdleme32fva  37733  elmapintrab  40276  ntrneik2  40795  ntrneix2  40796  ntrneikb  40797  pm10.541  41071  pm10.542  41072