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 379
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 201 1 ((𝜑 → (𝜓𝜒)) ↔ (𝜓 → (𝜑𝜒)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 198
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 199
This theorem is referenced by:  imim21b  385  pm4.87  876  imimorb  980  r19.21t  3164  r19.21v  3169  reu8  3627  unissb  4691  reusv3  5105  fun11  6196  oeordi  7934  marypha1lem  8608  aceq1  9253  pwfseqlem3  9797  prime  11786  raluz2  12019  rlimresb  14673  isprm3  15768  isprm4  15769  acsfn  16672  pgpfac1  18833  pgpfac  18837  fbfinnfr  22015  wilthlem3  25209  isch3  28653  elat2  29754  isat3  35382  cdleme32fva  36512  elmapintrab  38723  ntrneik2  39230  ntrneix2  39231  ntrneikb  39232  pm10.541  39406  pm10.542  39407
  Copyright terms: Public domain W3C validator