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

Theorem a1dd 46
Description: Double deduction introducing a antecedent. Deduction associated with a1d 26. Double deduction associated with ax-1 6 and a1i 11. (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:  2a1dd  47  merco2  1591  equveli  2116  xpexr  6726  omordi  7254  omwordi  7259  odi  7267  omass  7268  oen0  7274  oewordi  7279  oewordri  7280  nnmwordi  7323  omabs  7335  fisupg  7804  cantnfle  8124  cantnflem1  8142  cantnfleOLD  8154  cantnflem1OLD  8165  pr2ne  8417  gchina  9109  nqereu  9339  supsrlem  9520  1re  9627  lemul1a  10439  nnsub  10617  xlemul1a  11535  xrsupsslem  11553  xrinfmsslem  11554  xrub  11558  supxrunb1  11566  supxrunb2  11567  difelfzle  11845  seqcl2  12171  facdiv  12411  facwordi  12413  faclbnd  12414  swrdswrdlem  12742  swrdccat3  12775  exprmfct  14462  prmfac1  14470  pockthg  14635  cply1mul  18657  mdetralt  19404  cmpsub  20195  fbfinnfr  20636  alexsubALTlem2  20842  alexsubALTlem3  20843  ovolicc2lem3  22224  fta1g  22862  fta1  22998  mulcxp  23362  cxpcn3lem  23419  colinearalg  24642  vdn0frgrav2  25452  vdgn0frgrav2  25453  2spotmdisj  25497  numclwwlkovf2ex  25515  dmdbr5ati  27767  cvmlift3lem4  29632  dfon2lem9  30023  fscgr  30431  colinbtwnle  30469  broutsideof2  30473  a1i14  30539  a1i24  30540  ordcmp  30692  wl-aleq  31368  itg2addnc  31455  filbcmb  31526  mpt2bi123f  31866  mptbi12f  31870  ac6s6  31875  ltrnid  33165  cdleme25dN  33388  ad4ant13  36254  ad4ant124  36257  ad4ant23  36259  ee323  36307  vd13  36424  vd23  36425  ee03  36575  ee23an  36591  ee32  36593  ee32an  36595  ee123  36597  iccpartgt  37707  stgoldbwt  37843  pfxccat3  37926  usgfis  38088  nzerooringczr  38404
  Copyright terms: Public domain W3C validator