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

Theorem bi2.04 393
 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 212 1 ((𝜑 → (𝜓𝜒)) ↔ (𝜓 → (𝜑𝜒)))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 209 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 210 This theorem is referenced by:  imim21b  399  pm4.87  841  imimorb  949  sbrimvlem  2099  r19.21v  3107  r19.21t  3143  reu8  3648  unissb  4830  reusv3  5272  fun11  6407  oeordi  8221  marypha1lem  8920  aceq1  9567  pwfseqlem3  10110  prime  12092  raluz2  12327  rlimresb  14960  isprm3  16069  isprm4  16070  acsfn  16978  pgpfac1  19260  pgpfac  19264  fbfinnfr  22531  wilthlem3  25744  isch3  29113  elat2  30212  fvineqsneq  35099  wl-dfralflem  35273  isat3  36873  cdleme32fva  38003  elmapintrab  40639  ntrneik2  41158  ntrneix2  41159  ntrneikb  41160  pm10.541  41434  pm10.542  41435
 Copyright terms: Public domain W3C validator