MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  a1dd Structured version   Visualization 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  1242  ad4ant124  1245  ad4ant23  1247  merco2  1630  equveli  2191  xpexr  6765  omordi  7298  omwordi  7303  odi  7311  omass  7312  oen0  7318  oewordi  7323  oewordri  7324  nnmwordi  7367  omabs  7379  fisupg  7850  fiinfg  8046  cantnfle  8207  cantnflem1  8225  pr2ne  8467  gchina  9155  nqereu  9385  supsrlem  9566  1re  9673  lemul1a  10492  nnsub  10681  xlemul1a  11608  xrsupsslem  11626  xrinfmsslem  11627  xrub  11631  supxrunb1  11639  supxrunb2  11640  difelfzle  11940  seqcl2  12269  facdiv  12510  facwordi  12512  faclbnd  12513  swrdswrdlem  12858  swrdccat3  12891  exprmfct  14703  prmfac1  14726  pockthg  14905  cply1mul  18942  mdetralt  19688  cmpsub  20470  fbfinnfr  20911  alexsubALTlem2  21118  alexsubALTlem3  21119  ovolicc2lem3  22527  fta1g  23174  fta1  23317  mulcxp  23686  cxpcn3lem  23743  colinearalg  24996  vdn0frgrav2  25807  vdgn0frgrav2  25808  2spotmdisj  25852  numclwwlkovf2ex  25870  dmdbr5ati  28131  cvmlift3lem4  30095  dfon2lem9  30487  fscgr  30897  colinbtwnle  30935  broutsideof2  30939  a1i14  31005  a1i24  31006  ordcmp  31157  wl-aleq  31914  itg2addnc  32042  filbcmb  32113  mpt2bi123f  32452  mptbi12f  32456  ac6s6  32461  ltrnid  33746  cdleme25dN  33969  ee323  36909  vd13  37024  vd23  37025  ee03  37169  ee23an  37185  ee32  37187  ee32an  37189  ee123  37191  iccpartgt  38876  stgoldbwt  39012  tgoldbach  39046  pfxccat3  39104  propeqop  39136  funopsn  39156  upgrwlkdvdelem  39864  umgr2wlk  39994  usgfis  40127  nzerooringczr  40443
  Copyright terms: Public domain W3C validator