MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  pm5.74d Unicode version

Theorem pm5.74d 238
Description: Distribution of implication over biconditional (deduction rule). (Contributed by NM, 21-Mar-1996.)
Hypothesis
Ref Expression
pm5.74d.1  |-  ( ph  ->  ( ps  ->  ( ch 
<->  th ) ) )
Assertion
Ref Expression
pm5.74d  |-  ( ph  ->  ( ( ps  ->  ch )  <->  ( ps  ->  th ) ) )

Proof of Theorem pm5.74d
StepHypRef Expression
1 pm5.74d.1 . 2  |-  ( ph  ->  ( ps  ->  ( ch 
<->  th ) ) )
2 pm5.74 235 . 2  |-  ( ( ps  ->  ( ch  <->  th ) )  <->  ( ( ps  ->  ch )  <->  ( ps  ->  th ) ) )
31, 2sylib 188 1  |-  ( ph  ->  ( ( ps  ->  ch )  <->  ( ps  ->  th ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176
This theorem is referenced by:  imbi2d  307  imim21b  356  pm5.74da  668  2mos  2222  dfiin2g  3936  oneqmini  4443  tfindsg  4651  findsg  4683  brecop  6751  dom2lem  6901  indpi  8531  uzindOLD  10106  nn0ind-raph  10112  cncls2  17002  ismbl2  18886  voliunlem3  18909  mdbr2  22876  dmdbr2  22883  mdsl2i  22902  mdsl2bi  22903  ralbidar  27648  cvlsupr3  29534  cdleme32fva  30626  cdlemk33N  31098  cdlemk34  31099
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