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  19789  pgpfac  19793  fbfinnfr  23115  wilthlem3  26342  isch3  29982  elat2  31081  fvineqsneq  35779  isat3  37665  cdleme32fva  38796  isdomn5  40519  elmapintrab  41611  ntrneik2  42129  ntrneix2  42130  ntrneikb  42131  pm10.541  42412  pm10.542  42413
  Copyright terms: Public domain W3C validator