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

Theorem a1dd 46
Description: Deduction introducing a nested embedded antecedent. (Contributed by NM, 17-Dec-2004.) (Proof shortened by Mel L. O'Cat, 15-Jan-2008.)
Hypothesis
Ref Expression
a1dd.1  |-  ( ph  ->  ( ps  ->  ch ) )
Assertion
Ref Expression
a1dd  |-  ( ph  ->  ( ps  ->  ( th  ->  ch ) ) )

Proof of Theorem a1dd
StepHypRef Expression
1 a1dd.1 . 2  |-  ( ph  ->  ( ps  ->  ch ) )
2 ax-1 6 . 2  |-  ( ch 
->  ( th  ->  ch ) )
31, 2syl6 33 1  |-  ( ph  ->  ( ps  ->  ( th  ->  ch ) ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7
This theorem is referenced by:  merco2  1556  equveli  2074  sotriOLD  5389  xpexr  6725  omordi  7217  omwordi  7222  odi  7230  omass  7231  oen0  7237  oewordi  7242  oewordri  7243  nnmwordi  7286  omabs  7298  fisupg  7770  cantnfle  8093  cantnflem1  8111  cantnfleOLD  8123  cantnflem1OLD  8134  pr2ne  8386  axpowndlem3OLD  8979  gchina  9080  nqereu  9310  supsrlem  9491  1re  9598  lemul1a  10403  nnsub  10581  xlemul1a  11491  xrsupsslem  11509  xrinfmsslem  11510  xrub  11514  supxrunb1  11522  supxrunb2  11523  difelfzle  11799  fsuppmapnn0fiubex  12080  seqcl2  12107  facdiv  12347  facwordi  12349  faclbnd  12350  swrdswrdlem  12666  swrdccat3  12699  exprmfct  14233  prmfac1  14241  pockthg  14406  cply1mul  18314  mdetralt  19088  cmpsub  19878  fbfinnfr  20320  alexsubALTlem2  20526  alexsubALTlem3  20527  ovolicc2lem3  21908  fta1g  22546  fta1  22682  mulcxp  23044  cxpcn3lem  23099  colinearalg  24191  vdn0frgrav2  25001  vdgn0frgrav2  25002  2spotmdisj  25046  numclwwlkovf2ex  25064  dmdbr5ati  27319  cvmlift3lem4  28745  dfon2lem9  29199  fscgr  29706  colinbtwnle  29744  broutsideof2  29748  ordcmp  29888  wl-aleq  29964  itg2addnc  30045  a1i14  30091  a1i24  30092  a1i34  30093  filbcmb  30207  mpt2bi123f  30547  mptbi12f  30551  ac6s6  30556  usgfis  32400  ad4ant124  33095  ee323  33145  vd13  33255  vd23  33256  ee03  33406  ee23an  33422  ee32  33424  ee32an  33426  ee123  33428  ltrnid  35734  cdleme25dN  35957
  Copyright terms: Public domain W3C validator