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

Theorem pm5.32d 643
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 640 . 2  |-  ( ( ps  ->  ( ch  <->  th ) )  <->  ( ( ps  /\  ch )  <->  ( ps  /\ 
th ) ) )
31, 2sylib 199 1  |-  ( ph  ->  ( ( ps  /\  ch )  <->  ( ps  /\  th ) ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 187    /\ wa 370
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 188  df-an 372
This theorem is referenced by:  pm5.32rd  644  pm5.32da  645  anbi2d  708  raltpd  4123  cores  5357  isoini  6244  mpt2eq123  6364  ordpwsuc  6656  rdglim2  7161  fzind  11040  btwnz  11044  elfzm11  11872  isprm2  14631  isprm3  14632  modprminv  14749  modprminveq  14750  isrim  17960  elimifd  28162  funcnvmptOLD  28272  xrecex  28396  ordtconlem1  28738  indpi1  28851  dfres3  30406  dfrdg4  30723  ee7.2aOLD  31126  wl-ax11-lem8  31886  expdioph  35848  pm14.122b  36744  rexbidar  36769  isrngim  39523
  Copyright terms: Public domain W3C validator