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 389
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 208 1 ((𝜑 → (𝜓𝜒)) ↔ (𝜓 → (𝜑𝜒)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205
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 206
This theorem is referenced by:  imim21b  396  pm4.87  842  imimorb  950  sbrimvw  2095  sbrim  2302  ralcom3  3099  r19.21vOLD  3176  r19.21t  3235  elabgt  3623  reu8  3690  unissb  4899  unissbOLD  4900  reusv3  5359  fun11  6571  oeordi  8502  marypha1lem  9303  aceq1  9987  pwfseqlem3  10530  prime  12515  raluz2  12751  rlimresb  15382  isprm3  16494  isprm4  16495  acsfn  17474  pgpfac1  19788  pgpfac  19792  fbfinnfr  23114  wilthlem3  26341  isch3  29969  elat2  31068  fvineqsneq  35769  isat3  37655  cdleme32fva  38786  isdomn5  40509  elmapintrab  41579  ntrneik2  42097  ntrneix2  42098  ntrneikb  42099  pm10.541  42380  pm10.542  42381
  Copyright terms: Public domain W3C validator