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 210 1 ((𝜑 → (𝜓𝜒)) ↔ (𝜓 → (𝜑𝜒)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 207
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 208
This theorem is referenced by:  imim21b  395  pm4.87  839  imimorb  946  sbrimvlem  2094  r19.21v  3179  r19.21t  3218  reu8  3727  unissb  4867  reusv3  5301  fun11  6424  oeordi  8206  marypha1lem  8889  aceq1  9535  pwfseqlem3  10074  prime  12055  raluz2  12289  rlimresb  14915  isprm3  16019  isprm4  16020  acsfn  16922  pgpfac1  19124  pgpfac  19128  fbfinnfr  22365  wilthlem3  25561  isch3  28932  elat2  30031  fvineqsneq  34562  wl-dfralflem  34705  isat3  36310  cdleme32fva  37440  elmapintrab  39797  ntrneik2  40303  ntrneix2  40304  ntrneikb  40305  pm10.541  40560  pm10.542  40561
  Copyright terms: Public domain W3C validator