Theorem syl31anc 1373

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 1128	. 2 ⊢ (𝜑 → (𝜓 ∧ 𝜒 ∧ 𝜃))
5		syl3Xanc.4	. 2 ⊢ (𝜑 → 𝜏)
6		syl31anc.5	. 2 ⊢ (((𝜓 ∧ 𝜒 ∧ 𝜃) ∧ 𝜏) → 𝜂)
7	4, 5, 6	syl2anc 583	1 ⊢ (𝜑 → 𝜂)

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1087

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 207  df-an 396  df-3an 1089

This theorem is referenced by:  syl32anc  1378  stoic4b  1776  3rspcedvdw  3653  elovmpt3rab1  7710  smo11  8420  omeulem2  8639  oeeui  8658  oaabs2  8705  omabs  8707  omxpenlem  9139  map2xp  9213  mapdom2  9214  fsuppsssupp  9450  cantnflt  9741  cnfcom  9769  mapdjuen  10250  pwsdompw  10272  ackbij1lem5  10292  cofsmo  10338  fin1a2lem4  10472  ltmul12a  12150  lt2msq1  12179  ledivp1  12197  lemul1ad  12234  lemul2ad  12235  suprubd  12257  supaddc  12262  supadd  12263  supmul1  12264  supmul  12267  rpnnen1lem3  13044  rpnnen1lem5  13046  lediv2ad  13121  xaddge0  13320  xadddi  13357  xadddi2  13359  supicc  13561  supicclub  13563  difelfznle  13699  flval3  13866  expcan  14219  ltexp2  14220  ltexp2r  14223  expubnd  14227  ltexp2rd  14297  ltexp2d  14300  leexp2d  14301  expcand  14302  hashmap  14484  swrds1  14714  ccatswrd  14716  pfxfv  14730  swrdccatin1  14773  pfxccatin12lem3  14780  cshwidxmod  14851  wrdl3s3  15011  o1fsum  15861  mertenslem1  15932  eftlub  16157  rpnnen2lem4  16265  ruclem12  16289  dvdsadd  16350  3dvds  16379  divalgmod  16454  bitsmod  16482  bitsinv1lem  16487  bezoutlem4  16589  gcdzeq  16599  rplpwr  16605  sqgcd  16609  expgcd  16610  rpmulgcd2  16703  rpdvds  16707  coprmproddvdslem  16709  isprm5  16754  divgcdodd  16757  dvdszzq  16768  divnumden  16795  crth  16825  phimullem  16826  modprm0  16852  modprmn0modprm0  16854  coprimeprodsq2  16856  pythagtriplem19  16880  pockthlem  16952  prmunb  16961  prmreclem3  16965  prmreclem6  16968  ramub  17060  ramz  17072  kerf1ghm  19287  pmtrprfv  19495  pmtrprfv3  19496  mndodcong  19584  odngen  19619  pgpfi  19647  sylow2blem3  19664  lsmless1  19702  lsmless2  19703  lsmless12  19704  lsmmod2  19718  pj1id  19741  odadd2  19891  gexexlem  19894  ablfacrplem  20109  ablfacrp  20110  ablfac1b  20114  ablfac1eu  20117  pgpfac1lem2  20119  elrhmunit  20536  rrgnz  20726  lsmssspx  21110  lspsncv0  21171  znunit  21605  uvcvvcl2  21831  uvcvv1  21832  uvcvv0  21833  coe1subfv  22290  coe1fzgsumdlem  22328  scmate  22537  mdetunilem2  22640  pmatcoe1fsupp  22728  mat2pmatlin  22762  decpmatmullem  22798  pmatcollpw1lem1  22801  pmatcollpw1lem2  22802  pm2mpghm  22843  chpscmat  22869  chp0mat  22873  chpidmat  22874  cpmadugsumlemB  22901  cpmadugsumlemC  22902  cpmadugsumlemF  22903  clsndisj  23104  neiptopnei  23161  rnelfm  23982  fmfnfmlem2  23984  fmfnfm  23987  flimss1  24002  isfcf  24063  cnextfun  24093  cnextfvval  24094  cnextf  24095  cnextcn  24096  cnextfres1  24097  ustuqtop1  24271  utopsnneiplem  24277  xblss2ps  24432  xblss2  24433  stdbdxmet  24549  metcnpi3  24580  metustexhalf  24590  nmoi  24770  nmoi2  24772  nmoco  24779  blcvx  24839  icccmplem2  24864  icccmplem3  24865  reconnlem2  24868  xrge0gsumle  24874  metds0  24891  metdstri  24892  metdseq0  24895  lebnumlem3  25014  nmoleub2lem  25166  bcthlem5  25381  csschl  25429  minveclem2  25479  minveclem3b  25481  minveclem4  25485  minveclem6  25487  icombl  25618  cncombf  25712  mbflimsup  25720  itg2monolem1  25805  itg2cnlem1  25816  itg2cnlem2  25817  bddmulibl  25894  ellimc2  25932  cpnord  25991  cpnres  25993  dvmulbr  25995  dvmulbrOLD  25996  dvcobr  26003  dvcobrOLD  26004  dvlipcn  26053  dvlip2  26054  dvivthlem1  26067  lhop1lem  26072  lhop1  26073  dvfsumlem2  26087  dvfsumlem2OLD  26088  itgsubstlem  26109  deg1add  26162  deg1sublt  26169  ply1remlem  26224  plyeq0lem  26269  taylthlem2  26434  taylthlem2OLD  26435  ulmdvlem3  26463  abelthlem7  26500  pilem2  26514  pilem3  26515  pige3ALT  26580  logccv  26723  cxpaddlelem  26812  cvxcl  27046  fsumharmonic  27073  ftalem5  27138  mpodvdsmulf1o  27255  dvdsmulf1o  27257  bposlem1  27346  lgsqr  27413  lgsquad2lem2  27447  2lgsoddprmlem1  27470  2sqlem8a  27487  2sqlem8  27488  dchrmusum2  27556  dchrvmasumiflem1  27563  dchrisum0flblem1  27570  dchrisum0lem1b  27577  pntlem3  27671  noetasuplem4  27799  noetainflem4  27803  noetalem1  27804  divsmulwd  28237  divsclwd  28239  uzsind  28409  tgdim01  28533  axsegcon  28960  ax5seglem1  28961  ax5seglem2  28962  axlowdimlem6  28980  axeuclidlem  28995  axcontlem7  29003  axcontlem9  29005  axcontlem10  29006  nbupgr  29379  nbumgrvtx  29381  cusgrsize2inds  29489  upgriswlk  29677  2pthnloop  29767  numclwwlk2lem1  30408  frgrreg  30426  nmoub3i  30805  ubthlem3  30904  minvecolem2  30907  minvecolem4  30912  minvecolem5  30913  minvecolem6  30914  htthlem  30949  pjpjpre  31451  chscllem1  31669  chscllem2  31670  chscllem3  31671  cnlnadjlem2  32100  leopnmid  32170  br8d  32632  swrdf1  32923  splfv3  32925  ogrpaddlt  33067  symgcom2  33077  cyc3genpmlem  33144  archirngz  33169  rlocf1  33245  subrdom  33254  ornglmullt  33302  orngrmullt  33303  dvdsruasso  33378  unitpidl1  33417  elrspunidl  33421  qsidomlem1  33445  ssdifidlprm  33451  mxidlirredi  33464  1arithidomlem2  33529  1arithidom  33530  1arithufdlem3  33539  ply1gsumz  33584  lssdimle  33620  dimkerim  33640  fedgmullem2  33643  fedgmul  33644  assalactf1o  33648  minplyirred  33704  irredminply  33707  algextdeglem2  33709  rtelextdg2lem  33717  2sqr3minply  33738  qqhval2lem  33927  qqhnm  33936  qqhucn  33938  esumcst  34027  esumpcvgval  34042  measunl  34180  dya2iocbrsiga  34240  dya2icobrsiga  34241  omssubadd  34265  inelcarsg  34276  carsgclctunlem2  34284  sibfof  34305  sitgaddlemb  34313  oddpwdc  34319  eulerpartlemgc  34327  bayesth  34404  ftc2re  34575  breprexplemc  34609  tgoldbachgt  34640  erdszelem8  35166  2goelgoanfmla1  35392  br8  35718  matunitlindflem2  37577  totbndbnd  37749  prdsbnd  37753  rrncmslem  37792  rrntotbnd  37796  isdrngo2  37918  lsatcmp  38959  lcvexchlem2  38991  lcvexchlem3  38992  ncvr1  39228  cvrletrN  39229  cvrnbtwn3  39232  cvrnrefN  39238  cvrcmp  39239  0ltat  39247  atnle0  39265  atlen0  39266  cvlcvr1  39295  cvrval3  39370  atle  39393  athgt  39413  1cvratex  39430  ps-2  39435  ps-2b  39439  llnnleat  39470  2atneat  39472  llnle  39475  atcvrlln  39477  llncmp  39479  2llnmat  39481  2at0mat0  39482  2atm  39484  ps-2c  39485  lplnle  39497  lplnnle2at  39498  llncvrlpln2  39514  llncvrlpln  39515  2lplnmN  39516  2llnmj  39517  2atmat  39518  lplncmp  39519  lplnexllnN  39521  2llnm2N  39525  2llnm4  39527  lvolnle3at  39539  4atlem3a  39554  4atlem3b  39555  4atlem10  39563  4atlem11  39566  4atlem12  39569  lplncvrlvol2  39572  lplncvrlvol  39573  lvolcmp  39574  2lplnm2N  39578  2lplnmj  39579  dalempjsen  39610  dalemcea  39617  dalem2  39618  dalemdea  39619  dalem9  39629  dalem16  39636  dalemcjden  39649  dalem21  39651  dalem23  39653  dalem39  39668  dalem54  39683  dalem60  39689  cdlemb  39751  elpadd2at  39763  paddasslem4  39780  paddasslem7  39783  paddasslem15  39791  paddasslem16  39792  pmodlem1  39803  pmodlem2  39804  llnexchb2  39826  pclfinclN  39907  osumcllem9N  39921  pmapojoinN  39925  pexmidN  39926  pl42lem1N  39936  lhp0lt  39960  lhpexle1  39965  lhpexle2lem  39966  lhpexle3lem  39968  lhprelat3N  39997  ltrnid  40092  trlval3  40144  arglem1N  40147  cdlemc5  40152  cdleme3b  40186  cdleme3c  40187  cdleme3h  40192  cdleme7e  40204  cdleme7ga  40205  cdleme20l1  40277  cdleme20l2  40278  cdleme20l  40279  cdleme22b  40298  cdlemefrs29clN  40356  cdlemefrs32fva  40357  cdlemeg46fvcl  40463  cdlemeg46c  40470  cdlemeg46fvaw  40473  cdlemeg46req  40486  cdleme48fgv  40495  cdlemf1  40518  cdlemg1cex  40545  cdlemg2dN  40547  cdlemg2ce  40549  cdlemg12e  40604  cdlemg35  40670  cdlemh  40774  tendocan  40781  cdlemk28-3  40865  tendoex  40932  dih1  41243  dihmeetlem9N  41272  dihlspsnssN  41289  dihlspsnat  41290  lcfrlem23  41522  renegneg  42387  fsuppind  42545  flt4lem4  42604  3cubes  42646  mzpsubst  42704  rencldnfi  42777  irrapx1  42784  pellexlem3  42787  pellexlem5  42789  infmrgelbi  42834  pellqrex  42835  pellfundge  42838  rmspecfund  42865  congtr  42922  acongeq  42940  jm2.20nn  42954  jm2.25lem1  42955  jm2.26  42959  expdiophlem1  42978  hbtlem2  43081  cantnftermord  43282  suprleubrd  44128  suprlubrd  44130  suprnmpt  45081  wessf1ornlem  45092  mpct  45108  upbdrech  45220  ssfiunibd  45224  uzfissfz  45241  xleadd2d  45242  suprltrp  45243  xleadd1d  45244  suprleubrnmpt  45337  iccintsng  45441  limcrecl  45550  fnlimfvre  45595  dvmulcncf  45846  dvdivcncf  45848  dvbdfbdioolem1  45849  ioodvbdlimc1lem2  45853  ioodvbdlimc2lem  45855  stoweidlem1  45922  stoweidlem20  45941  stoweidlem24  45945  stoweidlem34  45955  stoweidlem45  45966  stoweidlem60  45981  fourierdlem20  46048  fourierdlem31  46059  fourierdlem38  46066  fourierdlem64  46091  fourierdlem79  46106  fourierdlem94  46121  fourierdlem113  46140  fouriersw  46152  fouriercn  46153  sge0isum  46348  hoicvr  46469  ovnsubaddlem2  46492  hoidmv1lelem1  46512  hoidmv1lelem3  46514  hoidmvlelem1  46516  hoidmvlelem4  46519  smflimlem2  46693  fmtnof1  47409  lighneallem2  47480  uspgrlim  47816  upgrwlkupwlk  47863  lincresunit3  48210  elbigolo1  48291  eenglngeehlnm  48473