Theorem syl31anc 1375

Description: Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.)

Hypotheses

Ref	Expression
syl3anc.1	⊢ (𝜑 → 𝜓)
syl3anc.2	⊢ (𝜑 → 𝜒)
syl3anc.3	⊢ (𝜑 → 𝜃)
syl3Xanc.4	⊢ (𝜑 → 𝜏)
syl31anc.5	⊢ (((𝜓 ∧ 𝜒 ∧ 𝜃) ∧ 𝜏) → 𝜂)

Assertion

Ref	Expression
syl31anc	⊢ (𝜑 → 𝜂)

Proof of Theorem syl31anc

Step	Hyp	Ref	Expression
1		syl3anc.1	. . 3 ⊢ (𝜑 → 𝜓)
2		syl3anc.2	. . 3 ⊢ (𝜑 → 𝜒)
3		syl3anc.3	. . 3 ⊢ (𝜑 → 𝜃)
4	1, 2, 3	3jca 1130	. 2 ⊢ (𝜑 → (𝜓 ∧ 𝜒 ∧ 𝜃))
5		syl3Xanc.4	. 2 ⊢ (𝜑 → 𝜏)
6		syl31anc.5	. 2 ⊢ (((𝜓 ∧ 𝜒 ∧ 𝜃) ∧ 𝜏) → 𝜂)
7	4, 5, 6	syl2anc 587	1 ⊢ (𝜑 → 𝜂)

Syntax hints:   → wi 4   ∧ wa 399   ∧ w3a 1089

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 210  df-an 400  df-3an 1091

