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 249 1  |-  ( ph  ->  ( ( ps  ->  ch )  <->  ( ps  ->  th ) ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 186    /\ 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 187  df-an 371
This theorem is referenced by:  ralbida  2839  ralbidva  2842  ralxpxfr2d  3176  elrab3t  3208  ordunisuc2  6664  dfom2  6687  pwfseqlem3  9070  lo1resb  13538  rlimresb  13539  o1resb  13540  fsumparts  13773  isprm3  14437  ramval  14737  islindf4  19167  cnntr  20071  fclsbas  20816  metcnp  21338  voliunlem3  22256  ellimc2  22575  limcflf  22579  mdegleb  22758  xrlimcnp  23626  dchrelbas3  23896  lmicom  24549  dmdbr5ati  27767  isarchi3  28196  cmpcref  28319  sscoid  30264  cdlemefrs29bpre0  33428  cdlemkid3N  33965  cdlemkid4  33966  hdmap1eulem  34857  hdmap1eulemOLDN  34858  jm2.25  35316  fourierdlem87  37357
  Copyright terms: Public domain W3C validator