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  837  imimorb  944  sbrimvlem  2092  r19.21v  3175  r19.21t  3214  reu8  3723  unissb  4863  reusv3  5297  fun11  6422  oeordi  8203  marypha1lem  8886  aceq1  9532  pwfseqlem3  10071  prime  12052  raluz2  12286  rlimresb  14912  isprm3  16017  isprm4  16018  acsfn  16920  pgpfac1  19133  pgpfac  19137  fbfinnfr  22379  wilthlem3  25575  isch3  28946  elat2  30045  fvineqsneq  34576  wl-dfralflem  34720  isat3  36325  cdleme32fva  37455  elmapintrab  39816  ntrneik2  40322  ntrneix2  40323  ntrneikb  40324  pm10.541  40579  pm10.542  40580
  Copyright terms: Public domain W3C validator