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  1656  sbcom  2029  sbcom2  2053  r19.21t  2628  reu8  2961  ra5  3075  unissb  3857  reusv3  4542  fun11  5315  oeordi  6585  marypha1lem  7186  aceq1  7744  pwfseqlem3  8282  prime  10092  raluz2  10268  rlimresb  12039  isprm3  12767  isprm4  12768  acsfn  13561  pgpfac1  15315  pgpfac  15319  fbfinnfr  17536  wilthlem3  20308  isch3  21821  elat2  22920  pm10.541  27562  pm10.542  27563  isat3  29497  cdleme32fva  30626
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