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  2255  dfiin2g  3973  oneqmini  4480  tfindsg  4688  findsg  4720  brecop  6794  dom2lem  6944  indpi  8576  uzindOLD  10153  nn0ind-raph  10159  cncls2  17058  ismbl2  18939  voliunlem3  18962  mdbr2  22931  dmdbr2  22938  mdsl2i  22957  mdsl2bi  22958  ralbidar  26796  cvlsupr3  29352  cdleme32fva  30444  cdlemk33N  30916  cdlemk34  30917
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