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 374
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 87 . 2 ((𝜑 → (𝜓𝜒)) → (𝜓 → (𝜑𝜒)))
2 pm2.04 87 . 2 ((𝜓 → (𝜑𝜒)) → (𝜑 → (𝜓𝜒)))
31, 2impbii 197 1 ((𝜑 → (𝜓𝜒)) ↔ (𝜓 → (𝜑𝜒)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 194
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 195
This theorem is referenced by:  imim21b  380  pm4.87  605  imimorb  916  r19.21t  2933  r19.21v  2938  reu8  3364  unissb  4395  reusv3  4793  fun11  5859  oeordi  7527  marypha1lem  8195  aceq1  8796  pwfseqlem3  9334  prime  11286  raluz2  11565  rlimresb  14086  isprm3  15176  isprm4  15177  acsfn  16085  pgpfac1  18244  pgpfac  18248  fbfinnfr  21393  wilthlem3  24509  isch3  27284  elat2  28385  isat3  33411  cdleme32fva  34542  elmapintrab  36700  ntrneik2  37209  ntrneix2  37210  ntrneikb  37211  pm10.541  37387  pm10.542  37388
  Copyright terms: Public domain W3C validator