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  2002  raltpd  4156  cores  5516  isoini  6233  mpt2eq123  6351  ordpwsuc  6645  rdglim2  7110  fzind  10971  btwnz  10975  elfzm11  11761  isprm2  14101  isprm3  14102  modprminv  14202  modprminveq  14203  isrim  17253  elimifd  27244  funcnvmptOLD  27332  xrecex  27440  ordtconlem1  27731  indpi1  27860  dfres3  29115  dfrdg4  29527  ee7.2aOLD  29853  wl-ax11-lem8  29959  expdioph  30893  pm14.122b  31232  rexbidar  31257
  Copyright terms: Public domain W3C validator