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

Theorem bi2.04 351
Description: Logical equivalence of commuted antecedents. Part of Theorem *4.87 of [WhiteheadRussell] p. 122. (Contributed by NM, 5-Aug-1993.)
Assertion
Ref Expression
bi2.04  |-  ( (
ph  ->  ( ps  ->  ch ) )  <->  ( ps  ->  ( ph  ->  ch ) ) )

Proof of Theorem bi2.04
StepHypRef Expression
1 pm2.04 78 . 2  |-  ( (
ph  ->  ( ps  ->  ch ) )  ->  ( ps  ->  ( ph  ->  ch ) ) )
2 pm2.04 78 . 2  |-  ( ( ps  ->  ( ph  ->  ch ) )  -> 
( ph  ->  ( ps 
->  ch ) ) )
31, 2impbii 181 1  |-  ( (
ph  ->  ( ps  ->  ch ) )  <->  ( ps  ->  ( ph  ->  ch ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177
This theorem is referenced by:  imim21b  357  pm4.87  568  imimorb  848  ax12bOLD  1702  sbcom  2164  sbcom2  2189  r19.21t  2783  reu8  3122  ra5  3237  unissb  4037  reusv3  4722  fun11  5507  oeordi  6821  marypha1lem  7429  aceq1  7987  pwfseqlem3  8524  prime  10339  raluz2  10515  rlimresb  12347  isprm3  13076  isprm4  13077  acsfn  13872  pgpfac1  15626  pgpfac  15630  fbfinnfr  17861  wilthlem3  20841  isch3  22732  elat2  23831  pm10.541  27477  pm10.542  27478  sbcomwAUX7  29439  sbcom2NEW7  29493  sbcomOLD7  29594  isat3  29944  cdleme32fva  31073
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 178
  Copyright terms: Public domain W3C validator