This theorem is referenced by:  syl32anc  1380  stoic4b  1786  elovmpt3rab1  7465  smo11  8101  omeulem2  8311  oeeui  8330  oaabs2  8374  omabs  8376  omxpenlem  8746  map2xp  8816  mapdom2  8817  fsuppsssupp  9001  cantnflt  9287  cnfcom  9315  mapdjuen  9794  pwsdompw  9818  ackbij1lem5  9838  cofsmo  9883  fin1a2lem4  10017  ltmul12a  11688  lt2msq1  11716  ledivp1  11734  lemul1ad  11771  lemul2ad  11772  suprubd  11794  supaddc  11799  supadd  11800  supmul1  11801  supmul  11804  rpnnen1lem3  12575  rpnnen1lem5  12577  lediv2ad  12650  xaddge0  12848  xadddi  12885  xadddi2  12887  supicc  13089  supicclub  13091  difelfznle  13226  flval3  13390  expcan  13739  ltexp2  13740  ltexp2r  13743  expubnd  13747  ltexp2rd  13815  ltexp2d  13820  leexp2d  13821  expcand  13822  hashmap  14002  swrds1  14231  ccatswrd  14233  pfxfv  14247  swrdccatin1  14290  pfxccatin12lem3  14297  cshwidxmod  14368  wrdl3s3  14529  o1fsum  15377  mertenslem1  15448  eftlub  15670  rpnnen2lem4  15778  ruclem12  15802  dvdsadd  15863  3dvds  15892  divalgmod  15967  bitsmod  15995  bitsinv1lem  16000  bezoutlem4  16102  gcdzeq  16114  rplpwr  16119  sqgcd  16122  rpmulgcd2  16213  rpdvds  16217  coprmproddvdslem  16219  isprm5  16264  divgcdodd  16267  divnumden  16304  crth  16331  phimullem  16332  modprm0  16358  modprmn0modprm0  16360  coprimeprodsq2  16362  pythagtriplem19  16386  pockthlem  16458  prmunb  16467  prmreclem3  16471  prmreclem6  16474  ramub  16566  ramz  16578  pmtrprfv  18845  pmtrprfv3  18846  mndodcong  18934  odngen  18966  pgpfi  18994  sylow2blem3  19011  lsmless1  19049  lsmless2  19050  lsmless12  19051  lsmmod2  19066  pj1id  19089  odadd2  19234  gexexlem  19237  ablfacrplem  19452  ablfacrp  19453  ablfac1b  19457  ablfac1eu  19460  pgpfac1lem2  19462  kerf1ghm  19763  lsmssspx  20125  lspsncv0  20183  znunit  20528  uvcvvcl2  20750  uvcvv1  20751  uvcvv0  20752  coe1subfv  21187  coe1fzgsumdlem  21222  scmate  21407  mdetunilem2  21510  pmatcoe1fsupp  21598  mat2pmatlin  21632  decpmatmullem  21668  pmatcollpw1lem1  21671  pmatcollpw1lem2  21672  pm2mpghm  21713  chpscmat  21739  chp0mat  21743  chpidmat  21744  cpmadugsumlemB  21771  cpmadugsumlemC  21772  cpmadugsumlemF  21773  clsndisj  21972  neiptopnei  22029  rnelfm  22850  fmfnfmlem2  22852  fmfnfm  22855  flimss1  22870  isfcf  22931  cnextfun  22961  cnextfvval  22962  cnextf  22963  cnextcn  22964  cnextfres1  22965  ustuqtop1  23139  utopsnneiplem  23145  xblss2ps  23299  xblss2  23300  stdbdxmet  23413  metcnpi3  23444  metustexhalf  23454  nmoi  23626  nmoi2  23628  nmoco  23635  blcvx  23695  icccmplem2  23720  icccmplem3  23721  reconnlem2  23724  xrge0gsumle  23730  metds0  23747  metdstri  23748  metdseq0  23751  lebnumlem3  23860  nmoleub2lem  24011  bcthlem5  24225  csschl  24273  minveclem2  24323  minveclem3b  24325  minveclem4  24329  minveclem6  24331  icombl  24461  cncombf  24555  mbflimsup  24563  itg2monolem1  24648  itg2cnlem1  24659  itg2cnlem2  24660  bddmulibl  24736  ellimc2  24774  cpnord  24832  cpnres  24834  dvmulbr  24836  dvcobr  24843  dvlipcn  24891  dvlip2  24892  dvivthlem1  24905  lhop1lem  24910  lhop1  24911  dvfsumlem2  24924  itgsubstlem  24945  deg1add  25001  deg1sublt  25008  ply1remlem  25060  plyeq0lem  25104  taylthlem2  25266  ulmdvlem3  25294  abelthlem7  25330  pilem2  25344  pilem3  25345  pige3ALT  25409  logccv  25551  cxpaddlelem  25637  cvxcl  25867  fsumharmonic  25894  ftalem5  25959  dvdsmulf1o  26076  bposlem1  26165  lgsqr  26232  lgsquad2lem2  26266  2lgsoddprmlem1  26289  2sqlem8a  26306  2sqlem8  26307  dchrmusum2  26375  dchrvmasumiflem1  26382  dchrisum0flblem1  26389  dchrisum0lem1b  26396  pntlem3  26490  tgdim01  26598  axsegcon  27018  ax5seglem1  27019  ax5seglem2  27020  axlowdimlem6  27038  axeuclidlem  27053  axcontlem7  27061  axcontlem9  27063  axcontlem10  27064  nbupgr  27432  nbumgrvtx  27434  cusgrsize2inds  27541  upgriswlk  27728  2pthnloop  27818  numclwwlk2lem1  28459  frgrreg  28477  nmoub3i  28854  ubthlem3  28953  minvecolem2  28956  minvecolem4  28961  minvecolem5  28962  minvecolem6  28963  htthlem  28998  pjpjpre  29500  chscllem1  29718  chscllem2  29719  chscllem3  29720  cnlnadjlem2  30149  leopnmid  30219  br8d  30669  dvdszzq  30849  swrdf1  30948  splfv3  30950  ogrpaddlt  31062  symgcom2  31072  cyc3genpmlem  31137  archirngz  31162  ornglmullt  31225  orngrmullt  31226  elrhmunit  31238  elrspunidl  31320  qsidomlem1  31342  lssdimle  31405  dimkerim  31422  fedgmullem2  31425  fedgmul  31426  qqhval2lem  31643  qqhnm  31652  qqhucn  31654  esumcst  31743  esumpcvgval  31758  measunl  31896  dya2iocbrsiga  31954  dya2icobrsiga  31955  omssubadd  31979  inelcarsg  31990  carsgclctunlem2  31998  sibfof  32019  sitgaddlemb  32027  oddpwdc  32033  eulerpartlemgc  32041  bayesth  32118  ftc2re  32290  breprexplemc  32324  tgoldbachgt  32355  erdszelem8  32873  2goelgoanfmla1  33099  br8  33442  noetasuplem4  33676  noetainflem4  33680  noetalem1  33681  matunitlindflem2  35511  totbndbnd  35684  prdsbnd  35688  rrncmslem  35727  rrntotbnd  35731  isdrngo2  35853  lsatcmp  36754  lcvexchlem2  36786  lcvexchlem3  36787  ncvr1  37023  cvrletrN  37024  cvrnbtwn3  37027  cvrnrefN  37033  cvrcmp  37034  0ltat  37042  atnle0  37060  atlen0  37061  cvlcvr1  37090  cvrval3  37164  atle  37187  athgt  37207  1cvratex  37224  ps-2  37229  ps-2b  37233  llnnleat  37264  2atneat  37266  llnle  37269  atcvrlln  37271  llncmp  37273  2llnmat  37275  2at0mat0  37276  2atm  37278  ps-2c  37279  lplnle  37291  lplnnle2at  37292  llncvrlpln2  37308  llncvrlpln  37309  2lplnmN  37310  2llnmj  37311  2atmat  37312  lplncmp  37313  lplnexllnN  37315  2llnm2N  37319  2llnm4  37321  lvolnle3at  37333  4atlem3a  37348  4atlem3b  37349  4atlem10  37357  4atlem11  37360  4atlem12  37363  lplncvrlvol2  37366  lplncvrlvol  37367  lvolcmp  37368  2lplnm2N  37372  2lplnmj  37373  dalempjsen  37404  dalemcea  37411  dalem2  37412  dalemdea  37413  dalem9  37423  dalem16  37430  dalemcjden  37443  dalem21  37445  dalem23  37447  dalem39  37462  dalem54  37477  dalem60  37483  cdlemb  37545  elpadd2at  37557  paddasslem4  37574  paddasslem7  37577  paddasslem15  37585  paddasslem16  37586  pmodlem1  37597  pmodlem2  37598  llnexchb2  37620  pclfinclN  37701  osumcllem9N  37715  pmapojoinN  37719  pexmidN  37720  pl42lem1N  37730  lhp0lt  37754  lhpexle1  37759  lhpexle2lem  37760  lhpexle3lem  37762  lhprelat3N  37791  ltrnid  37886  trlval3  37938  arglem1N  37941  cdlemc5  37946  cdleme3b  37980  cdleme3c  37981  cdleme3h  37986  cdleme7e  37998  cdleme7ga  37999  cdleme20l1  38071  cdleme20l2  38072  cdleme20l  38073  cdleme22b  38092  cdlemefrs29clN  38150  cdlemefrs32fva  38151  cdlemeg46fvcl  38257  cdlemeg46c  38264  cdlemeg46fvaw  38267  cdlemeg46req  38280  cdleme48fgv  38289  cdlemf1  38312  cdlemg1cex  38339  cdlemg2dN  38341  cdlemg2ce  38343  cdlemg12e  38398  cdlemg35  38464  cdlemh  38568  tendocan  38575  cdlemk28-3  38659  tendoex  38726  dih1  39037  dihmeetlem9N  39066  dihlspsnssN  39083  dihlspsnat  39084  lcfrlem23  39316  3rspcedvdw  39904  fsuppind  39989  expgcd  40042  renegneg  40102  flt4lem4  40189  3cubes  40215  mzpsubst  40273  rencldnfi  40346  irrapx1  40353  pellexlem3  40356  pellexlem5  40358  infmrgelbi  40403  pellqrex  40404  pellfundge  40407  rmspecfund  40434  congtr  40490  acongeq  40508  jm2.20nn  40522  jm2.25lem1  40523  jm2.26  40527  expdiophlem1  40546  hbtlem2  40652  suprleubrd  41454  suprlubrd  41456  suprnmpt  42383  wessf1ornlem  42395  mpct  42414  upbdrech  42517  ssfiunibd  42521  uzfissfz  42538  xleadd2d  42539  suprltrp  42540  xleadd1d  42541  suprleubrnmpt  42635  iccintsng  42736  limcrecl  42845  fnlimfvre  42890  dvmulcncf  43141  dvdivcncf  43143  dvbdfbdioolem1  43144  ioodvbdlimc1lem2  43148  ioodvbdlimc2lem  43150  stoweidlem1  43217  stoweidlem20  43236  stoweidlem24  43240  stoweidlem34  43250  stoweidlem45  43261  stoweidlem60  43276  fourierdlem20  43343  fourierdlem31  43354  fourierdlem38  43361  fourierdlem64  43386  fourierdlem79  43401  fourierdlem94  43416  fourierdlem113  43435  fouriersw  43447  fouriercn  43448  sge0isum  43640  hoicvr  43761  ovnsubaddlem2  43784  hoidmv1lelem1  43804  hoidmv1lelem3  43806  hoidmvlelem1  43808  hoidmvlelem4  43811  smflimlem2  43979  fmtnof1  44660  lighneallem2  44731  upgrwlkupwlk  44975  lincresunit3  45495  elbigolo1  45576  eenglngeehlnm  45758