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

Syntax hints:   → wi 4   ∧ wa 394   ∧ 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 395  df-3an 1086

This theorem is referenced by:  syl32anc  1375  stoic4b  1772  elovmpt3rab1  7676  smo11  8381  omeulem2  8600  oeeui  8619  oaabs2  8666  omabs  8668  omxpenlem  9094  map2xp  9168  mapdom2  9169  fsuppsssupp  9402  cantnflt  9693  cnfcom  9721  mapdjuen  10201  pwsdompw  10225  ackbij1lem5  10245  cofsmo  10290  fin1a2lem4  10424  ltmul12a  12098  lt2msq1  12126  ledivp1  12144  lemul1ad  12181  lemul2ad  12182  suprubd  12204  supaddc  12209  supadd  12210  supmul1  12211  supmul  12214  rpnnen1lem3  12991  rpnnen1lem5  12993  lediv2ad  13068  xaddge0  13267  xadddi  13304  xadddi2  13306  supicc  13508  supicclub  13510  difelfznle  13645  flval3  13810  expcan  14163  ltexp2  14164  ltexp2r  14167  expubnd  14171  ltexp2rd  14240  ltexp2d  14243  leexp2d  14244  expcand  14245  hashmap  14424  swrds1  14646  ccatswrd  14648  pfxfv  14662  swrdccatin1  14705  pfxccatin12lem3  14712  cshwidxmod  14783  wrdl3s3  14943  o1fsum  15789  mertenslem1  15860  eftlub  16083  rpnnen2lem4  16191  ruclem12  16215  dvdsadd  16276  3dvds  16305  divalgmod  16380  bitsmod  16408  bitsinv1lem  16413  bezoutlem4  16515  gcdzeq  16525  rplpwr  16530  sqgcd  16533  rpmulgcd2  16624  rpdvds  16628  coprmproddvdslem  16630  isprm5  16675  divgcdodd  16678  dvdszzq  16690  divnumden  16717  crth  16744  phimullem  16745  modprm0  16771  modprmn0modprm0  16773  coprimeprodsq2  16775  pythagtriplem19  16799  pockthlem  16871  prmunb  16880  prmreclem3  16884  prmreclem6  16887  ramub  16979  ramz  16991  kerf1ghm  19203  pmtrprfv  19410  pmtrprfv3  19411  mndodcong  19499  odngen  19534  pgpfi  19562  sylow2blem3  19579  lsmless1  19617  lsmless2  19618  lsmless12  19619  lsmmod2  19633  pj1id  19656  odadd2  19806  gexexlem  19809  ablfacrplem  20024  ablfacrp  20025  ablfac1b  20029  ablfac1eu  20032  pgpfac1lem2  20034  elrhmunit  20451  lsmssspx  20975  lspsncv0  21036  znunit  21499  uvcvvcl2  21724  uvcvv1  21725  uvcvv0  21726  coe1subfv  22192  coe1fzgsumdlem  22229  scmate  22428  mdetunilem2  22531  pmatcoe1fsupp  22619  mat2pmatlin  22653  decpmatmullem  22689  pmatcollpw1lem1  22692  pmatcollpw1lem2  22693  pm2mpghm  22734  chpscmat  22760  chp0mat  22764  chpidmat  22765  cpmadugsumlemB  22792  cpmadugsumlemC  22793  cpmadugsumlemF  22794  clsndisj  22995  neiptopnei  23052  rnelfm  23873  fmfnfmlem2  23875  fmfnfm  23878  flimss1  23893  isfcf  23954  cnextfun  23984  cnextfvval  23985  cnextf  23986  cnextcn  23987  cnextfres1  23988  ustuqtop1  24162  utopsnneiplem  24168  xblss2ps  24323  xblss2  24324  stdbdxmet  24440  metcnpi3  24471  metustexhalf  24481  nmoi  24661  nmoi2  24663  nmoco  24670  blcvx  24730  icccmplem2  24755  icccmplem3  24756  reconnlem2  24759  xrge0gsumle  24765  metds0  24782  metdstri  24783  metdseq0  24786  lebnumlem3  24905  nmoleub2lem  25057  bcthlem5  25272  csschl  25320  minveclem2  25370  minveclem3b  25372  minveclem4  25376  minveclem6  25378  icombl  25509  cncombf  25603  mbflimsup  25611  itg2monolem1  25696  itg2cnlem1  25707  itg2cnlem2  25708  bddmulibl  25784  ellimc2  25822  cpnord  25881  cpnres  25883  dvmulbr  25885  dvmulbrOLD  25886  dvcobr  25893  dvcobrOLD  25894  dvlipcn  25943  dvlip2  25944  dvivthlem1  25957  lhop1lem  25962  lhop1  25963  dvfsumlem2  25977  dvfsumlem2OLD  25978  itgsubstlem  25999  deg1add  26055  deg1sublt  26062  ply1remlem  26115  plyeq0lem  26160  taylthlem2  26325  taylthlem2OLD  26326  ulmdvlem3  26354  abelthlem7  26391  pilem2  26405  pilem3  26406  pige3ALT  26470  logccv  26613  cxpaddlelem  26702  cvxcl  26933  fsumharmonic  26960  ftalem5  27025  mpodvdsmulf1o  27142  dvdsmulf1o  27144  bposlem1  27233  lgsqr  27300  lgsquad2lem2  27334  2lgsoddprmlem1  27357  2sqlem8a  27374  2sqlem8  27375  dchrmusum2  27443  dchrvmasumiflem1  27450  dchrisum0flblem1  27457  dchrisum0lem1b  27464  pntlem3  27558  noetasuplem4  27685  noetainflem4  27689  noetalem1  27690  divsmulwd  28109  divsclwd  28111  tgdim01  28327  axsegcon  28754  ax5seglem1  28755  ax5seglem2  28756  axlowdimlem6  28774  axeuclidlem  28789  axcontlem7  28797  axcontlem9  28799  axcontlem10  28800  nbupgr  29173  nbumgrvtx  29175  cusgrsize2inds  29283  upgriswlk  29471  2pthnloop  29561  numclwwlk2lem1  30202  frgrreg  30220  nmoub3i  30599  ubthlem3  30698  minvecolem2  30701  minvecolem4  30706  minvecolem5  30707  minvecolem6  30708  htthlem  30743  pjpjpre  31245  chscllem1  31463  chscllem2  31464  chscllem3  31465  cnlnadjlem2  31894  leopnmid  31964  br8d  32417  swrdf1  32694  splfv3  32696  ogrpaddlt  32814  symgcom2  32824  cyc3genpmlem  32889  archirngz  32914  rrgnz  32970  subrdom  32973  rlocf1  33008  ornglmullt  33042  orngrmullt  33043  dvdsruasso  33110  unitpidl1  33160  elrspunidl  33165  qsidomlem1  33189  mxidlirredi  33205  ply1gsumz  33298  lssdimle  33334  dimkerim  33354  fedgmullem2  33357  fedgmul  33358  minplyirred  33410  irredminply  33413  algextdeglem2  33415  qqhval2lem  33611  qqhnm  33620  qqhucn  33622  esumcst  33711  esumpcvgval  33726  measunl  33864  dya2iocbrsiga  33924  dya2icobrsiga  33925  omssubadd  33949  inelcarsg  33960  carsgclctunlem2  33968  sibfof  33989  sitgaddlemb  33997  oddpwdc  34003  eulerpartlemgc  34011  bayesth  34088  ftc2re  34259  breprexplemc  34293  tgoldbachgt  34324  erdszelem8  34837  2goelgoanfmla1  35063  br8  35379  matunitlindflem2  37119  totbndbnd  37291  prdsbnd  37295  rrncmslem  37334  rrntotbnd  37338  isdrngo2  37460  lsatcmp  38503  lcvexchlem2  38535  lcvexchlem3  38536  ncvr1  38772  cvrletrN  38773  cvrnbtwn3  38776  cvrnrefN  38782  cvrcmp  38783  0ltat  38791  atnle0  38809  atlen0  38810  cvlcvr1  38839  cvrval3  38914  atle  38937  athgt  38957  1cvratex  38974  ps-2  38979  ps-2b  38983  llnnleat  39014  2atneat  39016  llnle  39019  atcvrlln  39021  llncmp  39023  2llnmat  39025  2at0mat0  39026  2atm  39028  ps-2c  39029  lplnle  39041  lplnnle2at  39042  llncvrlpln2  39058  llncvrlpln  39059  2lplnmN  39060  2llnmj  39061  2atmat  39062  lplncmp  39063  lplnexllnN  39065  2llnm2N  39069  2llnm4  39071  lvolnle3at  39083  4atlem3a  39098  4atlem3b  39099  4atlem10  39107  4atlem11  39110  4atlem12  39113  lplncvrlvol2  39116  lplncvrlvol  39117  lvolcmp  39118  2lplnm2N  39122  2lplnmj  39123  dalempjsen  39154  dalemcea  39161  dalem2  39162  dalemdea  39163  dalem9  39173  dalem16  39180  dalemcjden  39193  dalem21  39195  dalem23  39197  dalem39  39212  dalem54  39227  dalem60  39233  cdlemb  39295  elpadd2at  39307  paddasslem4  39324  paddasslem7  39327  paddasslem15  39335  paddasslem16  39336  pmodlem1  39347  pmodlem2  39348  llnexchb2  39370  pclfinclN  39451  osumcllem9N  39465  pmapojoinN  39469  pexmidN  39470  pl42lem1N  39480  lhp0lt  39504  lhpexle1  39509  lhpexle2lem  39510  lhpexle3lem  39512  lhprelat3N  39541  ltrnid  39636  trlval3  39688  arglem1N  39691  cdlemc5  39696  cdleme3b  39730  cdleme3c  39731  cdleme3h  39736  cdleme7e  39748  cdleme7ga  39749  cdleme20l1  39821  cdleme20l2  39822  cdleme20l  39823  cdleme22b  39842  cdlemefrs29clN  39900  cdlemefrs32fva  39901  cdlemeg46fvcl  40007  cdlemeg46c  40014  cdlemeg46fvaw  40017  cdlemeg46req  40030  cdleme48fgv  40039  cdlemf1  40062  cdlemg1cex  40089  cdlemg2dN  40091  cdlemg2ce  40093  cdlemg12e  40148  cdlemg35  40214  cdlemh  40318  tendocan  40325  cdlemk28-3  40409  tendoex  40476  dih1  40787  dihmeetlem9N  40816  dihlspsnssN  40833  dihlspsnat  40834  lcfrlem23  41066  3rspcedvdw  41730  fsuppind  41860  expgcd  41931  renegneg  42003  flt4lem4  42110  3cubes  42147  mzpsubst  42205  rencldnfi  42278  irrapx1  42285  pellexlem3  42288  pellexlem5  42290  infmrgelbi  42335  pellqrex  42336  pellfundge  42339  rmspecfund  42366  congtr  42423  acongeq  42441  jm2.20nn  42455  jm2.25lem1  42456  jm2.26  42460  expdiophlem1  42479  hbtlem2  42585  cantnftermord  42786  suprleubrd  43633  suprlubrd  43635  suprnmpt  44583  wessf1ornlem  44594  mpct  44610  upbdrech  44722  ssfiunibd  44726  uzfissfz  44743  xleadd2d  44744  suprltrp  44745  xleadd1d  44746  suprleubrnmpt  44839  iccintsng  44943  limcrecl  45052  fnlimfvre  45097  dvmulcncf  45348  dvdivcncf  45350  dvbdfbdioolem1  45351  ioodvbdlimc1lem2  45355  ioodvbdlimc2lem  45357  stoweidlem1  45424  stoweidlem20  45443  stoweidlem24  45447  stoweidlem34  45457  stoweidlem45  45468  stoweidlem60  45483  fourierdlem20  45550  fourierdlem31  45561  fourierdlem38  45568  fourierdlem64  45593  fourierdlem79  45608  fourierdlem94  45623  fourierdlem113  45642  fouriersw  45654  fouriercn  45655  sge0isum  45850  hoicvr  45971  ovnsubaddlem2  45994  hoidmv1lelem1  46014  hoidmv1lelem3  46016  hoidmvlelem1  46018  hoidmvlelem4  46021  smflimlem2  46195  fmtnof1  46910  lighneallem2  46981  upgrwlkupwlk  47286  lincresunit3  47633  elbigolo1  47714  eenglngeehlnm  47896