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

Theorem pm5.32d 639
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 636 . 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 369
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 371
This theorem is referenced by:  pm5.32rd  640  pm5.32da  641  anbi2d  703  cbvex2OLD  2015  raltpd  4138  cores  5500  isoini  6219  mpt2eq123  6341  ordpwsuc  6635  rdglim2  7100  fzind  10967  btwnz  10971  elfzm11  11758  isprm2  14102  isprm3  14103  modprminv  14203  modprminveq  14204  isrim  17256  elimifd  27293  funcnvmptOLD  27381  xrecex  27489  ordtconlem1  27779  indpi1  27908  dfres3  29163  dfrdg4  29575  ee7.2aOLD  29901  wl-ax11-lem8  30007  expdioph  30940  pm14.122b  31284  rexbidar  31309  isrngim  32425
  Copyright terms: Public domain W3C validator