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

Theorem pm5.74d 240
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 237 . 2  |-  ( ( ps  ->  ( ch  <->  th ) )  <->  ( ( ps  ->  ch )  <->  ( ps  ->  th ) ) )
31, 2sylib 190 1  |-  ( ph  ->  ( ( ps  ->  ch )  <->  ( ps  ->  th ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 178
This theorem is referenced by:  imbi2d  309  imim21b  358  pm5.74da  670  cbval2  1990  dvelimdf  2071  sbied  2152  dfiin2g  4126  oneqmini  4634  tfindsg  4842  findsg  4874  brecop  6999  dom2lem  7149  indpi  8786  uzindOLD  10366  nn0ind-raph  10372  cncls2  17339  ismbl2  19425  voliunlem3  19448  mdbr2  23801  dmdbr2  23808  mdsl2i  23827  mdsl2bi  23828  ralbidar  27626  cvlsupr3  30204  cdleme32fva  31296  cdlemk33N  31768  cdlemk34  31769
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 179
  Copyright terms: Public domain W3C validator