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

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

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 1088

This theorem is referenced by:  syl32anc  1380  stoic4b  1779  3rspcedvdw  3594  elovmpt3rab1  7618  smo11  8296  omeulem2  8510  oeeui  8530  oaabs2  8577  omabs  8579  omxpenlem  9006  map2xp  9075  mapdom2  9076  fsuppsssupp  9284  cantnflt  9581  cnfcom  9609  mapdjuen  10091  pwsdompw  10113  ackbij1lem5  10133  cofsmo  10179  fin1a2lem4  10313  ltmul12a  11997  lt2msq1  12026  ledivp1  12044  lemul1ad  12081  lemul2ad  12082  suprubd  12104  supaddc  12109  supadd  12110  supmul1  12111  supmul  12114  rpnnen1lem3  12892  rpnnen1lem5  12894  lediv2ad  12971  xaddge0  13173  xadddi  13210  xadddi2  13212  supicc  13417  supicclub  13419  difelfznle  13558  flval3  13735  expcan  14092  ltexp2  14093  ltexp2r  14096  expubnd  14101  ltexp2rd  14171  ltexp2d  14174  leexp2d  14175  expcand  14176  hashmap  14358  swrds1  14590  ccatswrd  14592  pfxfv  14606  swrdccatin1  14648  pfxccatin12lem3  14655  cshwidxmod  14726  wrdl3s3  14885  o1fsum  15736  mertenslem1  15807  eftlub  16034  rpnnen2lem4  16142  ruclem12  16166  dvdsadd  16229  3dvds  16258  divalgmod  16333  bitsmod  16363  bitsinv1lem  16368  bezoutlem4  16469  gcdzeq  16479  rplpwr  16485  sqgcd  16489  expgcd  16490  rpmulgcd2  16583  rpdvds  16587  coprmproddvdslem  16589  isprm5  16634  divgcdodd  16637  dvdszzq  16648  divnumden  16675  crth  16705  phimullem  16706  modprm0  16733  modprmn0modprm0  16735  coprimeprodsq2  16737  pythagtriplem19  16761  pockthlem  16833  prmunb  16842  prmreclem3  16846  prmreclem6  16849  ramub  16941  ramz  16953  kerf1ghm  19176  pmtrprfv  19382  pmtrprfv3  19383  mndodcong  19471  odngen  19506  pgpfi  19534  sylow2blem3  19551  lsmless1  19589  lsmless2  19590  lsmless12  19591  lsmmod2  19605  pj1id  19628  odadd2  19778  gexexlem  19781  ablfacrplem  19996  ablfacrp  19997  ablfac1b  20001  ablfac1eu  20004  pgpfac1lem2  20006  ogrpaddlt  20067  elrhmunit  20443  rrgnz  20637  ornglmullt  20802  orngrmullt  20803  lsmssspx  21040  lspsncv0  21101  znunit  21518  uvcvvcl2  21743  uvcvv1  21744  uvcvv0  21745  coe1subfv  22208  coe1fzgsumdlem  22247  scmate  22454  mdetunilem2  22557  pmatcoe1fsupp  22645  mat2pmatlin  22679  decpmatmullem  22715  pmatcollpw1lem1  22718  pmatcollpw1lem2  22719  pm2mpghm  22760  chpscmat  22786  chp0mat  22790  chpidmat  22791  cpmadugsumlemB  22818  cpmadugsumlemC  22819  cpmadugsumlemF  22820  clsndisj  23019  neiptopnei  23076  rnelfm  23897  fmfnfmlem2  23899  fmfnfm  23902  flimss1  23917  isfcf  23978  cnextfun  24008  cnextfvval  24009  cnextf  24010  cnextcn  24011  cnextfres1  24012  ustuqtop1  24185  utopsnneiplem  24191  xblss2ps  24345  xblss2  24346  stdbdxmet  24459  metcnpi3  24490  metustexhalf  24500  nmoi  24672  nmoi2  24674  nmoco  24681  blcvx  24742  icccmplem2  24768  icccmplem3  24769  reconnlem2  24772  xrge0gsumle  24778  metds0  24795  metdstri  24796  metdseq0  24799  lebnumlem3  24918  nmoleub2lem  25070  bcthlem5  25284  csschl  25332  minveclem2  25382  minveclem3b  25384  minveclem4  25388  minveclem6  25390  icombl  25521  cncombf  25615  mbflimsup  25623  itg2monolem1  25707  itg2cnlem1  25718  itg2cnlem2  25719  bddmulibl  25796  ellimc2  25834  cpnord  25893  cpnres  25895  dvmulbr  25897  dvmulbrOLD  25898  dvcobr  25905  dvcobrOLD  25906  dvlipcn  25955  dvlip2  25956  dvivthlem1  25969  lhop1lem  25974  lhop1  25975  dvfsumlem2  25989  dvfsumlem2OLD  25990  itgsubstlem  26011  deg1add  26064  deg1sublt  26071  ply1remlem  26126  plyeq0lem  26171  taylthlem2  26338  taylthlem2OLD  26339  ulmdvlem3  26367  abelthlem7  26404  pilem2  26418  pilem3  26419  pige3ALT  26485  logccv  26628  cxpaddlelem  26717  cvxcl  26951  fsumharmonic  26978  ftalem5  27043  mpodvdsmulf1o  27160  dvdsmulf1o  27162  bposlem1  27251  lgsqr  27318  lgsquad2lem2  27352  2lgsoddprmlem1  27375  2sqlem8a  27392  2sqlem8  27393  dchrmusum2  27461  dchrvmasumiflem1  27468  dchrisum0flblem1  27475  dchrisum0lem1b  27482  pntlem3  27576  noetasuplem4  27704  noetainflem4  27708  noetalem1  27709  divmulswd  28190  divsclwd  28192  uzsind  28401  tgdim01  28579  axsegcon  29000  ax5seglem1  29001  ax5seglem2  29002  axlowdimlem6  29020  axeuclidlem  29035  axcontlem7  29043  axcontlem9  29045  axcontlem10  29046  nbupgr  29417  nbumgrvtx  29419  cusgrsize2inds  29527  upgriswlk  29714  2pthnloop  29804  numclwwlk2lem1  30451  frgrreg  30469  nmoub3i  30848  ubthlem3  30947  minvecolem2  30950  minvecolem4  30955  minvecolem5  30956  minvecolem6  30957  htthlem  30992  pjpjpre  31494  chscllem1  31712  chscllem2  31713  chscllem3  31714  cnlnadjlem2  32143  leopnmid  32213  tpssad  32614  br8d  32686  swrdf1  33038  splfv3  33040  symgcom2  33166  cyc3genpmlem  33233  archirngz  33271  elrgspnlem1  33324  rlocf1  33355  subrdom  33367  dvdsruasso  33466  unitpidl1  33505  elrspunidl  33509  qsidomlem1  33533  ssdifidlprm  33539  mxidlirredi  33552  1arithidomlem2  33617  1arithidom  33618  1arithufdlem3  33627  ply1gsumz  33680  esplymhp  33726  vietadeg1  33734  lssdimle  33764  dimkerim  33784  fedgmullem2  33787  fedgmul  33788  assalactf1o  33792  fldextrspundglemul  33836  fldextrspundgdvds  33838  minplyirred  33868  irredminply  33873  algextdeglem2  33875  rtelextdg2lem  33883  constrext2chnlem  33907  constrresqrtcl  33934  2sqr3minply  33937  cos9thpiminplylem2  33940  cos9thpiminply  33945  qqhval2lem  34138  qqhnm  34147  qqhucn  34149  esumcst  34220  esumpcvgval  34235  measunl  34373  dya2iocbrsiga  34432  dya2icobrsiga  34433  omssubadd  34457  inelcarsg  34468  carsgclctunlem2  34476  sibfof  34497  sitgaddlemb  34505  oddpwdc  34511  eulerpartlemgc  34519  bayesth  34596  ftc2re  34755  breprexplemc  34789  tgoldbachgt  34820  erdszelem8  35392  2goelgoanfmla1  35618  br8  35950  matunitlindflem2  37814  totbndbnd  37986  prdsbnd  37990  rrncmslem  38029  rrntotbnd  38033  isdrngo2  38155  lsatcmp  39259  lcvexchlem2  39291  lcvexchlem3  39292  ncvr1  39528  cvrletrN  39529  cvrnbtwn3  39532  cvrnrefN  39538  cvrcmp  39539  0ltat  39547  atnle0  39565  atlen0  39566  cvlcvr1  39595  cvrval3  39669  atle  39692  athgt  39712  1cvratex  39729  ps-2  39734  ps-2b  39738  llnnleat  39769  2atneat  39771  llnle  39774  atcvrlln  39776  llncmp  39778  2llnmat  39780  2at0mat0  39781  2atm  39783  ps-2c  39784  lplnle  39796  lplnnle2at  39797  llncvrlpln2  39813  llncvrlpln  39814  2lplnmN  39815  2llnmj  39816  2atmat  39817  lplncmp  39818  lplnexllnN  39820  2llnm2N  39824  2llnm4  39826  lvolnle3at  39838  4atlem3a  39853  4atlem3b  39854  4atlem10  39862  4atlem11  39865  4atlem12  39868  lplncvrlvol2  39871  lplncvrlvol  39872  lvolcmp  39873  2lplnm2N  39877  2lplnmj  39878  dalempjsen  39909  dalemcea  39916  dalem2  39917  dalemdea  39918  dalem9  39928  dalem16  39935  dalemcjden  39948  dalem21  39950  dalem23  39952  dalem39  39967  dalem54  39982  dalem60  39988  cdlemb  40050  elpadd2at  40062  paddasslem4  40079  paddasslem7  40082  paddasslem15  40090  paddasslem16  40091  pmodlem1  40102  pmodlem2  40103  llnexchb2  40125  pclfinclN  40206  osumcllem9N  40220  pmapojoinN  40224  pexmidN  40225  pl42lem1N  40235  lhp0lt  40259  lhpexle1  40264  lhpexle2lem  40265  lhpexle3lem  40267  lhprelat3N  40296  ltrnid  40391  trlval3  40443  arglem1N  40446  cdlemc5  40451  cdleme3b  40485  cdleme3c  40486  cdleme3h  40491  cdleme7e  40503  cdleme7ga  40504  cdleme20l1  40576  cdleme20l2  40577  cdleme20l  40578  cdleme22b  40597  cdlemefrs29clN  40655  cdlemefrs32fva  40656  cdlemeg46fvcl  40762  cdlemeg46c  40769  cdlemeg46fvaw  40772  cdlemeg46req  40785  cdleme48fgv  40794  cdlemf1  40817  cdlemg1cex  40844  cdlemg2dN  40846  cdlemg2ce  40848  cdlemg12e  40903  cdlemg35  40969  cdlemh  41073  tendocan  41080  cdlemk28-3  41164  tendoex  41231  dih1  41542  dihmeetlem9N  41571  dihlspsnssN  41588  dihlspsnat  41589  lcfrlem23  41821  renegneg  42663  fsuppind  42829  flt4lem4  42888  3cubes  42928  mzpsubst  42986  rencldnfi  43059  irrapx1  43066  pellexlem3  43069  pellexlem5  43071  infmrgelbi  43116  pellqrex  43117  pellfundge  43120  rmspecfund  43147  congtr  43203  acongeq  43221  jm2.20nn  43235  jm2.25lem1  43236  jm2.26  43240  expdiophlem1  43259  hbtlem2  43362  cantnftermord  43558  suprleubrd  44403  suprlubrd  44405  suprnmpt  45414  wessf1ornlem  45425  mpct  45441  upbdrech  45549  ssfiunibd  45553  uzfissfz  45567  xleadd2d  45568  suprltrp  45569  xleadd1d  45570  suprleubrnmpt  45662  iccintsng  45765  limcrecl  45871  fnlimfvre  45914  dvmulcncf  46165  dvdivcncf  46167  dvbdfbdioolem1  46168  ioodvbdlimc1lem2  46172  ioodvbdlimc2lem  46174  stoweidlem1  46241  stoweidlem20  46260  stoweidlem24  46264  stoweidlem34  46274  stoweidlem45  46285  stoweidlem60  46300  fourierdlem20  46367  fourierdlem31  46378  fourierdlem38  46385  fourierdlem64  46410  fourierdlem79  46425  fourierdlem94  46440  fourierdlem113  46459  fouriersw  46471  fouriercn  46472  sge0isum  46667  hoicvr  46788  ovnsubaddlem2  46811  hoidmv1lelem1  46831  hoidmv1lelem3  46833  hoidmvlelem1  46835  hoidmvlelem4  46838  smflimlem2  47012  fmtnof1  47777  lighneallem2  47848  uspgrlim  48234  upgrwlkupwlk  48382  lincresunit3  48723  elbigolo1  48799  eenglngeehlnm  48981