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

Theorem pm5.74da 687
Description: Distribution of implication over biconditional (deduction rule). (Contributed by NM, 4-May-2007.)
Hypothesis
Ref Expression
pm5.74da.1  |-  ( (
ph  /\  ps )  ->  ( ch  <->  th )
)
Assertion
Ref Expression
pm5.74da  |-  ( ph  ->  ( ( ps  ->  ch )  <->  ( ps  ->  th ) ) )

Proof of Theorem pm5.74da
StepHypRef Expression
1 pm5.74da.1 . . 3  |-  ( (
ph  /\  ps )  ->  ( ch  <->  th )
)
21ex 434 . 2  |-  ( ph  ->  ( ps  ->  ( ch 
<->  th ) ) )
32pm5.74d 247 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:  ralbida  2897  ralbidva  2900  ralxpxfr2d  3228  elrab3t  3260  ordunisuc2  6657  dfom2  6680  pwfseqlem3  9034  uzindOLD  10951  lo1resb  13346  rlimresb  13347  o1resb  13348  fsumparts  13579  isprm3  14081  ramval  14381  islindf4  18640  cnntr  19542  fclsbas  20257  metcnp  20779  voliunlem3  21697  ellimc2  22016  limcflf  22020  mdegleb  22199  xrlimcnp  23026  dchrelbas3  23241  lmicom  23831  dmdbr5ati  27017  isarchi3  27393  sscoid  29140  jm2.25  30545  fourierdlem87  31494  cdlemefrs29bpre0  35192  cdlemkid3N  35729  cdlemkid4  35730  hdmap1eulem  36621  hdmap1eulemOLDN  36622
  Copyright terms: Public domain W3C validator