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

Theorem pm5.74da 668
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 423 . 2  |-  ( ph  ->  ( ps  ->  ( ch 
<->  th ) ) )
32pm5.74d 238 1  |-  ( ph  ->  ( ( ps  ->  ch )  <->  ( ps  ->  th ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176    /\ wa 358
This theorem is referenced by:  ralbida  2570  ordunisuc2  4651  dfom2  4674  pwfseqlem3  8298  uzindOLD  10122  lo1resb  12054  rlimresb  12055  o1resb  12056  fsumparts  12280  isprm3  12783  ramval  13071  cnntr  17020  fclsbas  17732  metcnp  18103  voliunlem3  18925  ellimc2  19243  limcflf  19247  mdegleb  19466  xrlimcnp  20279  dchrelbas3  20493  dmdbr5ati  23018  islimrs3  25684  ralxpxfr2d  26863  jm2.25  27195  islindf4  27411  cdlemefrs29bpre0  31207  cdlemkid3N  31744  cdlemkid4  31745  hdmap1eulem  32636  hdmap1eulemOLDN  32637
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 177  df-an 360
  Copyright terms: Public domain W3C validator