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

Theorem bi2.04 352
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 182 1  |-  ( (
ph  ->  ( ps  ->  ch ) )  <->  ( ps  ->  ( ph  ->  ch ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 6    <-> wb 178
This theorem is referenced by:  imim21b  358  pm4.87  570  imimorb  852  ax12b  1834  sbcom  1984  sbcom2  2077  r19.21t  2599  reu8  2914  ra5  3019  unissb  3798  reusv3  4479  fun11  5218  oeordi  6518  marypha1lem  7119  aceq1  7677  pwfseqlem3  8215  prime  10024  raluz2  10200  rlimresb  11969  isprm3  12694  isprm4  12695  acsfn  13488  pgpfac1  15242  pgpfac  15246  fbfinnfr  17463  wilthlem3  20235  isch3  21746  elat2  22845  pm10.541  26894  pm10.542  26895  isat3  28627  cdleme32fva  29756
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10
This theorem depends on definitions:  df-bi 179
  Copyright terms: Public domain W3C validator