MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  syl31anc Structured version   Visualization version   GIF version

Theorem syl31anc 1321
Description: Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.)
Hypotheses
Ref Expression
syl12anc.1 (𝜑𝜓)
syl12anc.2 (𝜑𝜒)
syl12anc.3 (𝜑𝜃)
syl22anc.4 (𝜑𝜏)
syl31anc.5 (((𝜓𝜒𝜃) ∧ 𝜏) → 𝜂)
Assertion
Ref Expression
syl31anc (𝜑𝜂)

Proof of Theorem syl31anc
StepHypRef Expression
1 syl12anc.1 . . 3 (𝜑𝜓)
2 syl12anc.2 . . 3 (𝜑𝜒)
3 syl12anc.3 . . 3 (𝜑𝜃)
41, 2, 33jca 1235 . 2 (𝜑 → (𝜓𝜒𝜃))
5 syl22anc.4 . 2 (𝜑𝜏)
6 syl31anc.5 . 2 (((𝜓𝜒𝜃) ∧ 𝜏) → 𝜂)
74, 5, 6syl2anc 691 1 (𝜑𝜂)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383  w3a 1031
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 196  df-an 385  df-3an 1033
This theorem is referenced by:  syl32anc  1326  stoic4b  1694  elovmpt3rab1  6791  smo11  7348  omeulem2  7550  oeeui  7569  oaabs2  7612  omabs  7614  omxpenlem  7946  map2xp  8015  mapdom2  8016  fsuppsssupp  8174  cantnflt  8452  cnfcom  8480  mapcdaen  8889  pwsdompw  8909  cofsmo  8974  fin1a2lem4  9108  ltmul12a  10758  lt2msq1  10786  ledivp1  10804  lemul1ad  10842  lemul2ad  10843  supaddc  10867  supadd  10868  supmul1  10869  supmul  10872  rpnnen1lem3  11692  rpnnen1lem5  11694  rpnnen1lem3OLD  11698  rpnnen1lem5OLD  11700  lediv2ad  11770  xaddge0  11960  xadddi  11997  xadddi2  11999  supicc  12191  supiccub  12192  supicclub  12193  difelfznle  12322  flval3  12478  fseqsupubi  12639  expcan  12775  ltexp2  12776  ltexp2r  12779  expubnd  12783  ltexp2rd  12895  ltexp2d  12900  leexp2d  12901  expcand  12902  swrdid  13280  swrd0fv  13291  swrds1  13303  ccatswrd  13308  swrdccat2  13310  swrdccatin2  13338  swrdccatin12lem2  13340  swrdccatin12lem3  13341  splfv1  13357  cshwidxmod  13400  wrdl3s3  13553  o1fsum  14386  mertenslem1  14455  eftlub  14678  rpnnen2lem4  14785  ruclem12  14809  dvdsadd  14862  3dvds  14890  3dvdsOLD  14891  divalgmod  14967  divalgmodOLD  14968  bitsmod  14996  bitsinv1lem  15001  bezoutlem4  15097  gcdzeq  15109  rplpwr  15114  sqgcd  15116  bezoutr  15119  rpmulgcd2  15208  rpdvds  15212  coprmproddvdslem  15214  isprm5  15257  divgcdodd  15260  divnumden  15294  crth  15321  phimullem  15322  modprm0  15348  modprmn0modprm0  15350  coprimeprodsq2  15352  pythagtriplem19  15376  pockthlem  15447  prmunb  15456  prmreclem3  15460  prmreclem6  15463  ramub  15555  ramz  15567  pmtrprfv  17696  pmtrprfv3  17697  mndodcong  17784  odngen  17815  pgpfi  17843  pgpssslw  17852  sylow2blem3  17860  lsmless1  17897  lsmless2  17898  lsmless12  17899  lsmmod2  17912  pj1id  17935  odadd2  18075  gexexlem  18078  ablfacrplem  18287  ablfacrp  18288  ablfac1b  18292  ablfac1eu  18295  pgpfac1lem2  18297  kerf1hrm  18566  lsmssspx  18909  lspsncv0  18967  coe1subfv  19457  coe1fzgsumdlem  19492  znunit  19731  uvcvvcl2  19946  uvcvv1  19947  uvcvv0  19948  scmate  20135  mdetunilem2  20238  pmatcoe1fsupp  20325  mat2pmatlin  20359  decpmatmullem  20395  pmatcollpw1lem1  20398  pmatcollpw1lem2  20399  pm2mpghm  20440  chpscmat  20466  chp0mat  20470  chpidmat  20471  cpmadugsumlemB  20498  cpmadugsumlemC  20499  cpmadugsumlemF  20500  clsndisj  20689  neiptopnei  20746  rnelfm  21567  fmfnfmlem2  21569  fmfnfm  21572  flimss1  21587  isfcf  21648  cnextfun  21678  cnextfvval  21679  cnextf  21680  cnextcn  21681  cnextfres1  21682  ustuqtop1  21855  utopsnneiplem  21861  xblss2ps  22016  xblss2  22017  stdbdxmet  22130  metcnpi3  22161  metustexhalf  22171  nmoi  22342  nmoi2  22344  nmoco  22351  blcvx  22409  icccmplem2  22434  icccmplem3  22435  reconnlem2  22438  xrge0gsumle  22444  metds0  22461  metdstri  22462  metdseq0  22465  lebnumlem3  22570  nmoleub2lem  22722  bcthlem5  22933  minveclem2  23005  minveclem3b  23007  minveclem4  23011  minveclem6  23013  icombl  23139  cncombf  23231  mbflimsup  23239  itg2monolem1  23323  itg2mono  23326  itg2cnlem1  23334  itg2cnlem2  23335  bddmulibl  23411  ellimc2  23447  cpnord  23504  cpnres  23506  dvmulbr  23508  dvcobr  23515  dvlipcn  23561  dvlip2  23562  c1liplem1  23563  dvivthlem1  23575  lhop1lem  23580  lhop1  23581  dvfsumlem2  23594  itgsubstlem  23615  deg1add  23667  deg1sublt  23674  ply1remlem  23726  plyeq0lem  23770  taylthlem2  23932  ulmdvlem3  23960  abelthlem7  23996  pilem2  24010  pilem3  24011  pige3  24073  logccv  24209  cxpaddlelem  24292  cvxcl  24511  fsumharmonic  24538  ftalem5  24603  dvdsmulf1o  24720  bposlem1  24809  lgsqr  24876  lgsquad2lem2  24910  2lgsoddprmlem1  24933  2sqlem8a  24950  2sqlem8  24951  dchrmusum2  24983  dchrvmasumiflem1  24990  dchrisum0flblem1  24997  dchrisum0lem1b  25004  pntlem3  25098  tgdim01  25202  axsegcon  25607  ax5seglem1  25608  ax5seglem2  25609  axlowdimlem6  25627  axeuclidlem  25642  axcontlem7  25650  axcontlem9  25652  axcontlem10  25653  cusgrasize2inds  26005  usgra2adedgspth  26141  vdgrun  26428  vdgrfiun  26429  vdgr1d  26430  vdgr1b  26431  vdgr1a  26433  2pthfrgra  26538  vdn1frgrav2  26552  vdgn1frgrav2  26553  frgrawopreg  26576  frrusgraord  26598  numclwwlk2lem1  26629  numclwwlk3  26636  frgrareg  26644  nmoub3i  27012  ubthlem3  27112  minvecolem2  27115  minvecolem4  27120  minvecolem5  27121  minvecolem6  27122  htthlem  27158  pjpjpre  27662  chscllem1  27880  chscllem2  27881  chscllem3  27882  cnlnadjlem2  28311  leopnmid  28381  br8d  28802  ogrpaddlt  29049  archirngz  29074  ornglmullt  29138  orngrmullt  29139  elrhmunit  29151  qqhval2lem  29353  qqhnm  29362  qqhucn  29364  esumcst  29452  esumpcvgval  29467  measunl  29606  dya2iocbrsiga  29664  dya2icobrsiga  29665  omssubadd  29689  inelcarsg  29700  carsgclctunlem2  29708  sibfof  29729  sitgaddlemb  29737  oddpwdc  29743  eulerpartlemgc  29751  bayesth  29828  erdszelem8  30434  br8  30899  matunitlindflem2  32576  totbndbnd  32758  prdsbnd  32762  rrncmslem  32801  rrntotbnd  32805  isdrngo2  32927  lsatcmp  33308  lcvexchlem2  33340  lcvexchlem3  33341  ncvr1  33577  cvrletrN  33578  cvrnbtwn3  33581  cvrnrefN  33587  cvrcmp  33588  0ltat  33596  atnle0  33614  atlen0  33615  cvlcvr1  33644  cvrval3  33717  atle  33740  athgt  33760  1cvratex  33777  ps-2  33782  ps-2b  33786  llnnleat  33817  2atneat  33819  llnle  33822  atcvrlln  33824  llncmp  33826  2llnmat  33828  2at0mat0  33829  2atm  33831  ps-2c  33832  lplnle  33844  lplnnle2at  33845  llncvrlpln2  33861  llncvrlpln  33862  2lplnmN  33863  2llnmj  33864  2atmat  33865  lplncmp  33866  lplnexllnN  33868  2llnm2N  33872  2llnm4  33874  lvolnle3at  33886  4atlem3a  33901  4atlem3b  33902  4atlem10  33910  4atlem11  33913  4atlem12  33916  lplncvrlvol2  33919  lplncvrlvol  33920  lvolcmp  33921  2lplnm2N  33925  2lplnmj  33926  dalempjsen  33957  dalemcea  33964  dalem2  33965  dalemdea  33966  dalem9  33976  dalem16  33983  dalemcjden  33996  dalem21  33998  dalem23  34000  dalem39  34015  dalem54  34030  dalem60  34036  cdlemb  34098  elpadd2at  34110  paddasslem4  34127  paddasslem7  34130  paddasslem15  34138  paddasslem16  34139  pmodlem1  34150  pmodlem2  34151  llnexchb2  34173  pclfinclN  34254  osumcllem9N  34268  pmapojoinN  34272  pexmidN  34273  pl42lem1N  34283  lhp0lt  34307  lhpexle1  34312  lhpexle2lem  34313  lhpexle3lem  34315  lhprelat3N  34344  ltrnid  34439  trlval3  34492  arglem1N  34495  cdlemc5  34500  cdleme3b  34534  cdleme3c  34535  cdleme3h  34540  cdleme7e  34552  cdleme7ga  34553  cdleme20l1  34626  cdleme20l2  34627  cdleme20l  34628  cdleme22b  34647  cdlemefrs29clN  34705  cdlemefrs32fva  34706  cdlemeg46fvcl  34812  cdlemeg46c  34819  cdlemeg46fvaw  34822  cdlemeg46req  34835  cdleme48fgv  34844  cdlemf1  34867  cdlemg1cex  34894  cdlemg2dN  34896  cdlemg2ce  34898  cdlemg12e  34953  cdlemg35  35019  cdlemh  35123  tendocan  35130  cdlemk28-3  35214  tendoex  35281  dih1  35593  dihmeetlem9N  35622  dihlspsnssN  35639  dihlspsnat  35640  lcfrlem23  35872  mzpsubst  36329  rencldnfi  36403  irrapx1  36410  pellexlem3  36413  pellexlem5  36415  infmrgelbi  36460  pellqrex  36461  pellfundge  36464  rmspecfund  36492  congtr  36550  acongeq  36568  jm2.20nn  36582  jm2.25lem1  36583  jm2.26  36587  expdiophlem1  36606  hbtlem2  36713  suprubd  37482  suprleubrd  37488  suprlubrd  37492  suprnmpt  38350  wessf1ornlem  38366  mpct  38388  upbdrech  38460  ssfiunibd  38464  uzfissfz  38483  xleadd2d  38484  suprltrp  38485  xleadd1d  38486  iccintsng  38596  limcrecl  38696  fnlimfvre  38741  dvmulcncf  38815  dvdivcncf  38817  dvbdfbdioolem1  38818  ioodvbdlimc1lem2  38822  ioodvbdlimc2lem  38824  stoweidlem1  38894  stoweidlem20  38913  stoweidlem24  38917  stoweidlem34  38927  stoweidlem45  38938  stoweidlem60  38953  fourierdlem20  39020  fourierdlem31  39031  fourierdlem38  39038  fourierdlem64  39063  fourierdlem79  39078  fourierdlem94  39093  fourierdlem113  39112  fouriersw  39124  fouriercn  39125  sge0isum  39320  hoicvr  39438  ovnsubaddlem2  39461  hoidmv1lelem1  39481  hoidmv1lelem3  39483  hoidmvlelem1  39485  hoidmvlelem4  39488  smflimlem2  39658  fmtnof1  39985  lighneallem2  40061  pfxfv  40262  nbupgr  40566  nbumgrvtx  40568  cusgrsize2inds  40669  upgr1wlkwlk  40847  2pthnloop  40937  frgrwopreg  41486  frrusgrord  41504  av-numclwwlk2lem1  41532  av-frgrareg  41548  lincresunit3  42064  elbigolo1  42149
  Copyright terms: Public domain W3C validator