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  1957  cbvex2  1958  ordpwsuc  4622  cores  5192  isoini  5851  mpt2eq123  5923  rdglim2  6461  fzind  10126  btwnz  10130  elfzm11  10869  isprm2  12782  isprm3  12783  xrecex  23119  elimifd  23167  funcnvmptOLD  23249  funcnvmpt  23250  indpi1  23620  dfres3  24187  dfrdg4  24560  ee7.2aOLD  24972  expdioph  27219  pm14.122b  27726  rexbidar  27752  cbval2OLD7  29684  cbvex2OLD7  29685
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