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

Theorem pm5.32d 637
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 634 . 2  |-  ( ( ps  ->  ( ch  <->  th ) )  <->  ( ( ps  /\  ch )  <->  ( ps  /\ 
th ) ) )
31, 2sylib 196 1  |-  ( ph  ->  ( ( ps  /\  ch )  <->  ( ps  /\  th ) ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    /\ wa 367
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 185  df-an 369
This theorem is referenced by:  pm5.32rd  638  pm5.32da  639  anbi2d  701  raltpd  4067  cores  5418  isoini  6135  mpt2eq123  6255  ordpwsuc  6549  rdglim2  7016  fzind  10877  btwnz  10881  elfzm11  11671  isprm2  14227  isprm3  14228  modprminv  14328  modprminveq  14329  isrim  17495  elimifd  27546  funcnvmptOLD  27655  xrecex  27769  ordtconlem1  28060  indpi1  28170  dfres3  29354  dfrdg4  29753  ee7.2aOLD  30079  wl-ax11-lem8  30197  expdioph  31131  pm14.122b  31498  rexbidar  31523  isrngim  32910
  Copyright terms: Public domain W3C validator