Theorem syl31anc 1370

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

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

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 206  df-an 396  df-3an 1086

This theorem is referenced by:  syl32anc  1375  stoic4b  1772  elovmpt3rab1  7663  smo11  8365  omeulem2  8584  oeeui  8603  oaabs2  8650  omabs  8652  omxpenlem  9075  map2xp  9149  mapdom2  9150  fsuppsssupp  9381  cantnflt  9669  cnfcom  9697  mapdjuen  10177  pwsdompw  10201  ackbij1lem5  10221  cofsmo  10266  fin1a2lem4  10400  ltmul12a  12074  lt2msq1  12102  ledivp1  12120  lemul1ad  12157  lemul2ad  12158  suprubd  12180  supaddc  12185  supadd  12186  supmul1  12187  supmul  12190  rpnnen1lem3  12967  rpnnen1lem5  12969  lediv2ad  13044  xaddge0  13243  xadddi  13280  xadddi2  13282  supicc  13484  supicclub  13486  difelfznle  13621  flval3  13786  expcan  14139  ltexp2  14140  ltexp2r  14143  expubnd  14147  ltexp2rd  14216  ltexp2d  14219  leexp2d  14220  expcand  14221  hashmap  14400  swrds1  14622  ccatswrd  14624  pfxfv  14638  swrdccatin1  14681  pfxccatin12lem3  14688  cshwidxmod  14759  wrdl3s3  14919  o1fsum  15765  mertenslem1  15836  eftlub  16059  rpnnen2lem4  16167  ruclem12  16191  dvdsadd  16252  3dvds  16281  divalgmod  16356  bitsmod  16384  bitsinv1lem  16389  bezoutlem4  16491  gcdzeq  16501  rplpwr  16506  sqgcd  16509  rpmulgcd2  16600  rpdvds  16604  coprmproddvdslem  16606  isprm5  16651  divgcdodd  16654  dvdszzq  16666  divnumden  16693  crth  16720  phimullem  16721  modprm0  16747  modprmn0modprm0  16749  coprimeprodsq2  16751  pythagtriplem19  16775  pockthlem  16847  prmunb  16856  prmreclem3  16860  prmreclem6  16863  ramub  16955  ramz  16967  kerf1ghm  19172  pmtrprfv  19373  pmtrprfv3  19374  mndodcong  19462  odngen  19497  pgpfi  19525  sylow2blem3  19542  lsmless1  19580  lsmless2  19581  lsmless12  19582  lsmmod2  19596  pj1id  19619  odadd2  19769  gexexlem  19772  ablfacrplem  19987  ablfacrp  19988  ablfac1b  19992  ablfac1eu  19995  pgpfac1lem2  19997  elrhmunit  20412  lsmssspx  20936  lspsncv0  20997  znunit  21458  uvcvvcl2  21683  uvcvv1  21684  uvcvv0  21685  coe1subfv  22140  coe1fzgsumdlem  22177  scmate  22367  mdetunilem2  22470  pmatcoe1fsupp  22558  mat2pmatlin  22592  decpmatmullem  22628  pmatcollpw1lem1  22631  pmatcollpw1lem2  22632  pm2mpghm  22673  chpscmat  22699  chp0mat  22703  chpidmat  22704  cpmadugsumlemB  22731  cpmadugsumlemC  22732  cpmadugsumlemF  22733  clsndisj  22934  neiptopnei  22991  rnelfm  23812  fmfnfmlem2  23814  fmfnfm  23817  flimss1  23832  isfcf  23893  cnextfun  23923  cnextfvval  23924  cnextf  23925  cnextcn  23926  cnextfres1  23927  ustuqtop1  24101  utopsnneiplem  24107  xblss2ps  24262  xblss2  24263  stdbdxmet  24379  metcnpi3  24410  metustexhalf  24420  nmoi  24600  nmoi2  24602  nmoco  24609  blcvx  24669  icccmplem2  24694  icccmplem3  24695  reconnlem2  24698  xrge0gsumle  24704  metds0  24721  metdstri  24722  metdseq0  24725  lebnumlem3  24844  nmoleub2lem  24996  bcthlem5  25211  csschl  25259  minveclem2  25309  minveclem3b  25311  minveclem4  25315  minveclem6  25317  icombl  25448  cncombf  25542  mbflimsup  25550  itg2monolem1  25635  itg2cnlem1  25646  itg2cnlem2  25647  bddmulibl  25723  ellimc2  25761  cpnord  25820  cpnres  25822  dvmulbr  25824  dvmulbrOLD  25825  dvcobr  25832  dvcobrOLD  25833  dvlipcn  25882  dvlip2  25883  dvivthlem1  25896  lhop1lem  25901  lhop1  25902  dvfsumlem2  25916  dvfsumlem2OLD  25917  itgsubstlem  25938  deg1add  25994  deg1sublt  26001  ply1remlem  26054  plyeq0lem  26099  taylthlem2  26264  taylthlem2OLD  26265  ulmdvlem3  26293  abelthlem7  26330  pilem2  26344  pilem3  26345  pige3ALT  26409  logccv  26552  cxpaddlelem  26641  cvxcl  26872  fsumharmonic  26899  ftalem5  26964  mpodvdsmulf1o  27081  dvdsmulf1o  27083  bposlem1  27172  lgsqr  27239  lgsquad2lem2  27273  2lgsoddprmlem1  27296  2sqlem8a  27313  2sqlem8  27314  dchrmusum2  27382  dchrvmasumiflem1  27389  dchrisum0flblem1  27396  dchrisum0lem1b  27403  pntlem3  27497  noetasuplem4  27624  noetainflem4  27628  noetalem1  27629  divsmulwd  28048  divsclwd  28050  tgdim01  28266  axsegcon  28693  ax5seglem1  28694  ax5seglem2  28695  axlowdimlem6  28713  axeuclidlem  28728  axcontlem7  28736  axcontlem9  28738  axcontlem10  28739  nbupgr  29109  nbumgrvtx  29111  cusgrsize2inds  29219  upgriswlk  29407  2pthnloop  29497  numclwwlk2lem1  30138  frgrreg  30156  nmoub3i  30535  ubthlem3  30634  minvecolem2  30637  minvecolem4  30642  minvecolem5  30643  minvecolem6  30644  htthlem  30679  pjpjpre  31181  chscllem1  31399  chscllem2  31400  chscllem3  31401  cnlnadjlem2  31830  leopnmid  31900  br8d  32348  swrdf1  32625  splfv3  32627  ogrpaddlt  32741  symgcom2  32751  cyc3genpmlem  32816  archirngz  32841  ornglmullt  32928  orngrmullt  32929  dvdsruasso  32996  unitpidl1  33048  elrspunidl  33052  qsidomlem1  33077  mxidlirredi  33093  ply1gsumz  33174  lssdimle  33210  dimkerim  33230  fedgmullem2  33233  fedgmul  33234  minplyirred  33290  irredminply  33293  algextdeglem2  33295  qqhval2lem  33491  qqhnm  33500  qqhucn  33502  esumcst  33591  esumpcvgval  33606  measunl  33744  dya2iocbrsiga  33804  dya2icobrsiga  33805  omssubadd  33829  inelcarsg  33840  carsgclctunlem2  33848  sibfof  33869  sitgaddlemb  33877  oddpwdc  33883  eulerpartlemgc  33891  bayesth  33968  ftc2re  34139  breprexplemc  34173  tgoldbachgt  34204  erdszelem8  34717  2goelgoanfmla1  34943  br8  35259  matunitlindflem2  36998  totbndbnd  37170  prdsbnd  37174  rrncmslem  37213  rrntotbnd  37217  isdrngo2  37339  lsatcmp  38386  lcvexchlem2  38418  lcvexchlem3  38419  ncvr1  38655  cvrletrN  38656  cvrnbtwn3  38659  cvrnrefN  38665  cvrcmp  38666  0ltat  38674  atnle0  38692  atlen0  38693  cvlcvr1  38722  cvrval3  38797  atle  38820  athgt  38840  1cvratex  38857  ps-2  38862  ps-2b  38866  llnnleat  38897  2atneat  38899  llnle  38902  atcvrlln  38904  llncmp  38906  2llnmat  38908  2at0mat0  38909  2atm  38911  ps-2c  38912  lplnle  38924  lplnnle2at  38925  llncvrlpln2  38941  llncvrlpln  38942  2lplnmN  38943  2llnmj  38944  2atmat  38945  lplncmp  38946  lplnexllnN  38948  2llnm2N  38952  2llnm4  38954  lvolnle3at  38966  4atlem3a  38981  4atlem3b  38982  4atlem10  38990  4atlem11  38993  4atlem12  38996  lplncvrlvol2  38999  lplncvrlvol  39000  lvolcmp  39001  2lplnm2N  39005  2lplnmj  39006  dalempjsen  39037  dalemcea  39044  dalem2  39045  dalemdea  39046  dalem9  39056  dalem16  39063  dalemcjden  39076  dalem21  39078  dalem23  39080  dalem39  39095  dalem54  39110  dalem60  39116  cdlemb  39178  elpadd2at  39190  paddasslem4  39207  paddasslem7  39210  paddasslem15  39218  paddasslem16  39219  pmodlem1  39230  pmodlem2  39231  llnexchb2  39253  pclfinclN  39334  osumcllem9N  39348  pmapojoinN  39352  pexmidN  39353  pl42lem1N  39363  lhp0lt  39387  lhpexle1  39392  lhpexle2lem  39393  lhpexle3lem  39395  lhprelat3N  39424  ltrnid  39519  trlval3  39571  arglem1N  39574  cdlemc5  39579  cdleme3b  39613  cdleme3c  39614  cdleme3h  39619  cdleme7e  39631  cdleme7ga  39632  cdleme20l1  39704  cdleme20l2  39705  cdleme20l  39706  cdleme22b  39725  cdlemefrs29clN  39783  cdlemefrs32fva  39784  cdlemeg46fvcl  39890  cdlemeg46c  39897  cdlemeg46fvaw  39900  cdlemeg46req  39913  cdleme48fgv  39922  cdlemf1  39945  cdlemg1cex  39972  cdlemg2dN  39974  cdlemg2ce  39976  cdlemg12e  40031  cdlemg35  40097  cdlemh  40201  tendocan  40208  cdlemk28-3  40292  tendoex  40359  dih1  40670  dihmeetlem9N  40699  dihlspsnssN  40716  dihlspsnat  40717  lcfrlem23  40949  3rspcedvdw  41591  fsuppind  41719  expgcd  41790  renegneg  41862  flt4lem4  41969  3cubes  42006  mzpsubst  42064  rencldnfi  42137  irrapx1  42144  pellexlem3  42147  pellexlem5  42149  infmrgelbi  42194  pellqrex  42195  pellfundge  42198  rmspecfund  42225  congtr  42282  acongeq  42300  jm2.20nn  42314  jm2.25lem1  42315  jm2.26  42319  expdiophlem1  42338  hbtlem2  42444  cantnftermord  42646  suprleubrd  43494  suprlubrd  43496  suprnmpt  44445  wessf1ornlem  44456  mpct  44472  upbdrech  44587  ssfiunibd  44591  uzfissfz  44608  xleadd2d  44609  suprltrp  44610  xleadd1d  44611  suprleubrnmpt  44704  iccintsng  44808  limcrecl  44917  fnlimfvre  44962  dvmulcncf  45213  dvdivcncf  45215  dvbdfbdioolem1  45216  ioodvbdlimc1lem2  45220  ioodvbdlimc2lem  45222  stoweidlem1  45289  stoweidlem20  45308  stoweidlem24  45312  stoweidlem34  45322  stoweidlem45  45333  stoweidlem60  45348  fourierdlem20  45415  fourierdlem31  45426  fourierdlem38  45433  fourierdlem64  45458  fourierdlem79  45473  fourierdlem94  45488  fourierdlem113  45507  fouriersw  45519  fouriercn  45520  sge0isum  45715  hoicvr  45836  ovnsubaddlem2  45859  hoidmv1lelem1  45879  hoidmv1lelem3  45881  hoidmvlelem1  45883  hoidmvlelem4  45886  smflimlem2  46060  fmtnof1  46775  lighneallem2  46846  upgrwlkupwlk  47090  lincresunit3  47437  elbigolo1  47518  eenglngeehlnm  47700