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

Theorem a1dd 47
Description: Double deduction introducing an 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 34 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  48  ad4ant13  1230  ad4ant124  1233  ad4ant23  1235  merco2  1615  equveli  2143  xpexr  6743  omordi  7271  omwordi  7276  odi  7284  omass  7285  oen0  7291  oewordi  7296  oewordri  7297  nnmwordi  7340  omabs  7352  fisupg  7821  fiinfg  8017  cantnfle  8177  cantnflem1  8195  pr2ne  8437  gchina  9124  nqereu  9354  supsrlem  9535  1re  9642  lemul1a  10459  nnsub  10648  xlemul1a  11574  xrsupsslem  11592  xrinfmsslem  11593  xrub  11597  supxrunb1  11605  supxrunb2  11606  difelfzle  11904  seqcl2  12230  facdiv  12471  facwordi  12473  faclbnd  12474  swrdswrdlem  12803  swrdccat3  12836  exprmfct  14633  prmfac1  14656  pockthg  14835  cply1mul  18872  mdetralt  19617  cmpsub  20399  fbfinnfr  20840  alexsubALTlem2  21047  alexsubALTlem3  21048  ovolicc2lem3  22456  fta1g  23102  fta1  23245  mulcxp  23614  cxpcn3lem  23671  colinearalg  24924  vdn0frgrav2  25734  vdgn0frgrav2  25735  2spotmdisj  25779  numclwwlkovf2ex  25797  dmdbr5ati  28058  cvmlift3lem4  30038  dfon2lem9  30429  fscgr  30837  colinbtwnle  30875  broutsideof2  30879  a1i14  30945  a1i24  30946  ordcmp  31097  wl-aleq  31779  itg2addnc  31907  filbcmb  31978  mpt2bi123f  32317  mptbi12f  32321  ac6s6  32326  ltrnid  33616  cdleme25dN  33839  ee323  36719  vd13  36836  vd23  36837  ee03  36986  ee23an  37002  ee32  37004  ee32an  37006  ee123  37008  iccpartgt  38450  stgoldbwt  38586  tgoldbach  38620  pfxccat3  38676  propeqop  38701  funopsn  38714  usgfis  38944  nzerooringczr  39260
  Copyright terms: Public domain W3C validator