MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  a1dd 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
Assertion
Ref Expression
a1dd

Proof of Theorem a1dd
StepHypRef Expression
1 a1dd.1 . 2
2 ax-1 6 . 2
31, 2syl6 33 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4
This theorem is referenced by:  merco2  1569  equveli  2088  sotriOLD  5404  xpexr  6740  omordi  7234  omwordi  7239  odi  7247  omass  7248  oen0  7254  oewordi  7259  oewordri  7260  nnmwordi  7303  omabs  7315  fisupg  7788  cantnfle  8111  cantnflem1  8129  cantnfleOLD  8141  cantnflem1OLD  8152  pr2ne  8404  axpowndlem3OLD  8997  gchina  9098  nqereu  9328  supsrlem  9509  1re  9616  lemul1a  10421  nnsub  10599  xlemul1a  11509  xrsupsslem  11527  xrinfmsslem  11528  xrub  11532  supxrunb1  11540  supxrunb2  11541  difelfzle  11817  fsuppmapnn0fiubex  12098  seqcl2  12125  facdiv  12365  facwordi  12367  faclbnd  12368  swrdswrdlem  12684  swrdccat3  12717  exprmfct  14251  prmfac1  14259  pockthg  14424  cply1mul  18335  mdetralt  19110  cmpsub  19900  fbfinnfr  20342  alexsubALTlem2  20548  alexsubALTlem3  20549  ovolicc2lem3  21930  fta1g  22568  fta1  22704  mulcxp  23066  cxpcn3lem  23121  colinearalg  24213  vdn0frgrav2  25023  vdgn0frgrav2  25024  2spotmdisj  25068  numclwwlkovf2ex  25086  dmdbr5ati  27341  cvmlift3lem4  28767  dfon2lem9  29223  fscgr  29730  colinbtwnle  29768  broutsideof2  29772  ordcmp  29912  wl-aleq  29988  itg2addnc  30069  a1i14  30115  a1i24  30116  a1i34  30117  filbcmb  30231  mpt2bi123f  30571  mptbi12f  30575  ac6s6  30580  usgfis  32446  nzerooringczr  32880  ad4ant124  33227  ee323  33277  vd13  33387  vd23  33388  ee03  33538  ee23an  33554  ee32  33556  ee32an  33558  ee123  33560  ltrnid  35859  cdleme25dN  36082
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7
  Copyright terms: Public domain W3C validator