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  1810  3rspcedvdw  3593  elovmpt3rab1  7681  smo11  8375  omeulem2  8594  oeeui  8614  oaabs2  8661  omabs  8663  omxpenlem  9100  map2xp  9169  mapdom2  9170  fsuppsssupp  9376  cantnflt  9676  cnfcom  9704  mapdjuen  10262  pwsdompw  10284  ackbij1lem5  10304  cofsmo  10350  fin1a2lem4  10484  ltmul12a  12176  lt2msq1  12204  ledivp1  12222  lemul1ad  12259  lemul2ad  12260  suprubd  12282  supaddc  12287  supadd  12288  supmul1  12289  supmul  12292  rpnnen1lem3  13110  rpnnen1lem5  13112  lediv2ad  13189  xaddge0  13391  xadddi  13428  xadddi2  13430  supicc  13635  supicclub  13637  difelfznle  13779  flval3  13958  expcan  14315  ltexp2  14316  ltexp2r  14319  expubnd  14324  ltexp2rd  14395  ltexp2d  14398  leexp2d  14399  expcand  14400  hashmap  14583  swrdf1  14803  swrds1  14820  ccatswrd  14822  pfxfv  14836  swrdccatin1  14878  pfxccatin12lem3  14885  cshwidxmod  14958  wrdl3s3  15120  o1fsum  15985  mertenslem1  16058  eftlub  16282  rpnnen2lem4  16390  ruclem12  16414  dvdsadd  16477  3dvds  16506  divalgmod  16581  bitsmod  16611  bitsinv1lem  16616  bezoutlem4  16720  gcdzeq  16730  rplpwr  16737  sqgcd  16741  expgcd  16742  rpmulgcd2  16836  rpdvds  16840  coprmproddvdslem  16842  isprm5  16888  divgcdodd  16891  dvdszzq  16902  divnumden  16929  crth  16960  phimullem  16961  modprm0  16988  modprmn0modprm0  16990  coprimeprodsq2  16992  pythagtriplem19  17016  pockthlem  17088  prmunb  17097  prmreclem3  17101  prmreclem6  17104  ramub  17196  ramz  17208  kerf1ghm  19466  pmtrprfv  19672  pmtrprfv3  19673  mndodcong  19761  odngen  19796  pgpfi  19824  sylow2blem3  19841  lsmless1  19879  lsmless2  19880  lsmless12  19881  lsmmod2  19895  pj1id  19918  odadd2  20068  gexexlem  20071  ablfacrplem  20286  ablfacrp  20287  ablfac1b  20291  ablfac1eu  20294  pgpfac1lem2  20296  ogrpaddlt  20357  elrhmunit  20765  rrgnz  20961  ornglmullt  21131  orngrmullt  21132  lsmssspx  21368  lspsncv0  21429  qsidomlem1  21641  ssdifidlprm  21647  znunit  21874  uvcvvcl2  22099  uvcvv1  22100  uvcvv0  22101  coe1subfv  22590  coe1fzgsumdlem  22626  scmate  22830  mdetunilem2  22933  matunitlindflem2  23000  pmatcoe1fsupp  23024  mat2pmatlin  23058  decpmatmullem  23094  pmatcollpw1lem1  23097  pmatcollpw1lem2  23098  pm2mpghm  23139  chpscmat  23165  chp0mat  23169  chpidmat  23170  cpmadugsumlemB  23197  cpmadugsumlemC  23198  cpmadugsumlemF  23199  clsndisj  23398  neiptopnei  23455  rnelfm  24277  fmfnfmlem2  24279  fmfnfm  24282  flimss1  24297  isfcf  24358  cnextfun  24388  cnextfvval  24389  cnextf  24390  cnextcn  24391  cnextfres1  24392  ustuqtop1  24565  utopsnneiplem  24571  xblss2ps  24725  xblss2  24726  stdbdxmet  24839  metcnpi3  24870  metustexhalf  24880  nmoi  25052  nmoi2  25054  nmoco  25061  blcvx  25122  icccmplem2  25148  icccmplem3  25149  reconnlem2  25152  xrge0gsumle  25158  metds0  25175  metdstri  25176  metdseq0  25179  lebnumlem3  25289  nmoleub2lem  25440  bcthlem5  25654  csschl  25702  minveclem2  25752  minveclem3b  25754  minveclem4  25758  minveclem6  25760  icombl  25890  cncombf  25984  mbflimsup  25992  itg2monolem1  26076  itg2cnlem1  26087  itg2cnlem2  26088  bddmulibl  26164  ellimc2  26202  cpnord  26260  cpnres  26262  dvmulbr  26264  dvcobr  26271  dvlipcn  26319  dvlip2  26320  dvivthlem1  26333  lhop1lem  26338  lhop1  26339  dvfsumlem2  26352  itgsubstlem  26373  deg1add  26426  deg1sublt  26433  ply1remlem  26488  plyeq0lem  26534  taylthlem2  26706  ulmdvlem3  26734  abelthlem7  26770  pilem2  26784  pilem3  26785  pige3ALT  26853  logccv  26996  cxpaddlelem  27084  cvxcl  27317  fsumharmonic  27344  ftalem5  27409  mpodvdsmulf1o  27526  dvdsmulf1o  27528  bposlem1  27616  lgsqr  27683  lgsquad2lem2  27717  2lgsoddprmlem1  27740  2sqlem8a  27757  2sqlem8  27758  dchrmusum2  27826  dchrvmasumiflem1  27833  dchrisum0flblem1  27840  dchrisum0lem1b  27847  pntlem3  27941  flt4lem4  27984  noetasuplem4  28098  noetainflem4  28102  noetalem1  28103  divmulswd  28585  divsclwd  28587  uzsind  28796  tgdim01  28975  axsegcon  29510  ax5seglem1  29511  ax5seglem2  29512  axlowdimlem6  29530  axeuclidlem  29545  axcontlem7  29553  axcontlem9  29555  axcontlem10  29556  nbupgr  29930  nbumgrvtx  29932  cusgrsize2inds  30039  upgriswlk  30226  2pthnloop  30322  numclwwlk2lem1  30982  frgrreg  31000  nmoub3i  31380  ubthlem3  31479  minvecolem2  31482  minvecolem4  31487  minvecolem5  31488  minvecolem6  31489  htthlem  31524  pjpjpre  32026  chscllem1  32244  chscllem2  32245  chscllem3  32246  cnlnadjlem2  32675  leopnmid  32745  tpssad  33182  br8d  33249  splfv3  33565  symgcom2  33691  cyc3genpmlem  33758  archirngz  33796  elrgspnlem1  33849  erld2  33873  rlocf1  33881  subrdom  33892  ricdomn1  33896  dvdsruasso  33986  unitpidl1  34020  mxidlirredi  34042  dflringlem2  34073  1arithidomlem2  34114  1arithidom  34115  1arithufdlem3  34124  ply1gsumz  34177  mplidomlem  34205  esplymhp  34246  esplyfvaln  34252  vietadeg1  34256  lssdimle  34286  dimkerim  34305  fedgmullem2  34308  fedgmul  34309  assalactf1o  34313  fldextrspundglemul  34357  fldextrspundgdvds  34359  minplyirred  34389  irredminply  34394  algextdeglem2  34396  rtelextdg2lem  34404  constrext2chnlem  34428  constrresqrtcl  34455  2sqr3minply  34458  cos9thpiminplylem2  34461  cos9thpiminply  34466  qqhval2lem  34659  qqhnm  34668  qqhucn  34670  esumcst  34741  esumpcvgval  34756  measunl  34895  dya2iocbrsiga  34953  dya2icobrsiga  34954  omssubadd  34978  inelcarsg  34989  carsgclctunlem2  34997  sibfof  35018  sitgaddlemb  35026  oddpwdc  35032  eulerpartlemgc  35040  bayesth  35117  ftc2re  35273  breprexplemc  35307  tgoldbachgt  35338  erdszelem8  36049  2goelgoanfmla1  36275  br8  36613  totbndbnd  38816  prdsbnd  38820  rrncmslem  38859  rrntotbnd  38863  isdrngo2  38985  lsatcmp  40153  lcvexchlem2  40185  lcvexchlem3  40186  ncvr1  40422  cvrletrN  40423  cvrnbtwn3  40426  cvrnrefN  40432  cvrcmp  40433  0ltat  40441  atnle0  40459  atlen0  40460  cvlcvr1  40489  cvrval3  40563  atle  40586  athgt  40606  1cvratex  40623  ps-2  40628  ps-2b  40632  llnnleat  40663  2atneat  40665  llnle  40668  atcvrlln  40670  llncmp  40672  2llnmat  40674  2at0mat0  40675  2atm  40677  ps-2c  40678  lplnle  40690  lplnnle2at  40691  llncvrlpln2  40707  llncvrlpln  40708  2lplnmN  40709  2llnmj  40710  2atmat  40711  lplncmp  40712  lplnexllnN  40714  2llnm2N  40718  2llnm4  40720  lvolnle3at  40732  4atlem3a  40747  4atlem3b  40748  4atlem10  40756  4atlem11  40759  4atlem12  40762  lplncvrlvol2  40765  lplncvrlvol  40766  lvolcmp  40767  2lplnm2N  40771  2lplnmj  40772  dalempjsen  40803  dalemcea  40810  dalem2  40811  dalemdea  40812  dalem9  40822  dalem16  40829  dalemcjden  40842  dalem21  40844  dalem23  40846  dalem39  40861  dalem54  40876  dalem60  40882  cdlemb  40944  elpadd2at  40956  paddasslem4  40973  paddasslem7  40976  paddasslem15  40984  paddasslem16  40985  pmodlem1  40996  pmodlem2  40997  llnexchb2  41019  pclfinclN  41100  osumcllem9N  41114  pmapojoinN  41118  pexmidN  41119  pl42lem1N  41129  lhp0lt  41153  lhpexle1  41158  lhpexle2lem  41159  lhpexle3lem  41161  lhprelat3N  41190  ltrnid  41285  trlval3  41337  arglem1N  41340  cdlemc5  41345  cdleme3b  41379  cdleme3c  41380  cdleme3h  41385  cdleme7e  41397  cdleme7ga  41398  cdleme20l1  41470  cdleme20l2  41471  cdleme20l  41472  cdleme22b  41491  cdlemefrs29clN  41549  cdlemefrs32fva  41550  cdlemeg46fvcl  41656  cdlemeg46c  41663  cdlemeg46fvaw  41666  cdlemeg46req  41679  cdleme48fgv  41688  cdlemf1  41711  cdlemg1cex  41738  cdlemg2dN  41740  cdlemg2ce  41742  cdlemg12e  41797  cdlemg35  41863  cdlemh  41967  tendocan  41974  cdlemk28-3  42058  tendoex  42125  dih1  42436  dihmeetlem9N  42465  dihlspsnssN  42482  dihlspsnat  42483  lcfrlem23  42715  renegneg  43556  fsuppind  43711  3cubes  43793  mzpsubst  43852  rencldnfi  43921  irrapx1  43928  pellexlem3  43931  pellexlem5  43933  infmrgelbi  43978  pellqrex  43979  pellfundge  43982  rmspecfund  44009  congtr  44065  acongeq  44083  jm2.20nn  44097  jm2.25lem1  44098  jm2.26  44102  expdiophlem1  44121  hbtlem2  44219  cantnftermord  44415  suprleubrd  45259  suprlubrd  45261  suprnmpt  46282  wessf1ornlem  46293  mpct  46308  upbdrech  46414  ssfiunibd  46418  uzfissfz  46431  xleadd2d  46432  suprltrp  46433  xleadd1d  46434  suprleubrnmpt  46525  iccintsng  46628  limcrecl  46734  fnlimfvre  46777  dvmulcncf  47028  dvdivcncf  47030  dvbdfbdioolem1  47031  ioodvbdlimc1lem2  47035  ioodvbdlimc2lem  47037  stoweidlem1  47104  stoweidlem20  47123  stoweidlem24  47127  stoweidlem34  47137  stoweidlem45  47148  stoweidlem60  47163  fourierdlem20  47230  fourierdlem31  47241  fourierdlem38  47248  fourierdlem64  47273  fourierdlem79  47288  fourierdlem94  47303  fourierdlem113  47322  fouriersw  47334  fouriercn  47335  sge0isum  47530  hoicvr  47651  ovnsubaddlem2  47674  hoidmv1lelem1  47694  hoidmv1lelem3  47696  hoidmvlelem1  47698  hoidmvlelem4  47701  smflimlem2  47875  2timesltsq  48541  fmtnof1  48713  lighneallem2  48784  uspgrlim  49183  upgrwlkupwlk  49331  lincresunit3  49686  elbigolo1  49762