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  sbcom  1983  sbcom2  2074  r19.21t  2590  reu8  2900  ra5  3005  unissb  3755  reusv3  4433  fun11  5172  oeordi  6471  marypha1lem  7070  aceq1  7628  pwfseqlem3  8162  prime  9971  raluz2  10147  rlimresb  11916  isprm3  12641  isprm4  12642  acsfn  13405  pgpfac1  15150  pgpfac  15154  fbfinnfr  17368  wilthlem3  20140  isch3  21651  elat2  22750  pm10.541  26728  pm10.542  26729  isat3  28186  cdleme32fva  29315
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