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 376
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 200 1 ((𝜑 → (𝜓𝜒)) ↔ (𝜓 → (𝜑𝜒)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 197
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 198
This theorem is referenced by:  imim21b  382  pm4.87  858  imimorb  962  r19.21t  3107  r19.21v  3112  reu8  3560  unissb  4616  reusv3  5019  fun11  6114  oeordi  7842  marypha1lem  8516  aceq1  9161  pwfseqlem3  9705  prime  11682  raluz2  11961  rlimresb  14526  isprm3  15624  isprm4  15625  acsfn  16547  pgpfac1  18707  pgpfac  18711  fbfinnfr  21885  wilthlem3  25038  isch3  28455  elat2  29556  isat3  35131  cdleme32fva  36262  elmapintrab  38422  ntrneik2  38930  ntrneix2  38931  ntrneikb  38932  pm10.541  39106  pm10.542  39107
  Copyright terms: Public domain W3C validator