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  569  imimorb  849  ax12bOLD  1657  sbcom  2029  sbcom2  2057  r19.21t  2630  reu8  2963  ra5  3077  unissb  3859  reusv3  4542  fun11  5281  oeordi  6581  marypha1lem  7182  aceq1  7740  pwfseqlem3  8278  prime  10088  raluz2  10264  rlimresb  12034  isprm3  12762  isprm4  12763  acsfn  13556  pgpfac1  15310  pgpfac  15314  fbfinnfr  17531  wilthlem3  20303  isch3  21814  elat2  22913  pm10.541  26962  pm10.542  26963  isat3  28765  cdleme32fva  29894
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