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  1977  raltpd  3997  cores  5340  isoini  6028  mpt2eq123  6144  ordpwsuc  6425  rdglim2  6887  fzind  10739  btwnz  10743  elfzm11  11527  isprm2  13770  isprm3  13771  modprminv  13869  modprminveq  13870  isrim  16821  elimifd  25904  funcnvmptOLD  25985  xrecex  26094  ordtconlem1  26353  indpi1  26477  dfres3  27568  dfrdg4  27980  ee7.2aOLD  28306  wl-ax11-lem8  28406  expdioph  29370  pm14.122b  29675  rexbidar  29700
  Copyright terms: Public domain W3C validator