Theorem bi2.04 391

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 91	. 2 ⊢ ((𝜑 → (𝜓 → 𝜒)) → (𝜓 → (𝜑 → 𝜒)))
2		pm2.04 91	. 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  399  pm4.87  856  imimorb  965  sbrimvwOLD  2126  sbrim  2339  ralcom3  3115  r19.21t  3259  reu8  3696  sbccomlem  3822  unissb  4906  reusv3  5376  fun11  6610  xpord3inddlem  8146  oeordi  8569  marypha1lem  9389  aceq1  10097  pwfseqlem3  10640  prime  12672  raluz2  12916  rlimresb  15612  isprm3  16736  isprm4  16737  acsfn  17710  pgpfac1  20147  pgpfac  20151  isdomn5  20809  fbfinnfr  23998  wilthlem3  27234  onsfi  28549  isch3  31593  elat2  32692  mh-unprimbi  37055  fvineqsneq  38058  isat3  40081  cdleme32fva  41211  indstrd  42960  elmapintrab  44302  ntrneik2  44818  ntrneix2  44819  ntrneikb  44820  pm10.541  45077  pm10.542  45078