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

Theorem pm5.74da 669
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 424 . 2  |-  ( ph  ->  ( ps  ->  ( ch 
<->  th ) ) )
32pm5.74d 239 1  |-  ( ph  ->  ( ( ps  ->  ch )  <->  ( ps  ->  th ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177    /\ wa 359
This theorem is referenced by:  ralbida  2719  ordunisuc2  4824  dfom2  4847  pwfseqlem3  8535  uzindOLD  10364  lo1resb  12358  rlimresb  12359  o1resb  12360  fsumparts  12585  isprm3  13088  ramval  13376  cnntr  17339  fclsbas  18053  metcnp  18571  voliunlem3  19446  ellimc2  19764  limcflf  19768  mdegleb  19987  xrlimcnp  20807  dchrelbas3  21022  dmdbr5ati  23925  sscoid  25758  ralxpxfr2d  26741  jm2.25  27070  islindf4  27285  cdlemefrs29bpre0  31193  cdlemkid3N  31730  cdlemkid4  31731  hdmap1eulem  32622  hdmap1eulemOLDN  32623
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 178  df-an 361
  Copyright terms: Public domain W3C validator