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  3602  elovmpt3rab1  7683  smo11  8360  omeulem2  8577  oeeui  8597  oaabs2  8644  omabs  8646  omxpenlem  9076  map2xp  9145  mapdom2  9146  fsuppsssupp  9351  cantnflt  9651  cnfcom  9679  mapdjuen  10183  pwsdompw  10205  ackbij1lem5  10225  cofsmo  10271  fin1a2lem4  10405  ltmul12a  12089  lt2msq1  12117  ledivp1  12135  lemul1ad  12172  lemul2ad  12173  suprubd  12195  supaddc  12200  supadd  12201  supmul1  12202  supmul  12205  rpnnen1lem3  13021  rpnnen1lem5  13023  lediv2ad  13100  xaddge0  13302  xadddi  13339  xadddi2  13341  supicc  13546  supicclub  13548  difelfznle  13689  flval3  13868  expcan  14225  ltexp2  14226  ltexp2r  14229  expubnd  14234  ltexp2rd  14304  ltexp2d  14307  leexp2d  14308  expcand  14309  hashmap  14492  swrdf1  14711  swrds1  14728  ccatswrd  14730  pfxfv  14744  swrdccatin1  14786  pfxccatin12lem3  14793  cshwidxmod  14866  wrdl3s3  15025  o1fsum  15891  mertenslem1  15964  eftlub  16190  rpnnen2lem4  16298  ruclem12  16322  dvdsadd  16385  3dvds  16414  divalgmod  16489  bitsmod  16519  bitsinv1lem  16524  bezoutlem4  16625  gcdzeq  16635  rplpwr  16641  sqgcd  16645  expgcd  16646  rpmulgcd2  16739  rpdvds  16743  coprmproddvdslem  16745  isprm5  16791  divgcdodd  16794  dvdszzq  16805  divnumden  16832  crth  16862  phimullem  16863  modprm0  16890  modprmn0modprm0  16892  coprimeprodsq2  16894  pythagtriplem19  16918  pockthlem  16990  prmunb  16999  prmreclem3  17003  prmreclem6  17006  ramub  17098  ramz  17110  kerf1ghm  19348  pmtrprfv  19554  pmtrprfv3  19555  mndodcong  19643  odngen  19678  pgpfi  19706  sylow2blem3  19723  lsmless1  19761  lsmless2  19762  lsmless12  19763  lsmmod2  19777  pj1id  19800  odadd2  19950  gexexlem  19953  ablfacrplem  20168  ablfacrp  20169  ablfac1b  20173  ablfac1eu  20176  pgpfac1lem2  20178  ogrpaddlt  20239  elrhmunit  20644  rrgnz  20840  ornglmullt  21009  orngrmullt  21010  lsmssspx  21246  lspsncv0  21307  qsidomlem1  21517  ssdifidlprm  21523  znunit  21750  uvcvvcl2  21975  uvcvv1  21976  uvcvv0  21977  coe1subfv  22464  coe1fzgsumdlem  22500  scmate  22704  mdetunilem2  22807  pmatcoe1fsupp  22895  mat2pmatlin  22929  decpmatmullem  22965  pmatcollpw1lem1  22968  pmatcollpw1lem2  22969  pm2mpghm  23010  chpscmat  23036  chp0mat  23040  chpidmat  23041  cpmadugsumlemB  23068  cpmadugsumlemC  23069  cpmadugsumlemF  23070  clsndisj  23269  neiptopnei  23326  rnelfm  24147  fmfnfmlem2  24149  fmfnfm  24152  flimss1  24167  isfcf  24228  cnextfun  24258  cnextfvval  24259  cnextf  24260  cnextcn  24261  cnextfres1  24262  ustuqtop1  24435  utopsnneiplem  24441  xblss2ps  24595  xblss2  24596  stdbdxmet  24709  metcnpi3  24740  metustexhalf  24750  nmoi  24922  nmoi2  24924  nmoco  24931  blcvx  24992  icccmplem2  25018  icccmplem3  25019  reconnlem2  25022  xrge0gsumle  25028  metds0  25045  metdstri  25046  metdseq0  25049  lebnumlem3  25159  nmoleub2lem  25310  bcthlem5  25524  csschl  25572  minveclem2  25622  minveclem3b  25624  minveclem4  25628  minveclem6  25630  icombl  25760  cncombf  25854  mbflimsup  25862  itg2monolem1  25946  itg2cnlem1  25957  itg2cnlem2  25958  bddmulibl  26035  ellimc2  26073  cpnord  26131  cpnres  26133  dvmulbr  26135  dvcobr  26142  dvlipcn  26190  dvlip2  26191  dvivthlem1  26204  lhop1lem  26209  lhop1  26210  dvfsumlem2  26223  itgsubstlem  26244  deg1add  26297  deg1sublt  26304  ply1remlem  26359  plyeq0lem  26404  taylthlem2  26574  ulmdvlem3  26602  abelthlem7  26638  pilem2  26652  pilem3  26653  pige3ALT  26722  logccv  26865  cxpaddlelem  26953  cvxcl  27186  fsumharmonic  27213  ftalem5  27278  mpodvdsmulf1o  27395  dvdsmulf1o  27397  bposlem1  27485  lgsqr  27552  lgsquad2lem2  27586  2lgsoddprmlem1  27609  2sqlem8a  27626  2sqlem8  27627  dchrmusum2  27695  dchrvmasumiflem1  27702  dchrisum0flblem1  27709  dchrisum0lem1b  27716  pntlem3  27810  noetasuplem4  27937  noetainflem4  27941  noetalem1  27942  divmulswd  28424  divsclwd  28426  uzsind  28635  tgdim01  28813  axsegcon  29314  ax5seglem1  29315  ax5seglem2  29316  axlowdimlem6  29334  axeuclidlem  29349  axcontlem7  29357  axcontlem9  29359  axcontlem10  29360  nbupgr  29731  nbumgrvtx  29733  cusgrsize2inds  29840  upgriswlk  30027  2pthnloop  30117  numclwwlk2lem1  30764  frgrreg  30782  nmoub3i  31162  ubthlem3  31261  minvecolem2  31264  minvecolem4  31269  minvecolem5  31270  minvecolem6  31271  htthlem  31306  pjpjpre  31808  chscllem1  32026  chscllem2  32027  chscllem3  32028  cnlnadjlem2  32457  leopnmid  32527  tpssad  32922  br8d  32990  splfv3  33309  symgcom2  33435  cyc3genpmlem  33502  archirngz  33540  elrgspnlem1  33593  erld2  33617  rlocf1  33625  subrdom  33636  ricdomn1  33640  dvdsruasso  33729  unitpidl1  33763  elrspunidl  33767  mxidlirredi  33785  dflringlem2  33816  1arithidomlem2  33857  1arithidom  33858  1arithufdlem3  33867  ply1gsumz  33920  mplidomlem  33948  esplymhp  33989  esplyfvaln  33995  vietadeg1  33999  lssdimle  34029  dimkerim  34048  fedgmullem2  34051  fedgmul  34052  assalactf1o  34056  fldextrspundglemul  34100  fldextrspundgdvds  34102  minplyirred  34132  irredminply  34137  algextdeglem2  34139  rtelextdg2lem  34147  constrext2chnlem  34171  constrresqrtcl  34198  2sqr3minply  34201  cos9thpiminplylem2  34204  cos9thpiminply  34209  qqhval2lem  34402  qqhnm  34411  qqhucn  34413  esumcst  34484  esumpcvgval  34499  measunl  34638  dya2iocbrsiga  34697  dya2icobrsiga  34698  omssubadd  34722  inelcarsg  34733  carsgclctunlem2  34741  sibfof  34762  sitgaddlemb  34770  oddpwdc  34776  eulerpartlemgc  34784  bayesth  34861  ftc2re  35017  breprexplemc  35051  tgoldbachgt  35082  erdszelem8  35711  2goelgoanfmla1  35937  br8  36269  matunitlindflem2  38309  totbndbnd  38481  prdsbnd  38485  rrncmslem  38524  rrntotbnd  38528  isdrngo2  38650  lsatcmp  39818  lcvexchlem2  39850  lcvexchlem3  39851  ncvr1  40087  cvrletrN  40088  cvrnbtwn3  40091  cvrnrefN  40097  cvrcmp  40098  0ltat  40106  atnle0  40124  atlen0  40125  cvlcvr1  40154  cvrval3  40228  atle  40251  athgt  40271  1cvratex  40288  ps-2  40293  ps-2b  40297  llnnleat  40328  2atneat  40330  llnle  40333  atcvrlln  40335  llncmp  40337  2llnmat  40339  2at0mat0  40340  2atm  40342  ps-2c  40343  lplnle  40355  lplnnle2at  40356  llncvrlpln2  40372  llncvrlpln  40373  2lplnmN  40374  2llnmj  40375  2atmat  40376  lplncmp  40377  lplnexllnN  40379  2llnm2N  40383  2llnm4  40385  lvolnle3at  40397  4atlem3a  40412  4atlem3b  40413  4atlem10  40421  4atlem11  40424  4atlem12  40427  lplncvrlvol2  40430  lplncvrlvol  40431  lvolcmp  40432  2lplnm2N  40436  2lplnmj  40437  dalempjsen  40468  dalemcea  40475  dalem2  40476  dalemdea  40477  dalem9  40487  dalem16  40494  dalemcjden  40507  dalem21  40509  dalem23  40511  dalem39  40526  dalem54  40541  dalem60  40547  cdlemb  40609  elpadd2at  40621  paddasslem4  40638  paddasslem7  40641  paddasslem15  40649  paddasslem16  40650  pmodlem1  40661  pmodlem2  40662  llnexchb2  40684  pclfinclN  40765  osumcllem9N  40779  pmapojoinN  40783  pexmidN  40784  pl42lem1N  40794  lhp0lt  40818  lhpexle1  40823  lhpexle2lem  40824  lhpexle3lem  40826  lhprelat3N  40855  ltrnid  40950  trlval3  41002  arglem1N  41005  cdlemc5  41010  cdleme3b  41044  cdleme3c  41045  cdleme3h  41050  cdleme7e  41062  cdleme7ga  41063  cdleme20l1  41135  cdleme20l2  41136  cdleme20l  41137  cdleme22b  41156  cdlemefrs29clN  41214  cdlemefrs32fva  41215  cdlemeg46fvcl  41321  cdlemeg46c  41328  cdlemeg46fvaw  41331  cdlemeg46req  41344  cdleme48fgv  41353  cdlemf1  41376  cdlemg1cex  41403  cdlemg2dN  41405  cdlemg2ce  41407  cdlemg12e  41462  cdlemg35  41528  cdlemh  41632  tendocan  41639  cdlemk28-3  41723  tendoex  41790  dih1  42101  dihmeetlem9N  42130  dihlspsnssN  42147  dihlspsnat  42148  lcfrlem23  42380  renegneg  43214  fsuppind  43363  flt4lem4  43422  3cubes  43462  mzpsubst  43520  rencldnfi  43589  irrapx1  43596  pellexlem3  43599  pellexlem5  43601  infmrgelbi  43646  pellqrex  43647  pellfundge  43650  rmspecfund  43677  congtr  43733  acongeq  43751  jm2.20nn  43765  jm2.25lem1  43766  jm2.26  43770  expdiophlem1  43789  hbtlem2  43892  cantnftermord  44088  suprleubrd  44933  suprlubrd  44935  suprnmpt  45933  wessf1ornlem  45944  mpct  45959  upbdrech  46065  ssfiunibd  46069  uzfissfz  46083  xleadd2d  46084  suprltrp  46085  xleadd1d  46086  suprleubrnmpt  46177  iccintsng  46280  limcrecl  46386  fnlimfvre  46429  dvmulcncf  46680  dvdivcncf  46682  dvbdfbdioolem1  46683  ioodvbdlimc1lem2  46687  ioodvbdlimc2lem  46689  stoweidlem1  46756  stoweidlem20  46775  stoweidlem24  46779  stoweidlem34  46789  stoweidlem45  46800  stoweidlem60  46815  fourierdlem20  46882  fourierdlem31  46893  fourierdlem38  46900  fourierdlem64  46925  fourierdlem79  46940  fourierdlem94  46955  fourierdlem113  46974  fouriersw  46986  fouriercn  46987  sge0isum  47182  hoicvr  47303  ovnsubaddlem2  47326  hoidmv1lelem1  47346  hoidmv1lelem3  47348  hoidmvlelem1  47350  hoidmvlelem4  47353  smflimlem2  47527  2timesltsq  48156  fmtnof1  48328  lighneallem2  48399  uspgrlim  48798  upgrwlkupwlk  48946  lincresunit3  49302  elbigolo1  49378  eenglngeehlnm  49560