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 596	1 ⊢ (𝜑 → 𝜂)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  syl32anc  1405  stoic4b  1811  3rspcedvdw  3594  elovmpt3rab1  7673  smo11  8356  omeulem2  8575  oeeui  8595  oaabs2  8642  omabs  8644  omxpenlem  9081  map2xp  9150  mapdom2  9151  fsuppsssupp  9357  cantnflt  9657  cnfcom  9685  mapdjuen  10240  pwsdompw  10262  ackbij1lem5  10282  cofsmo  10328  fin1a2lem4  10462  ltmul12a  12154  lt2msq1  12182  ledivp1  12200  lemul1ad  12237  lemul2ad  12238  suprubd  12260  supaddc  12265  supadd  12266  supmul1  12267  supmul  12270  rpnnen1lem3  13088  rpnnen1lem5  13090  lediv2ad  13167  xaddge0  13369  xadddi  13406  xadddi2  13408  supicc  13613  supicclub  13615  difelfznle  13756  flval3  13935  expcan  14292  ltexp2  14293  ltexp2r  14296  expubnd  14301  ltexp2rd  14372  ltexp2d  14375  leexp2d  14376  expcand  14377  hashmap  14560  swrdf1  14779  swrds1  14796  ccatswrd  14798  pfxfv  14812  swrdccatin1  14854  pfxccatin12lem3  14861  cshwidxmod  14934  wrdl3s3  15095  o1fsum  15960  mertenslem1  16033  eftlub  16257  rpnnen2lem4  16365  ruclem12  16389  dvdsadd  16452  3dvds  16481  divalgmod  16556  bitsmod  16586  bitsinv1lem  16591  bezoutlem4  16695  gcdzeq  16705  rplpwr  16712  sqgcd  16716  expgcd  16717  rpmulgcd2  16811  rpdvds  16815  coprmproddvdslem  16817  isprm5  16863  divgcdodd  16866  dvdszzq  16877  divnumden  16904  crth  16935  phimullem  16936  modprm0  16963  modprmn0modprm0  16965  coprimeprodsq2  16967  pythagtriplem19  16991  pockthlem  17063  prmunb  17072  prmreclem3  17076  prmreclem6  17079  ramub  17171  ramz  17183  kerf1ghm  19441  pmtrprfv  19647  pmtrprfv3  19648  mndodcong  19736  odngen  19771  pgpfi  19799  sylow2blem3  19816  lsmless1  19854  lsmless2  19855  lsmless12  19856  lsmmod2  19870  pj1id  19893  odadd2  20043  gexexlem  20046  ablfacrplem  20261  ablfacrp  20262  ablfac1b  20266  ablfac1eu  20269  pgpfac1lem2  20271  ogrpaddlt  20332  elrhmunit  20740  rrgnz  20936  ornglmullt  21106  orngrmullt  21107  lsmssspx  21343  lspsncv0  21404  qsidomlem1  21616  ssdifidlprm  21622  znunit  21849  uvcvvcl2  22074  uvcvv1  22075  uvcvv0  22076  coe1subfv  22565  coe1fzgsumdlem  22601  scmate  22805  mdetunilem2  22908  matunitlindflem2  22975  pmatcoe1fsupp  22999  mat2pmatlin  23033  decpmatmullem  23069  pmatcollpw1lem1  23072  pmatcollpw1lem2  23073  pm2mpghm  23114  chpscmat  23140  chp0mat  23144  chpidmat  23145  cpmadugsumlemB  23172  cpmadugsumlemC  23173  cpmadugsumlemF  23174  clsndisj  23373  neiptopnei  23430  rnelfm  24252  fmfnfmlem2  24254  fmfnfm  24257  flimss1  24272  isfcf  24333  cnextfun  24363  cnextfvval  24364  cnextf  24365  cnextcn  24366  cnextfres1  24367  ustuqtop1  24540  utopsnneiplem  24546  xblss2ps  24700  xblss2  24701  stdbdxmet  24814  metcnpi3  24845  metustexhalf  24855  nmoi  25027  nmoi2  25029  nmoco  25036  blcvx  25097  icccmplem2  25123  icccmplem3  25124  reconnlem2  25127  xrge0gsumle  25133  metds0  25150  metdstri  25151  metdseq0  25154  lebnumlem3  25264  nmoleub2lem  25415  bcthlem5  25629  csschl  25677  minveclem2  25727  minveclem3b  25729  minveclem4  25733  minveclem6  25735  icombl  25865  cncombf  25959  mbflimsup  25967  itg2monolem1  26051  itg2cnlem1  26062  itg2cnlem2  26063  bddmulibl  26139  ellimc2  26177  cpnord  26235  cpnres  26237  dvmulbr  26239  dvcobr  26246  dvlipcn  26294  dvlip2  26295  dvivthlem1  26308  lhop1lem  26313  lhop1  26314  dvfsumlem2  26327  itgsubstlem  26348  deg1add  26401  deg1sublt  26408  ply1remlem  26463  plyeq0lem  26509  taylthlem2  26683  ulmdvlem3  26711  abelthlem7  26747  pilem2  26761  pilem3  26762  pige3ALT  26830  logccv  26973  cxpaddlelem  27061  cvxcl  27294  fsumharmonic  27321  ftalem5  27386  mpodvdsmulf1o  27503  dvdsmulf1o  27505  bposlem1  27593  lgsqr  27660  lgsquad2lem2  27694  2lgsoddprmlem1  27717  2sqlem8a  27734  2sqlem8  27735  dchrmusum2  27803  dchrvmasumiflem1  27810  dchrisum0flblem1  27817  dchrisum0lem1b  27824  pntlem3  27918  flt4lem4  27961  noetasuplem4  28075  noetainflem4  28079  noetalem1  28080  divmulswd  28562  divsclwd  28564  uzsind  28773  tgdim01  28952  axsegcon  29487  ax5seglem1  29488  ax5seglem2  29489  axlowdimlem6  29507  axeuclidlem  29522  axcontlem7  29530  axcontlem9  29532  axcontlem10  29533  nbupgr  29907  nbumgrvtx  29909  cusgrsize2inds  30016  upgriswlk  30203  2pthnloop  30299  numclwwlk2lem1  30959  frgrreg  30977  nmoub3i  31357  ubthlem3  31456  minvecolem2  31459  minvecolem4  31464  minvecolem5  31465  minvecolem6  31466  htthlem  31501  pjpjpre  32003  chscllem1  32221  chscllem2  32222  chscllem3  32223  cnlnadjlem2  32652  leopnmid  32722  tpssad  33117  br8d  33184  splfv3  33501  symgcom2  33627  cyc3genpmlem  33694  archirngz  33732  elrgspnlem1  33785  erld2  33809  rlocf1  33817  subrdom  33828  ricdomn1  33832  dvdsruasso  33922  unitpidl1  33956  elrspunidl  33960  mxidlirredi  33978  dflringlem2  34009  1arithidomlem2  34050  1arithidom  34051  1arithufdlem3  34060  ply1gsumz  34113  mplidomlem  34141  esplymhp  34182  esplyfvaln  34188  vietadeg1  34192  lssdimle  34222  dimkerim  34241  fedgmullem2  34244  fedgmul  34245  assalactf1o  34249  fldextrspundglemul  34293  fldextrspundgdvds  34295  minplyirred  34325  irredminply  34330  algextdeglem2  34332  rtelextdg2lem  34340  constrext2chnlem  34364  constrresqrtcl  34391  2sqr3minply  34394  cos9thpiminplylem2  34397  cos9thpiminply  34402  qqhval2lem  34595  qqhnm  34604  qqhucn  34606  esumcst  34677  esumpcvgval  34692  measunl  34831  dya2iocbrsiga  34890  dya2icobrsiga  34891  omssubadd  34915  inelcarsg  34926  carsgclctunlem2  34934  sibfof  34955  sitgaddlemb  34963  oddpwdc  34969  eulerpartlemgc  34977  bayesth  35054  ftc2re  35210  breprexplemc  35244  tgoldbachgt  35275  erdszelem8  35932  2goelgoanfmla1  36158  br8  36490  totbndbnd  38691  prdsbnd  38695  rrncmslem  38734  rrntotbnd  38738  isdrngo2  38860  lsatcmp  40028  lcvexchlem2  40060  lcvexchlem3  40061  ncvr1  40297  cvrletrN  40298  cvrnbtwn3  40301  cvrnrefN  40307  cvrcmp  40308  0ltat  40316  atnle0  40334  atlen0  40335  cvlcvr1  40364  cvrval3  40438  atle  40461  athgt  40481  1cvratex  40498  ps-2  40503  ps-2b  40507  llnnleat  40538  2atneat  40540  llnle  40543  atcvrlln  40545  llncmp  40547  2llnmat  40549  2at0mat0  40550  2atm  40552  ps-2c  40553  lplnle  40565  lplnnle2at  40566  llncvrlpln2  40582  llncvrlpln  40583  2lplnmN  40584  2llnmj  40585  2atmat  40586  lplncmp  40587  lplnexllnN  40589  2llnm2N  40593  2llnm4  40595  lvolnle3at  40607  4atlem3a  40622  4atlem3b  40623  4atlem10  40631  4atlem11  40634  4atlem12  40637  lplncvrlvol2  40640  lplncvrlvol  40641  lvolcmp  40642  2lplnm2N  40646  2lplnmj  40647  dalempjsen  40678  dalemcea  40685  dalem2  40686  dalemdea  40687  dalem9  40697  dalem16  40704  dalemcjden  40717  dalem21  40719  dalem23  40721  dalem39  40736  dalem54  40751  dalem60  40757  cdlemb  40819  elpadd2at  40831  paddasslem4  40848  paddasslem7  40851  paddasslem15  40859  paddasslem16  40860  pmodlem1  40871  pmodlem2  40872  llnexchb2  40894  pclfinclN  40975  osumcllem9N  40989  pmapojoinN  40993  pexmidN  40994  pl42lem1N  41004  lhp0lt  41028  lhpexle1  41033  lhpexle2lem  41034  lhpexle3lem  41036  lhprelat3N  41065  ltrnid  41160  trlval3  41212  arglem1N  41215  cdlemc5  41220  cdleme3b  41254  cdleme3c  41255  cdleme3h  41260  cdleme7e  41272  cdleme7ga  41273  cdleme20l1  41345  cdleme20l2  41346  cdleme20l  41347  cdleme22b  41366  cdlemefrs29clN  41424  cdlemefrs32fva  41425  cdlemeg46fvcl  41531  cdlemeg46c  41538  cdlemeg46fvaw  41541  cdlemeg46req  41554  cdleme48fgv  41563  cdlemf1  41586  cdlemg1cex  41613  cdlemg2dN  41615  cdlemg2ce  41617  cdlemg12e  41672  cdlemg35  41738  cdlemh  41842  tendocan  41849  cdlemk28-3  41933  tendoex  42000  dih1  42311  dihmeetlem9N  42340  dihlspsnssN  42357  dihlspsnat  42358  lcfrlem23  42590  renegneg  43431  fsuppind  43580  3cubes  43654  mzpsubst  43712  rencldnfi  43781  irrapx1  43788  pellexlem3  43791  pellexlem5  43793  infmrgelbi  43838  pellqrex  43839  pellfundge  43842  rmspecfund  43869  congtr  43925  acongeq  43943  jm2.20nn  43957  jm2.25lem1  43958  jm2.26  43962  expdiophlem1  43981  hbtlem2  44084  cantnftermord  44280  suprleubrd  45125  suprlubrd  45127  suprnmpt  46132  wessf1ornlem  46143  mpct  46158  upbdrech  46264  ssfiunibd  46268  uzfissfz  46282  xleadd2d  46283  suprltrp  46284  xleadd1d  46285  suprleubrnmpt  46376  iccintsng  46479  limcrecl  46585  fnlimfvre  46628  dvmulcncf  46879  dvdivcncf  46881  dvbdfbdioolem1  46882  ioodvbdlimc1lem2  46886  ioodvbdlimc2lem  46888  stoweidlem1  46955  stoweidlem20  46974  stoweidlem24  46978  stoweidlem34  46988  stoweidlem45  46999  stoweidlem60  47014  fourierdlem20  47081  fourierdlem31  47092  fourierdlem38  47099  fourierdlem64  47124  fourierdlem79  47139  fourierdlem94  47154  fourierdlem113  47173  fouriersw  47185  fouriercn  47186  sge0isum  47381  hoicvr  47502  ovnsubaddlem2  47525  hoidmv1lelem1  47545  hoidmv1lelem3  47547  hoidmvlelem1  47549  hoidmvlelem4  47552  smflimlem2  47726  2timesltsq  48392  fmtnof1  48564  lighneallem2  48635  uspgrlim  49034  upgrwlkupwlk  49182  lincresunit3  49537  elbigolo1  49613  eenglngeehlnm  49795