Theorem bi2.04 375

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

Syntax hints:   → wi 4   ↔ wb 196

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 197

This theorem is referenced by:  imim21b  381  pm4.87  607  imimorb  939  r19.21t  2984  r19.21v  2989  reu8  3435  unissb  4501  reusv3  4906  fun11  6001  oeordi  7712  marypha1lem  8380  aceq1  8978  pwfseqlem3  9520  prime  11496  raluz2  11775  rlimresb  14340  isprm3  15443  isprm4  15444  acsfn  16367  pgpfac1  18525  pgpfac  18529  fbfinnfr  21692  wilthlem3  24841  isch3  28226  elat2  29327  isat3  34912  cdleme32fva  36042  elmapintrab  38199  ntrneik2  38707  ntrneix2  38708  ntrneikb  38709  pm10.541  38883  pm10.542  38884