Theorem bi2.04 390

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

Syntax hints:   → wi 4   ↔ wb 208

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 209

This theorem is referenced by:  imim21b  398  pm4.87  854  imimorb  963  sbrimvwOLD  2125  sbrim  2338  ralcom3  3112  r19.21t  3256  reu8  3696  sbccomlem  3822  unissb  4899  reusv3  5362  fun11  6595  xpord3inddlem  8134  oeordi  8557  marypha1lem  9379  aceq1  10073  pwfseqlem3  10618  prime  12654  raluz2  12898  rlimresb  15592  isprm3  16717  isprm4  16718  acsfn  17691  pgpfac1  20122  pgpfac  20126  isdomn5  20760  fbfinnfr  23901  wilthlem3  27134  onsfi  28449  isch3  31444  elat2  32543  mh-unprimbi  36904  fvineqsneq  37906  isat3  39931  cdleme32fva  41061  indstrd  42810  elmapintrab  44152  ntrneik2  44668  ntrneix2  44669  ntrneikb  44670  pm10.541  44943  pm10.542  44944