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

Theorem bi2.04 350
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 76 . 2  |-  ( (
ph  ->  ( ps  ->  ch ) )  ->  ( ps  ->  ( ph  ->  ch ) ) )
2 pm2.04 76 . 2  |-  ( ( ps  ->  ( ph  ->  ch ) )  -> 
( ph  ->  ( ps 
->  ch ) ) )
31, 2impbii 180 1  |-  ( (
ph  ->  ( ps  ->  ch ) )  <->  ( ps  ->  ( ph  ->  ch ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176
This theorem is referenced by:  imim21b  356  pm4.87  567  imimorb  847  ax12bOLD  1675  sbcom  2042  sbcom2  2066  r19.21t  2641  reu8  2974  ra5  3088  unissb  3873  reusv3  4558  fun11  5331  oeordi  6601  marypha1lem  7202  aceq1  7760  pwfseqlem3  8298  prime  10108  raluz2  10284  rlimresb  12055  isprm3  12783  isprm4  12784  acsfn  13577  pgpfac1  15331  pgpfac  15335  fbfinnfr  17552  wilthlem3  20324  isch3  21837  elat2  22936  pm10.541  27665  pm10.542  27666  sbcomwAUX7  29562  sbcomOLD7  29709  sbcom2OLD7  29715  isat3  30119  cdleme32fva  31248
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 177
  Copyright terms: Public domain W3C validator