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  1778  3rspcedvdw  3619  elovmpt3rab1  7665  smo11  8376  omeulem2  8593  oeeui  8612  oaabs2  8659  omabs  8661  omxpenlem  9085  map2xp  9159  mapdom2  9160  fsuppsssupp  9391  cantnflt  9684  cnfcom  9712  mapdjuen  10193  pwsdompw  10215  ackbij1lem5  10235  cofsmo  10281  fin1a2lem4  10415  ltmul12a  12095  lt2msq1  12124  ledivp1  12142  lemul1ad  12179  lemul2ad  12180  suprubd  12202  supaddc  12207  supadd  12208  supmul1  12209  supmul  12212  rpnnen1lem3  12993  rpnnen1lem5  12995  lediv2ad  13071  xaddge0  13272  xadddi  13309  xadddi2  13311  supicc  13516  supicclub  13518  difelfznle  13657  flval3  13830  expcan  14185  ltexp2  14186  ltexp2r  14189  expubnd  14194  ltexp2rd  14264  ltexp2d  14267  leexp2d  14268  expcand  14269  hashmap  14451  swrds1  14682  ccatswrd  14684  pfxfv  14698  swrdccatin1  14741  pfxccatin12lem3  14748  cshwidxmod  14819  wrdl3s3  14979  o1fsum  15827  mertenslem1  15898  eftlub  16125  rpnnen2lem4  16233  ruclem12  16257  dvdsadd  16319  3dvds  16348  divalgmod  16423  bitsmod  16453  bitsinv1lem  16458  bezoutlem4  16559  gcdzeq  16569  rplpwr  16575  sqgcd  16579  expgcd  16580  rpmulgcd2  16673  rpdvds  16677  coprmproddvdslem  16679  isprm5  16724  divgcdodd  16727  dvdszzq  16738  divnumden  16765  crth  16795  phimullem  16796  modprm0  16823  modprmn0modprm0  16825  coprimeprodsq2  16827  pythagtriplem19  16851  pockthlem  16923  prmunb  16932  prmreclem3  16936  prmreclem6  16939  ramub  17031  ramz  17043  kerf1ghm  19228  pmtrprfv  19432  pmtrprfv3  19433  mndodcong  19521  odngen  19556  pgpfi  19584  sylow2blem3  19601  lsmless1  19639  lsmless2  19640  lsmless12  19641  lsmmod2  19655  pj1id  19678  odadd2  19828  gexexlem  19831  ablfacrplem  20046  ablfacrp  20047  ablfac1b  20051  ablfac1eu  20054  pgpfac1lem2  20056  elrhmunit  20468  rrgnz  20662  lsmssspx  21044  lspsncv0  21105  znunit  21522  uvcvvcl2  21746  uvcvv1  21747  uvcvv0  21748  coe1subfv  22201  coe1fzgsumdlem  22239  scmate  22446  mdetunilem2  22549  pmatcoe1fsupp  22637  mat2pmatlin  22671  decpmatmullem  22707  pmatcollpw1lem1  22710  pmatcollpw1lem2  22711  pm2mpghm  22752  chpscmat  22778  chp0mat  22782  chpidmat  22783  cpmadugsumlemB  22810  cpmadugsumlemC  22811  cpmadugsumlemF  22812  clsndisj  23011  neiptopnei  23068  rnelfm  23889  fmfnfmlem2  23891  fmfnfm  23894  flimss1  23909  isfcf  23970  cnextfun  24000  cnextfvval  24001  cnextf  24002  cnextcn  24003  cnextfres1  24004  ustuqtop1  24178  utopsnneiplem  24184  xblss2ps  24338  xblss2  24339  stdbdxmet  24452  metcnpi3  24483  metustexhalf  24493  nmoi  24665  nmoi2  24667  nmoco  24674  blcvx  24735  icccmplem2  24761  icccmplem3  24762  reconnlem2  24765  xrge0gsumle  24771  metds0  24788  metdstri  24789  metdseq0  24792  lebnumlem3  24911  nmoleub2lem  25063  bcthlem5  25278  csschl  25326  minveclem2  25376  minveclem3b  25378  minveclem4  25382  minveclem6  25384  icombl  25515  cncombf  25609  mbflimsup  25617  itg2monolem1  25701  itg2cnlem1  25712  itg2cnlem2  25713  bddmulibl  25790  ellimc2  25828  cpnord  25887  cpnres  25889  dvmulbr  25891  dvmulbrOLD  25892  dvcobr  25899  dvcobrOLD  25900  dvlipcn  25949  dvlip2  25950  dvivthlem1  25963  lhop1lem  25968  lhop1  25969  dvfsumlem2  25983  dvfsumlem2OLD  25984  itgsubstlem  26005  deg1add  26058  deg1sublt  26065  ply1remlem  26120  plyeq0lem  26165  taylthlem2  26332  taylthlem2OLD  26333  ulmdvlem3  26361  abelthlem7  26398  pilem2  26412  pilem3  26413  pige3ALT  26479  logccv  26622  cxpaddlelem  26711  cvxcl  26945  fsumharmonic  26972  ftalem5  27037  mpodvdsmulf1o  27154  dvdsmulf1o  27156  bposlem1  27245  lgsqr  27312  lgsquad2lem2  27346  2lgsoddprmlem1  27369  2sqlem8a  27386  2sqlem8  27387  dchrmusum2  27455  dchrvmasumiflem1  27462  dchrisum0flblem1  27469  dchrisum0lem1b  27476  pntlem3  27570  noetasuplem4  27698  noetainflem4  27702  noetalem1  27703  divsmulwd  28136  divsclwd  28138  uzsind  28308  tgdim01  28432  axsegcon  28852  ax5seglem1  28853  ax5seglem2  28854  axlowdimlem6  28872  axeuclidlem  28887  axcontlem7  28895  axcontlem9  28897  axcontlem10  28898  nbupgr  29269  nbumgrvtx  29271  cusgrsize2inds  29379  upgriswlk  29567  2pthnloop  29659  numclwwlk2lem1  30303  frgrreg  30321  nmoub3i  30700  ubthlem3  30799  minvecolem2  30802  minvecolem4  30807  minvecolem5  30808  minvecolem6  30809  htthlem  30844  pjpjpre  31346  chscllem1  31564  chscllem2  31565  chscllem3  31566  cnlnadjlem2  31995  leopnmid  32065  tpssad  32466  br8d  32536  swrdf1  32878  splfv3  32880  ogrpaddlt  33031  symgcom2  33041  cyc3genpmlem  33108  archirngz  33133  elrgspnlem1  33183  rlocf1  33214  subrdom  33225  ornglmullt  33275  orngrmullt  33276  dvdsruasso  33346  unitpidl1  33385  elrspunidl  33389  qsidomlem1  33413  ssdifidlprm  33419  mxidlirredi  33432  1arithidomlem2  33497  1arithidom  33498  1arithufdlem3  33507  ply1gsumz  33554  lssdimle  33593  dimkerim  33613  fedgmullem2  33616  fedgmul  33617  assalactf1o  33621  fldextrspundglemul  33666  fldextrspundgdvds  33668  minplyirred  33691  irredminply  33696  algextdeglem2  33698  rtelextdg2lem  33706  constrext2chnlem  33730  constrresqrtcl  33757  2sqr3minply  33760  cos9thpiminplylem2  33763  cos9thpiminply  33768  qqhval2lem  33958  qqhnm  33967  qqhucn  33969  esumcst  34040  esumpcvgval  34055  measunl  34193  dya2iocbrsiga  34253  dya2icobrsiga  34254  omssubadd  34278  inelcarsg  34289  carsgclctunlem2  34297  sibfof  34318  sitgaddlemb  34326  oddpwdc  34332  eulerpartlemgc  34340  bayesth  34417  ftc2re  34576  breprexplemc  34610  tgoldbachgt  34641  erdszelem8  35166  2goelgoanfmla1  35392  br8  35719  matunitlindflem2  37587  totbndbnd  37759  prdsbnd  37763  rrncmslem  37802  rrntotbnd  37806  isdrngo2  37928  lsatcmp  38967  lcvexchlem2  38999  lcvexchlem3  39000  ncvr1  39236  cvrletrN  39237  cvrnbtwn3  39240  cvrnrefN  39246  cvrcmp  39247  0ltat  39255  atnle0  39273  atlen0  39274  cvlcvr1  39303  cvrval3  39378  atle  39401  athgt  39421  1cvratex  39438  ps-2  39443  ps-2b  39447  llnnleat  39478  2atneat  39480  llnle  39483  atcvrlln  39485  llncmp  39487  2llnmat  39489  2at0mat0  39490  2atm  39492  ps-2c  39493  lplnle  39505  lplnnle2at  39506  llncvrlpln2  39522  llncvrlpln  39523  2lplnmN  39524  2llnmj  39525  2atmat  39526  lplncmp  39527  lplnexllnN  39529  2llnm2N  39533  2llnm4  39535  lvolnle3at  39547  4atlem3a  39562  4atlem3b  39563  4atlem10  39571  4atlem11  39574  4atlem12  39577  lplncvrlvol2  39580  lplncvrlvol  39581  lvolcmp  39582  2lplnm2N  39586  2lplnmj  39587  dalempjsen  39618  dalemcea  39625  dalem2  39626  dalemdea  39627  dalem9  39637  dalem16  39644  dalemcjden  39657  dalem21  39659  dalem23  39661  dalem39  39676  dalem54  39691  dalem60  39697  cdlemb  39759  elpadd2at  39771  paddasslem4  39788  paddasslem7  39791  paddasslem15  39799  paddasslem16  39800  pmodlem1  39811  pmodlem2  39812  llnexchb2  39834  pclfinclN  39915  osumcllem9N  39929  pmapojoinN  39933  pexmidN  39934  pl42lem1N  39944  lhp0lt  39968  lhpexle1  39973  lhpexle2lem  39974  lhpexle3lem  39976  lhprelat3N  40005  ltrnid  40100  trlval3  40152  arglem1N  40155  cdlemc5  40160  cdleme3b  40194  cdleme3c  40195  cdleme3h  40200  cdleme7e  40212  cdleme7ga  40213  cdleme20l1  40285  cdleme20l2  40286  cdleme20l  40287  cdleme22b  40306  cdlemefrs29clN  40364  cdlemefrs32fva  40365  cdlemeg46fvcl  40471  cdlemeg46c  40478  cdlemeg46fvaw  40481  cdlemeg46req  40494  cdleme48fgv  40503  cdlemf1  40526  cdlemg1cex  40553  cdlemg2dN  40555  cdlemg2ce  40557  cdlemg12e  40612  cdlemg35  40678  cdlemh  40782  tendocan  40789  cdlemk28-3  40873  tendoex  40940  dih1  41251  dihmeetlem9N  41280  dihlspsnssN  41297  dihlspsnat  41298  lcfrlem23  41530  renegneg  42401  fsuppind  42560  flt4lem4  42619  3cubes  42660  mzpsubst  42718  rencldnfi  42791  irrapx1  42798  pellexlem3  42801  pellexlem5  42803  infmrgelbi  42848  pellqrex  42849  pellfundge  42852  rmspecfund  42879  congtr  42936  acongeq  42954  jm2.20nn  42968  jm2.25lem1  42969  jm2.26  42973  expdiophlem1  42992  hbtlem2  43095  cantnftermord  43291  suprleubrd  44137  suprlubrd  44139  suprnmpt  45146  wessf1ornlem  45157  mpct  45173  upbdrech  45282  ssfiunibd  45286  uzfissfz  45301  xleadd2d  45302  suprltrp  45303  xleadd1d  45304  suprleubrnmpt  45397  iccintsng  45500  limcrecl  45606  fnlimfvre  45651  dvmulcncf  45902  dvdivcncf  45904  dvbdfbdioolem1  45905  ioodvbdlimc1lem2  45909  ioodvbdlimc2lem  45911  stoweidlem1  45978  stoweidlem20  45997  stoweidlem24  46001  stoweidlem34  46011  stoweidlem45  46022  stoweidlem60  46037  fourierdlem20  46104  fourierdlem31  46115  fourierdlem38  46122  fourierdlem64  46147  fourierdlem79  46162  fourierdlem94  46177  fourierdlem113  46196  fouriersw  46208  fouriercn  46209  sge0isum  46404  hoicvr  46525  ovnsubaddlem2  46548  hoidmv1lelem1  46568  hoidmv1lelem3  46570  hoidmvlelem1  46572  hoidmvlelem4  46575  smflimlem2  46749  fmtnof1  47497  lighneallem2  47568  uspgrlim  47952  upgrwlkupwlk  48063  lincresunit3  48405  elbigolo1  48485  eenglngeehlnm  48667