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

Theorem pm5.32d 622
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 619 . 2  |-  ( ( ps  ->  ( ch  <->  th ) )  <->  ( ( ps  /\  ch )  <->  ( ps  /\ 
th ) ) )
31, 2sylib 190 1  |-  ( ph  ->  ( ( ps  /\  ch )  <->  ( ps  /\  th ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 178    /\ wa 360
This theorem is referenced by:  pm5.32rd  623  pm5.32da  624  anbi2d  686  cbval2OLD  1991  cbvex2  1992  ordpwsuc  4797  cores  5375  isoini  6060  mpt2eq123  6135  rdglim2  6692  fzind  10370  btwnz  10374  elfzm11  11118  isprm2  13089  isprm3  13090  elimifd  24006  funcnvmptOLD  24084  xrecex  24168  indpi1  24421  dfres3  25384  dfrdg4  25797  ee7.2aOLD  26213  expdioph  27096  pm14.122b  27602  rexbidar  27627  modprminv  28247  modprminveq  28248  cbval2OLD7  29792  cbvex2OLD7  29793
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 179  df-an 362
  Copyright terms: Public domain W3C validator