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  3175  r19.21t  3214  reu8  3724  unissb  4870  reusv3  5306  fun11  6428  oeordi  8213  marypha1lem  8897  aceq1  9543  pwfseqlem3  10082  prime  12064  raluz2  12298  rlimresb  14922  isprm3  16027  isprm4  16028  acsfn  16930  pgpfac1  19202  pgpfac  19206  fbfinnfr  22449  wilthlem3  25647  isch3  29018  elat2  30117  fvineqsneq  34696  wl-dfralflem  34853  isat3  36458  cdleme32fva  37588  elmapintrab  39956  ntrneik2  40462  ntrneix2  40463  ntrneikb  40464  pm10.541  40719  pm10.542  40720