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 375
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 199 1 ((𝜑 → (𝜓𝜒)) ↔ (𝜓 → (𝜑𝜒)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196
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 197
This theorem is referenced by:  imim21b  381  pm4.87  607  imimorb  939  r19.21t  2984  r19.21v  2989  reu8  3435  unissb  4501  reusv3  4906  fun11  6001  oeordi  7712  marypha1lem  8380  aceq1  8978  pwfseqlem3  9520  prime  11496  raluz2  11775  rlimresb  14340  isprm3  15443  isprm4  15444  acsfn  16367  pgpfac1  18525  pgpfac  18529  fbfinnfr  21692  wilthlem3  24841  isch3  28226  elat2  29327  isat3  34912  cdleme32fva  36042  elmapintrab  38199  ntrneik2  38707  ntrneix2  38708  ntrneikb  38709  pm10.541  38883  pm10.542  38884
  Copyright terms: Public domain W3C validator