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 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  397  pm4.87  839  imimorb  947  sbrimvlem  2101  r19.21v  3177  r19.21t  3216  reu8  3726  unissb  4872  reusv3  5308  fun11  6430  oeordi  8215  marypha1lem  8899  aceq1  9545  pwfseqlem3  10084  prime  12066  raluz2  12300  rlimresb  14924  isprm3  16029  isprm4  16030  acsfn  16932  pgpfac1  19204  pgpfac  19208  fbfinnfr  22451  wilthlem3  25649  isch3  29020  elat2  30119  fvineqsneq  34695  wl-dfralflem  34840  isat3  36445  cdleme32fva  37575  elmapintrab  39943  ntrneik2  40449  ntrneix2  40450  ntrneikb  40451  pm10.541  40706  pm10.542  40707