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  2557  ordunisuc2  4635  dfom2  4658  pwfseqlem3  8282  uzindOLD  10106  lo1resb  12038  rlimresb  12039  o1resb  12040  fsumparts  12264  isprm3  12767  ramval  13055  cnntr  17004  fclsbas  17716  metcnp  18087  voliunlem3  18909  ellimc2  19227  limcflf  19231  mdegleb  19450  xrlimcnp  20263  dchrelbas3  20477  dmdbr5ati  23002  islimrs3  25581  ralxpxfr2d  26760  jm2.25  27092  islindf4  27308  cdlemefrs29bpre0  30585  cdlemkid3N  31122  cdlemkid4  31123  hdmap1eulem  32014  hdmap1eulemOLDN  32015
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