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

Theorem pm5.32d 620
Description: Distribution of implication over biconditional (deduction rule). (Contributed by NM, 29-Oct-1996.)
Hypothesis
Ref Expression
pm5.32d.1  |-  ( ph  ->  ( ps  ->  ( ch 
<->  th ) ) )
Assertion
Ref Expression
pm5.32d  |-  ( ph  ->  ( ( ps  /\  ch )  <->  ( ps  /\  th ) ) )

Proof of Theorem pm5.32d
StepHypRef Expression
1 pm5.32d.1 . 2  |-  ( ph  ->  ( ps  ->  ( ch 
<->  th ) ) )
2 pm5.32 617 . 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    /\ wa 358
This theorem is referenced by:  pm5.32rd  621  pm5.32da  622  anbi2d  684  cbval2  1944  cbvex2  1945  ordpwsuc  4606  cores  5176  isoini  5835  mpt2eq123  5907  rdglim2  6445  fzind  10110  btwnz  10114  elfzm11  10853  isprm2  12766  isprm3  12767  xrecex  23103  elimifd  23151  funcnvmptOLD  23234  funcnvmpt  23235  indpi1  23605  dfres3  24116  dfrdg4  24488  ee7.2aOLD  24900  expdioph  27116  pm14.122b  27623  rexbidar  27649
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  df-an 360
  Copyright terms: Public domain W3C validator