MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  bi2.04 Structured version   Visualization version   GIF version

Theorem bi2.04 376
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
StepHypRef Expression
1 pm2.04 90 . 2 ((𝜑 → (𝜓𝜒)) → (𝜓 → (𝜑𝜒)))
2 pm2.04 90 . 2 ((𝜓 → (𝜑𝜒)) → (𝜑 → (𝜓𝜒)))
31, 2impbii 199 1 ((𝜑 → (𝜓𝜒)) ↔ (𝜓 → (𝜑𝜒)))
Colors of variables: wff setvar class
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  382  pm4.87  607  imimorb  920  r19.21t  2952  r19.21v  2957  reu8  3396  unissb  4460  reusv3  4867  fun11  5951  oeordi  7652  marypha1lem  8324  aceq1  8925  pwfseqlem3  9467  prime  11443  raluz2  11722  rlimresb  14277  isprm3  15377  isprm4  15378  acsfn  16301  pgpfac1  18460  pgpfac  18464  fbfinnfr  21626  wilthlem3  24777  isch3  28068  elat2  29169  isat3  34413  cdleme32fva  35544  elmapintrab  37701  ntrneik2  38210  ntrneix2  38211  ntrneikb  38212  pm10.541  38386  pm10.542  38387
  Copyright terms: Public domain W3C validator