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:  ralbidaOLD  2834  ralxpxfr2d  3183  elrab3t  3215  ordunisuc2  6557  dfom2  6580  pwfseqlem3  8930  uzindOLD  10839  lo1resb  13146  rlimresb  13147  o1resb  13148  fsumparts  13373  isprm3  13876  ramval  14173  islindf4  18378  cnntr  18997  fclsbas  19712  metcnp  20234  voliunlem3  21151  ellimc2  21470  limcflf  21474  mdegleb  21653  xrlimcnp  22480  dchrelbas3  22695  dmdbr5ati  25963  isarchi3  26340  sscoid  28080  jm2.25  29488  cdlemefrs29bpre0  34348  cdlemkid3N  34885  cdlemkid4  34886  hdmap1eulem  35777  hdmap1eulemOLDN  35778
  Copyright terms: Public domain W3C validator