Theorem syl31anc 1400

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

Syntax hints:   → wi 4   ∧ wa 400   ∧ w3a 1103

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 401  df-3an 1105

This theorem is referenced by:  syl32anc  1405  stoic4b  1808  3rspcedvdw  3600  elovmpt3rab1  7672  smo11  8352  omeulem2  8569  oeeui  8589  oaabs2  8636  omabs  8638  omxpenlem  9067  map2xp  9136  mapdom2  9137  fsuppsssupp  9342  cantnflt  9642  cnfcom  9670  mapdjuen  10165  pwsdompw  10187  ackbij1lem5  10207  cofsmo  10254  fin1a2lem4  10388  ltmul12a  12072  lt2msq1  12100  ledivp1  12118  lemul1ad  12155  lemul2ad  12156  suprubd  12178  supaddc  12183  supadd  12184  supmul1  12185  supmul  12188  rpnnen1lem3  13004  rpnnen1lem5  13006  lediv2ad  13083  xaddge0  13285  xadddi  13322  xadddi2  13324  supicc  13529  supicclub  13531  difelfznle  13672  flval3  13850  expcan  14207  ltexp2  14208  ltexp2r  14211  expubnd  14216  ltexp2rd  14286  ltexp2d  14289  leexp2d  14290  expcand  14291  hashmap  14474  swrds1  14706  ccatswrd  14708  pfxfv  14722  swrdccatin1  14764  pfxccatin12lem3  14771  cshwidxmod  14842  wrdl3s3  15001  o1fsum  15867  mertenslem1  15940  eftlub  16166  rpnnen2lem4  16274  ruclem12  16298  dvdsadd  16361  3dvds  16390  divalgmod  16465  bitsmod  16495  bitsinv1lem  16500  bezoutlem4  16601  gcdzeq  16611  rplpwr  16617  sqgcd  16621  expgcd  16622  rpmulgcd2  16715  rpdvds  16719  coprmproddvdslem  16721  isprm5  16767  divgcdodd  16770  dvdszzq  16781  divnumden  16808  crth  16838  phimullem  16839  modprm0  16866  modprmn0modprm0  16868  coprimeprodsq2  16870  pythagtriplem19  16894  pockthlem  16966  prmunb  16975  prmreclem3  16979  prmreclem6  16982  ramub  17074  ramz  17086  kerf1ghm  19318  pmtrprfv  19524  pmtrprfv3  19525  mndodcong  19613  odngen  19648  pgpfi  19676  sylow2blem3  19693  lsmless1  19731  lsmless2  19732  lsmless12  19733  lsmmod2  19747  pj1id  19770  odadd2  19920  gexexlem  19923  ablfacrplem  20138  ablfacrp  20139  ablfac1b  20143  ablfac1eu  20146  pgpfac1lem2  20148  ogrpaddlt  20209  elrhmunit  20594  rrgnz  20790  ornglmullt  20953  orngrmullt  20954  lsmssspx  21190  lspsncv0  21251  qsidomlem1  21461  ssdifidlprm  21467  znunit  21694  uvcvvcl2  21919  uvcvv1  21920  uvcvv0  21921  coe1subfv  22408  coe1fzgsumdlem  22444  scmate  22648  mdetunilem2  22751  pmatcoe1fsupp  22839  mat2pmatlin  22873  decpmatmullem  22909  pmatcollpw1lem1  22912  pmatcollpw1lem2  22913  pm2mpghm  22954  chpscmat  22980  chp0mat  22984  chpidmat  22985  cpmadugsumlemB  23012  cpmadugsumlemC  23013  cpmadugsumlemF  23014  clsndisj  23213  neiptopnei  23270  rnelfm  24091  fmfnfmlem2  24093  fmfnfm  24096  flimss1  24111  isfcf  24172  cnextfun  24202  cnextfvval  24203  cnextf  24204  cnextcn  24205  cnextfres1  24206  ustuqtop1  24379  utopsnneiplem  24385  xblss2ps  24539  xblss2  24540  stdbdxmet  24653  metcnpi3  24684  metustexhalf  24694  nmoi  24866  nmoi2  24868  nmoco  24875  blcvx  24936  icccmplem2  24962  icccmplem3  24963  reconnlem2  24966  xrge0gsumle  24972  metds0  24989  metdstri  24990  metdseq0  24993  lebnumlem3  25103  nmoleub2lem  25254  bcthlem5  25468  csschl  25516  minveclem2  25566  minveclem3b  25568  minveclem4  25572  minveclem6  25574  icombl  25704  cncombf  25798  mbflimsup  25806  itg2monolem1  25890  itg2cnlem1  25901  itg2cnlem2  25902  bddmulibl  25979  ellimc2  26017  cpnord  26075  cpnres  26077  dvmulbr  26079  dvcobr  26086  dvlipcn  26134  dvlip2  26135  dvivthlem1  26148  lhop1lem  26153  lhop1  26154  dvfsumlem2  26167  itgsubstlem  26188  deg1add  26241  deg1sublt  26248  ply1remlem  26303  plyeq0lem  26348  taylthlem2  26518  ulmdvlem3  26546  abelthlem7  26582  pilem2  26596  pilem3  26597  pige3ALT  26666  logccv  26809  cxpaddlelem  26897  cvxcl  27130  fsumharmonic  27157  ftalem5  27222  mpodvdsmulf1o  27339  dvdsmulf1o  27341  bposlem1  27429  lgsqr  27496  lgsquad2lem2  27530  2lgsoddprmlem1  27553  2sqlem8a  27570  2sqlem8  27571  dchrmusum2  27639  dchrvmasumiflem1  27646  dchrisum0flblem1  27653  dchrisum0lem1b  27660  pntlem3  27754  noetasuplem4  27881  noetainflem4  27885  noetalem1  27886  divmulswd  28368  divsclwd  28370  uzsind  28579  tgdim01  28757  axsegcon  29258  ax5seglem1  29259  ax5seglem2  29260  axlowdimlem6  29278  axeuclidlem  29293  axcontlem7  29301  axcontlem9  29303  axcontlem10  29304  nbupgr  29675  nbumgrvtx  29677  cusgrsize2inds  29784  upgriswlk  29971  2pthnloop  30061  numclwwlk2lem1  30708  frgrreg  30726  nmoub3i  31106  ubthlem3  31205  minvecolem2  31208  minvecolem4  31213  minvecolem5  31214  minvecolem6  31215  htthlem  31250  pjpjpre  31752  chscllem1  31970  chscllem2  31971  chscllem3  31972  cnlnadjlem2  32401  leopnmid  32471  tpssad  32866  br8d  32934  swrdf1  33257  splfv3  33259  symgcom2  33385  cyc3genpmlem  33452  archirngz  33490  elrgspnlem1  33543  erld2  33567  rlocf1  33575  subrdom  33586  ricdomn1  33590  dvdsruasso  33679  unitpidl1  33713  elrspunidl  33717  mxidlirredi  33735  dflringlem2  33766  1arithidomlem2  33807  1arithidom  33808  1arithufdlem3  33817  ply1gsumz  33870  mplidomlem  33898  esplymhp  33939  esplyfvaln  33945  vietadeg1  33949  lssdimle  33979  dimkerim  33998  fedgmullem2  34001  fedgmul  34002  assalactf1o  34006  fldextrspundglemul  34050  fldextrspundgdvds  34052  minplyirred  34082  irredminply  34087  algextdeglem2  34089  rtelextdg2lem  34097  constrext2chnlem  34121  constrresqrtcl  34148  2sqr3minply  34151  cos9thpiminplylem2  34154  cos9thpiminply  34159  qqhval2lem  34352  qqhnm  34361  qqhucn  34363  esumcst  34434  esumpcvgval  34449  measunl  34587  dya2iocbrsiga  34646  dya2icobrsiga  34647  omssubadd  34671  inelcarsg  34682  carsgclctunlem2  34690  sibfof  34711  sitgaddlemb  34719  oddpwdc  34725  eulerpartlemgc  34733  bayesth  34810  ftc2re  34966  breprexplemc  35000  tgoldbachgt  35031  erdszelem8  35671  2goelgoanfmla1  35897  br8  36229  matunitlindflem2  38249  totbndbnd  38421  prdsbnd  38425  rrncmslem  38464  rrntotbnd  38468  isdrngo2  38590  lsatcmp  39758  lcvexchlem2  39790  lcvexchlem3  39791  ncvr1  40027  cvrletrN  40028  cvrnbtwn3  40031  cvrnrefN  40037  cvrcmp  40038  0ltat  40046  atnle0  40064  atlen0  40065  cvlcvr1  40094  cvrval3  40168  atle  40191  athgt  40211  1cvratex  40228  ps-2  40233  ps-2b  40237  llnnleat  40268  2atneat  40270  llnle  40273  atcvrlln  40275  llncmp  40277  2llnmat  40279  2at0mat0  40280  2atm  40282  ps-2c  40283  lplnle  40295  lplnnle2at  40296  llncvrlpln2  40312  llncvrlpln  40313  2lplnmN  40314  2llnmj  40315  2atmat  40316  lplncmp  40317  lplnexllnN  40319  2llnm2N  40323  2llnm4  40325  lvolnle3at  40337  4atlem3a  40352  4atlem3b  40353  4atlem10  40361  4atlem11  40364  4atlem12  40367  lplncvrlvol2  40370  lplncvrlvol  40371  lvolcmp  40372  2lplnm2N  40376  2lplnmj  40377  dalempjsen  40408  dalemcea  40415  dalem2  40416  dalemdea  40417  dalem9  40427  dalem16  40434  dalemcjden  40447  dalem21  40449  dalem23  40451  dalem39  40466  dalem54  40481  dalem60  40487  cdlemb  40549  elpadd2at  40561  paddasslem4  40578  paddasslem7  40581  paddasslem15  40589  paddasslem16  40590  pmodlem1  40601  pmodlem2  40602  llnexchb2  40624  pclfinclN  40705  osumcllem9N  40719  pmapojoinN  40723  pexmidN  40724  pl42lem1N  40734  lhp0lt  40758  lhpexle1  40763  lhpexle2lem  40764  lhpexle3lem  40766  lhprelat3N  40795  ltrnid  40890  trlval3  40942  arglem1N  40945  cdlemc5  40950  cdleme3b  40984  cdleme3c  40985  cdleme3h  40990  cdleme7e  41002  cdleme7ga  41003  cdleme20l1  41075  cdleme20l2  41076  cdleme20l  41077  cdleme22b  41096  cdlemefrs29clN  41154  cdlemefrs32fva  41155  cdlemeg46fvcl  41261  cdlemeg46c  41268  cdlemeg46fvaw  41271  cdlemeg46req  41284  cdleme48fgv  41293  cdlemf1  41316  cdlemg1cex  41343  cdlemg2dN  41345  cdlemg2ce  41347  cdlemg12e  41402  cdlemg35  41468  cdlemh  41572  tendocan  41579  cdlemk28-3  41663  tendoex  41730  dih1  42041  dihmeetlem9N  42070  dihlspsnssN  42087  dihlspsnat  42088  lcfrlem23  42320  renegneg  43154  fsuppind  43305  flt4lem4  43364  3cubes  43404  mzpsubst  43462  rencldnfi  43531  irrapx1  43538  pellexlem3  43541  pellexlem5  43543  infmrgelbi  43588  pellqrex  43589  pellfundge  43592  rmspecfund  43619  congtr  43675  acongeq  43693  jm2.20nn  43707  jm2.25lem1  43708  jm2.26  43712  expdiophlem1  43731  hbtlem2  43834  cantnftermord  44030  suprleubrd  44875  suprlubrd  44877  suprnmpt  45875  wessf1ornlem  45886  mpct  45901  upbdrech  46007  ssfiunibd  46011  uzfissfz  46025  xleadd2d  46026  suprltrp  46027  xleadd1d  46028  suprleubrnmpt  46119  iccintsng  46222  limcrecl  46328  fnlimfvre  46371  dvmulcncf  46622  dvdivcncf  46624  dvbdfbdioolem1  46625  ioodvbdlimc1lem2  46629  ioodvbdlimc2lem  46631  stoweidlem1  46698  stoweidlem20  46717  stoweidlem24  46721  stoweidlem34  46731  stoweidlem45  46742  stoweidlem60  46757  fourierdlem20  46824  fourierdlem31  46835  fourierdlem38  46842  fourierdlem64  46867  fourierdlem79  46882  fourierdlem94  46897  fourierdlem113  46916  fouriersw  46928  fouriercn  46929  sge0isum  47124  hoicvr  47245  ovnsubaddlem2  47268  hoidmv1lelem1  47288  hoidmv1lelem3  47290  hoidmvlelem1  47292  hoidmvlelem4  47295  smflimlem2  47469  2timesltsq  48098  fmtnof1  48270  lighneallem2  48341  uspgrlim  48740  upgrwlkupwlk  48888  lincresunit3  49244  elbigolo1  49320  eenglngeehlnm  49502