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

Theorem syl21anc 1227
Description: Syllogism combined with contraction. (Contributed by Jeff Hankins, 1-Aug-2009.)
Hypotheses
Ref Expression
sylXanc.1
sylXanc.2
sylXanc.3
syl21anc.4
Assertion
Ref Expression
syl21anc

Proof of Theorem syl21anc
StepHypRef Expression
1 sylXanc.1 . . 3
2 sylXanc.2 . . 3
3 sylXanc.3 . . 3
41, 2, 3jca31 534 . 2
5 syl21anc.4 . 2
64, 5syl 16 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  /\wa 369
This theorem is referenced by:  wereu2  4881  brcogw  5176  funprg  5642  funtpg  5643  fnunsn  5693  fresaun  5761  fvun1  5944  iinpreima  6017  ftpg  6081  fsnunf  6109  soisores  6223  isotr  6232  off  6554  caofrss  6573  caonncan  6578  fvmpt2curryd  7019  oaf1o  7231  omeulem1  7250  oeordi  7255  oelimcl  7268  oeeulem  7269  oeeui  7270  oaabs2  7313  omabs  7315  pmresg  7466  ralxpmap  7488  domunsncan  7637  mapunen  7706  sucdom2  7734  unxpdom2  7748  sucxpdom  7749  ac6sfi  7784  unblem4  7795  fodomfi  7819  hartogslem1  7988  brwdom2  8020  cantnflt  8112  cantnflem3  8131  cantnflem4  8132  cantnfltOLD  8142  cantnflem3OLD  8153  cantnflem4OLD  8154  cnfcomlem  8164  cnfcom  8165  cnfcomlemOLD  8172  cnfcomOLD  8173  infxpenlem  8412  infxpenc  8416  infxpencOLD  8421  fseqenlem1  8426  pwsdompw  8605  cfeq0  8657  cofsmo  8670  cfsmolem  8671  ssfin4  8711  hsmexlem4  8830  hsmexlem5  8831  axdc3lem2  8852  axdc3lem4  8854  fpwwe2  9042  wunpr  9108  mulclpi  9292  mulcanenq  9359  distrlem4pr  9425  prlem934  9432  prlem936  9446  divge0d  11321  fseq1p1m1  11781  elfznelfzob  11916  seqcaopr2  12143  facavg  12379  hashimarn  12496  swrdspsleq  12673  cats1un  12701  f1oun2prg  12865  sqrtdiv  13099  sqrtdivd  13255  mulcn2  13418  o1of2  13435  fsumsplit  13562  sumsplit  13583  isumless  13657  demoivreALT  13936  rpnnen2lem11  13958  qredeu  14248  isprm5  14253  rpexp  14261  rpdvds  14265  divnumden  14281  divdenle  14282  phimullem  14309  pythagtriplem4  14343  pythagtriplem8  14347  pythagtriplem9  14348  pcgcd1  14400  sumhash  14415  fldivp1  14416  pockthlem  14423  ssc2  15191  mndpropd  15946  grpidssd  16114  grpinvssd  16115  issubg2  16216  isnsg3  16235  eqgid  16253  gass  16339  symgextres  16450  gsmsymgreqlem2  16456  sylow1lem5  16622  sylow2alem2  16638  sylow3lem3  16649  efgredlemd  16762  efgredlem  16765  frgpnabllem1  16877  frgpnabllem2  16878  subgdmdprd  17081  ablfacrplem  17116  kerf1hrm  17392  issrngd  17510  lmodprop2d  17572  lsspropd  17663  pwssplit1  17705  lspvadd  17742  mplsubglem  18093  mplsubglemOLD  18095  mplind  18167  znidomb  18600  znrrg  18604  lindfind  18851  lindsind  18852  mat1ghm  18985  mdetunilem1  19114  mdetunilem3  19116  mdetunilem4  19117  mdetunilem9  19122  cramerimplem2  19186  mat2pmatlin  19236  monmatcollpw  19280  cpmadugsumlemF  19377  mretopd  19593  neiptopnei  19633  neitr  19681  ufilen  20431  flimrest  20484  flimclslem  20485  fclsrest  20525  cnextcn  20567  haustsms2  20635  tsmsxplem2  20656  trust  20732  utoptop  20737  restutop  20740  ustuqtop4  20747  utopsnneiplem  20750  utop2nei  20753  utop3cls  20754  isucn2  20782  ucnima  20784  ucncn  20788  fmucnd  20795  trcfilu  20797  comet  21016  metustexhalfOLD  21066  metustexhalf  21067  metustOLD  21070  metust  21071  metustblOLD  21083  metustbl  21084  metutopOLD  21085  psmetutop  21086  nrmmetd  21095  reconnlem1  21331  reconnlem2  21332  fsumcn  21374  cmetcaulem  21727  iscmet3lem1  21730  iscmet3lem2  21731  bcthlem5  21767  rrxdstprj1  21836  minveclem4  21847  ovolfiniun  21912  itg1addlem4  22106  itg1addlem5  22107  itgsplitioo  22244  c1liplem1  22397  dvfsumlem1  22427  plyeq0lem  22607  quotcan  22705  psercnlem1  22820  cxplea  23077  birthdaylem3  23283  musumsum  23468  dvdsmulf1o  23470  dchrelbas4  23518  dchrhash  23546  2sqlem8a  23646  2sqlem8  23647  chto1ub  23661  vmadivsum  23667  dchrisumlem1  23674  dchrvmasumlem2  23683  dchrvmasumiflem1  23686  rpvmasum2  23697  mulog2sumlem2  23720  selberg2lem  23735  pntrmax  23749  pntpbnd1  23771  pntlemb  23782  pntlemj  23788  ercgrg  23908  motcgr  23923  tglineeltr  24011  colline  24030  miriso  24050  midexlem  24069  perpneq  24091  foot  24096  f1otrg  24174  f1otrge  24175  axcontlem9  24275  uhgraun  24311  umgraun  24328  2wlklemA  24556  2wlklemB  24557  2wlklemC  24558  constr3trllem3  24652  vdgrun  24901  vdgrfiun  24902  eupap1  24976  nmblolbii  25714  minvecolem3  25792  minvecolem4  25796  htthlem  25834  bcs2  26099  nmopub2tALT  26828  nmfnleub2  26845  eighmorth  26883  nmophmi  26950  nmopcoadji  27020  hstle  27149  atcvat3i  27315  disjxpin  27447  off2  27481  xppreima2  27488  fgreu  27513  resf1o  27553  fpwrelmap  27556  xrofsup  27582  eliccelico  27588  elicoelioo  27589  iocinif  27592  difioo  27593  gcdnncl  27607  2sqcoprm  27635  2sqmod  27636  ressprs  27643  tleile  27649  xrge0addgt0  27681  xrge0adddir  27682  omndmul3  27703  archirng  27732  archirngz  27733  gsumle  27770  orngmul  27793  qtophaus  27839  locfinref  27844  metideq  27872  sqsscirc2  27891  tpr2rico  27894  fmcncfil  27913  lmxrge0  27934  lmdvg  27935  qqhval2lem  27962  qqhf  27967  qqhnm  27971  esumle  28065  gsumesum  28067  esumlef  28070  esumpcvgval  28084  ofcf  28102  imambfm  28233  oddpwdc  28293  eulerpartlems  28299  eulerpartlemb  28307  eulerpartlemt  28310  iwrdsplit  28326  sseqfn  28329  sseqf  28331  sseqfres  28332  ballotlemfc0  28431  ballotlemfcc  28432  ballotlemfrcn0  28468  sgnsub  28483  plymulx0  28504  signsplypnf  28507  signsvtn0  28527  signstfvneq0  28529  signsvtp  28540  signsvtn  28541  cvxscon  28688  elmrsubrn  28880  nobndup  29460  nobnddown  29461  mblfinlem3  30053  itg2addnclem3  30068  ftc1cnnclem  30088  neibastop3  30180  mapfzcons  30648  mzpcl34  30663  mzpindd  30678  mzpsubst  30681  diophrw  30692  diophren  30747  irrapxlem1  30758  pellexlem5  30769  acongrep  30918  pwssplit4  31035  phisum  31159  mulltgt0  31397  fnchoice  31404  3adantlr3  31417  3adantll2  31420  3adantll3  31421  fmuldfeq  31577  mccl  31606  limccog  31626  limcrecl  31635  lptioo1  31638  islpcn  31645  limsupre  31647  neglimc  31653  0ellimcdiv  31655  limclner  31657  icccncfext  31690  fprodcncf  31704  dvnmptdivc  31735  dvnmul  31740  dvmptfprod  31742  dvnprodlem3  31745  stoweidlem25  31807  stoweidlem34  31816  stoweidlem38  31820  stoweidlem44  31826  stoweidlem48  31830  stoweidlem49  31831  stoweidlem59  31841  stoweidlem60  31842  wallispilem4  31850  stirlinglem5  31860  dirkercncflem2  31886  fourierdlem39  31928  fourierdlem42  31931  fourierdlem46  31935  fourierdlem47  31936  fourierdlem48  31937  fourierdlem50  31939  fourierdlem51  31940  fourierdlem64  31953  fourierdlem73  31962  fourierdlem74  31963  fourierdlem77  31966  fourierdlem80  31969  fourierdlem87  31976  fourierdlem94  31983  fourierdlem103  31992  fourierdlem104  31993  etransclem32  32049  uhgun  32380  estrreslem1  32643  lincresunit2  33079  4an4132  33268  bnj927  33827  bnj1536  33912  bnj1001  34016  bnj1280  34076  lautlt  35815  lautcvr  35816  lauteq  35819  lautco  35821  ltrncl  35849  ltrncnvleN  35854  trljat2  35892  cdlemc6  35921  cdleme20c  36037  cdleme20j  36044  cdleme22e  36070  cdleme22eALTN  36071  cdlemg7aN  36351  cdlemg12e  36373  cdlemg17dALTN  36390  cdlemh  36543  cdlemkfid1N  36647  dibglbN  36893  diblss  36897  diclspsn  36921  dih1  37013  dihglbcpreN  37027  dihmeetlem4preN  37033  lcfrlem19  37288
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 185  df-an 371
  Copyright terms: Public domain W3C validator