Theorem syl31anc 1485

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

Syntax hints:   → wi 4   ∧ wa 384   ∧ w3a 1100

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 198  df-an 385  df-3an 1102

This theorem is referenced by:  syl32anc  1490  stoic4b  1858  elovmpt3rab1  7117  smo11  7691  omeulem2  7894  oeeui  7913  oaabs2  7956  omabs  7958  omxpenlem  8294  map2xp  8363  mapdom2  8364  fsuppsssupp  8524  cantnflt  8810  cnfcom  8838  mapcdaen  9285  pwsdompw  9305  ackbij1lem5  9325  cofsmo  9370  fin1a2lem4  9504  ltmul12a  11158  lt2msq1  11186  ledivp1  11204  lemul1ad  11242  lemul2ad  11243  suprubd  11264  supaddc  11269  supadd  11270  supmul1  11271  supmul  11274  rpnnen1lem3  12029  rpnnen1lem5  12031  lediv2ad  12102  xaddge0  12300  xadddi  12337  xadddi2  12339  supicc  12537  supiccub  12538  supicclub  12539  difelfznle  12671  flval3  12834  expcan  13130  ltexp2  13131  ltexp2r  13134  expubnd  13138  ltexp2rd  13250  ltexp2d  13255  leexp2d  13256  expcand  13257  hashmap  13433  swrdid  13646  swrd0fv  13657  swrds1  13669  ccatswrd  13674  swrdccat2  13676  swrdccatin2  13705  swrdccatin12lem2  13707  swrdccatin12lem3  13708  splfv1  13724  cshwidxmod  13767  wrdl3s3  13924  o1fsum  14761  mertenslem1  14831  eftlub  15053  rpnnen2lem4  15160  ruclem12  15184  dvdsadd  15241  3dvds  15269  divalgmod  15343  bitsmod  15371  bitsinv1lem  15376  bezoutlem4  15472  gcdzeq  15484  rplpwr  15489  sqgcd  15491  bezoutr  15494  rpmulgcd2  15582  rpdvds  15586  coprmproddvdslem  15588  isprm5  15630  divgcdodd  15633  divnumden  15667  crth  15694  phimullem  15695  modprm0  15721  modprmn0modprm0  15723  coprimeprodsq2  15725  pythagtriplem19  15749  pockthlem  15820  prmunb  15829  prmreclem3  15833  prmreclem6  15836  ramub  15928  ramz  15940  pmtrprfv  18068  pmtrprfv3  18069  mndodcong  18156  odngen  18187  pgpfi  18215  pgpssslw  18224  sylow2blem3  18232  lsmless1  18269  lsmless2  18270  lsmless12  18271  lsmmod2  18284  pj1id  18307  odadd2  18447  gexexlem  18450  ablfacrplem  18660  ablfacrp  18661  ablfac1b  18665  ablfac1eu  18668  pgpfac1lem2  18670  kerf1hrm  18941  lsmssspx  19289  lspsncv0  19348  lspsncv0OLD  19349  coe1subfv  19838  coe1fzgsumdlem  19873  znunit  20113  uvcvvcl2  20331  uvcvv1  20332  uvcvv0  20333  scmate  20521  mdetunilem2  20624  pmatcoe1fsupp  20713  mat2pmatlin  20747  decpmatmullem  20783  pmatcollpw1lem1  20786  pmatcollpw1lem2  20787  pm2mpghm  20828  chpscmat  20854  chp0mat  20858  chpidmat  20859  cpmadugsumlemB  20886  cpmadugsumlemC  20887  cpmadugsumlemF  20888  clsndisj  21087  neiptopnei  21144  rnelfm  21964  fmfnfmlem2  21966  fmfnfm  21969  flimss1  21984  isfcf  22045  cnextfun  22075  cnextfvval  22076  cnextf  22077  cnextcn  22078  cnextfres1  22079  ustuqtop1  22252  utopsnneiplem  22258  xblss2ps  22413  xblss2  22414  stdbdxmet  22527  metcnpi3  22558  metustexhalf  22568  nmoi  22739  nmoi2  22741  nmoco  22748  blcvx  22808  icccmplem2  22833  icccmplem3  22834  reconnlem2  22837  xrge0gsumle  22843  metds0  22860  metdstri  22861  metdseq0  22864  lebnumlem3  22969  nmoleub2lem  23120  bcthlem5  23331  minveclem2  23403  minveclem3b  23405  minveclem4  23409  minveclem6  23411  icombl  23539  cncombf  23633  mbflimsup  23641  itg2monolem1  23725  itg2mono  23728  itg2cnlem1  23736  itg2cnlem2  23737  bddmulibl  23813  ellimc2  23849  cpnord  23906  cpnres  23908  dvmulbr  23910  dvcobr  23917  dvlipcn  23965  dvlip2  23966  c1liplem1  23967  dvivthlem1  23979  lhop1lem  23984  lhop1  23985  dvfsumlem2  23998  itgsubstlem  24019  deg1add  24071  deg1sublt  24078  ply1remlem  24130  plyeq0lem  24174  taylthlem2  24336  ulmdvlem3  24364  abelthlem7  24400  pilem2  24414  pilem3  24415  pilem3OLD  24416  pige3  24478  logccv  24617  cxpaddlelem  24700  cvxcl  24919  fsumharmonic  24946  ftalem5  25011  dvdsmulf1o  25128  bposlem1  25217  lgsqr  25284  lgsquad2lem2  25318  2lgsoddprmlem1  25341  2sqlem8a  25358  2sqlem8  25359  dchrmusum2  25391  dchrvmasumiflem1  25398  dchrisum0flblem1  25405  dchrisum0lem1b  25412  pntlem3  25506  tgdim01  25610  axsegcon  26015  ax5seglem1  26016  ax5seglem2  26017  axlowdimlem6  26035  axeuclidlem  26050  axcontlem7  26058  axcontlem9  26060  axcontlem10  26061  nbupgr  26450  nbumgrvtx  26452  cusgrsize2inds  26571  upgriswlk  26759  2pthnloop  26849  clwwlknonex2lem2  27271  numclwwlk2lem1  27550  numclwwlk2lem1OLD  27557  frgrreg  27576  nmoub3i  27950  ubthlem3  28050  minvecolem2  28053  minvecolem4  28058  minvecolem5  28059  minvecolem6  28060  htthlem  28096  pjpjpre  28600  chscllem1  28818  chscllem2  28819  chscllem3  28820  cnlnadjlem2  29249  leopnmid  29319  br8d  29741  ogrpaddlt  30037  archirngz  30062  ornglmullt  30126  orngrmullt  30127  elrhmunit  30139  qqhval2lem  30344  qqhnm  30353  qqhucn  30355  esumcst  30444  esumpcvgval  30459  measunl  30598  dya2iocbrsiga  30656  dya2icobrsiga  30657  omssubadd  30681  inelcarsg  30692  carsgclctunlem2  30700  sibfof  30721  sitgaddlemb  30729  oddpwdc  30735  eulerpartlemgc  30743  bayesth  30820  ftc2re  30995  breprexplemc  31029  tgoldbachgt  31060  erdszelem8  31497  br8  31962  noetalem3  32180  noetalem5  32182  matunitlindflem2  33713  totbndbnd  33893  prdsbnd  33897  rrncmslem  33936  rrntotbnd  33940  isdrngo2  34062  lsatcmp  34777  lcvexchlem2  34809  lcvexchlem3  34810  ncvr1  35046  cvrletrN  35047  cvrnbtwn3  35050  cvrnrefN  35056  cvrcmp  35057  0ltat  35065  atnle0  35083  atlen0  35084  cvlcvr1  35113  cvrval3  35187  atle  35210  athgt  35230  1cvratex  35247  ps-2  35252  ps-2b  35256  llnnleat  35287  2atneat  35289  llnle  35292  atcvrlln  35294  llncmp  35296  2llnmat  35298  2at0mat0  35299  2atm  35301  ps-2c  35302  lplnle  35314  lplnnle2at  35315  llncvrlpln2  35331  llncvrlpln  35332  2lplnmN  35333  2llnmj  35334  2atmat  35335  lplncmp  35336  lplnexllnN  35338  2llnm2N  35342  2llnm4  35344  lvolnle3at  35356  4atlem3a  35371  4atlem3b  35372  4atlem10  35380  4atlem11  35383  4atlem12  35386  lplncvrlvol2  35389  lplncvrlvol  35390  lvolcmp  35391  2lplnm2N  35395  2lplnmj  35396  dalempjsen  35427  dalemcea  35434  dalem2  35435  dalemdea  35436  dalem9  35446  dalem16  35453  dalemcjden  35466  dalem21  35468  dalem23  35470  dalem39  35485  dalem54  35500  dalem60  35506  cdlemb  35568  elpadd2at  35580  paddasslem4  35597  paddasslem7  35600  paddasslem15  35608  paddasslem16  35609  pmodlem1  35620  pmodlem2  35621  llnexchb2  35643  pclfinclN  35724  osumcllem9N  35738  pmapojoinN  35742  pexmidN  35743  pl42lem1N  35753  lhp0lt  35777  lhpexle1  35782  lhpexle2lem  35783  lhpexle3lem  35785  lhprelat3N  35814  ltrnid  35909  trlval3  35962  arglem1N  35965  cdlemc5  35970  cdleme3b  36004  cdleme3c  36005  cdleme3h  36010  cdleme7e  36022  cdleme7ga  36023  cdleme20l1  36095  cdleme20l2  36096  cdleme20l  36097  cdleme22b  36116  cdlemefrs29clN  36174  cdlemefrs32fva  36175  cdlemeg46fvcl  36281  cdlemeg46c  36288  cdlemeg46fvaw  36291  cdlemeg46req  36304  cdleme48fgv  36313  cdlemf1  36336  cdlemg1cex  36363  cdlemg2dN  36365  cdlemg2ce  36367  cdlemg12e  36422  cdlemg35  36488  cdlemh  36592  tendocan  36599  cdlemk28-3  36683  tendoex  36750  dih1  37061  dihmeetlem9N  37090  dihlspsnssN  37107  dihlspsnat  37108  lcfrlem23  37340  mzpsubst  37807  rencldnfi  37881  irrapx1  37888  pellexlem3  37891  pellexlem5  37893  infmrgelbi  37938  pellqrex  37939  pellfundge  37942  rmspecfund  37969  congtr  38027  acongeq  38045  jm2.20nn  38059  jm2.25lem1  38060  jm2.26  38064  expdiophlem1  38083  hbtlem2  38189  suprleubrd  38960  suprlubrd  38964  suprnmpt  39838  wessf1ornlem  39854  mpct  39874  upbdrech  39994  ssfiunibd  39998  uzfissfz  40016  xleadd2d  40017  suprltrp  40018  xleadd1d  40019  suprleubrnmpt  40122  iccintsng  40224  limcrecl  40335  fnlimfvre  40380  dvmulcncf  40614  dvdivcncf  40616  dvbdfbdioolem1  40617  ioodvbdlimc1lem2  40621  ioodvbdlimc2lem  40623  stoweidlem1  40691  stoweidlem20  40710  stoweidlem24  40714  stoweidlem34  40724  stoweidlem45  40735  stoweidlem60  40750  fourierdlem20  40817  fourierdlem31  40828  fourierdlem38  40835  fourierdlem64  40860  fourierdlem79  40875  fourierdlem94  40890  fourierdlem113  40909  fouriersw  40921  fouriercn  40922  sge0isum  41117  hoicvr  41238  ovnsubaddlem2  41261  hoidmv1lelem1  41281  hoidmv1lelem3  41283  hoidmvlelem1  41285  hoidmvlelem4  41288  smflimlem2  41456  pfxfv  41968  fmtnof1  42016  lighneallem2  42092  upgrwlkupwlk  42283  lincresunit3  42832  elbigolo1  42913