Theorem syl31anc 1371

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

Syntax hints:   → wi 4   ∧ wa 394   ∧ w3a 1085

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 1087

This theorem is referenced by:  syl32anc  1376  stoic4b  1778  elovmpt3rab1  7668  smo11  8366  omeulem2  8585  oeeui  8604  oaabs2  8650  omabs  8652  omxpenlem  9075  map2xp  9149  mapdom2  9150  fsuppsssupp  9381  cantnflt  9669  cnfcom  9697  mapdjuen  10177  pwsdompw  10201  ackbij1lem5  10221  cofsmo  10266  fin1a2lem4  10400  ltmul12a  12074  lt2msq1  12102  ledivp1  12120  lemul1ad  12157  lemul2ad  12158  suprubd  12180  supaddc  12185  supadd  12186  supmul1  12187  supmul  12190  rpnnen1lem3  12967  rpnnen1lem5  12969  lediv2ad  13042  xaddge0  13241  xadddi  13278  xadddi2  13280  supicc  13482  supicclub  13484  difelfznle  13619  flval3  13784  expcan  14138  ltexp2  14139  ltexp2r  14142  expubnd  14146  ltexp2rd  14215  ltexp2d  14218  leexp2d  14219  expcand  14220  hashmap  14399  swrds1  14620  ccatswrd  14622  pfxfv  14636  swrdccatin1  14679  pfxccatin12lem3  14686  cshwidxmod  14757  wrdl3s3  14917  o1fsum  15763  mertenslem1  15834  eftlub  16056  rpnnen2lem4  16164  ruclem12  16188  dvdsadd  16249  3dvds  16278  divalgmod  16353  bitsmod  16381  bitsinv1lem  16386  bezoutlem4  16488  gcdzeq  16498  rplpwr  16503  sqgcd  16506  rpmulgcd2  16597  rpdvds  16601  coprmproddvdslem  16603  isprm5  16648  divgcdodd  16651  divnumden  16688  crth  16715  phimullem  16716  modprm0  16742  modprmn0modprm0  16744  coprimeprodsq2  16746  pythagtriplem19  16770  pockthlem  16842  prmunb  16851  prmreclem3  16855  prmreclem6  16858  ramub  16950  ramz  16962  kerf1ghm  19161  pmtrprfv  19362  pmtrprfv3  19363  mndodcong  19451  odngen  19486  pgpfi  19514  sylow2blem3  19531  lsmless1  19569  lsmless2  19570  lsmless12  19571  lsmmod2  19585  pj1id  19608  odadd2  19758  gexexlem  19761  ablfacrplem  19976  ablfacrp  19977  ablfac1b  19981  ablfac1eu  19984  pgpfac1lem2  19986  elrhmunit  20401  lsmssspx  20843  lspsncv0  20904  znunit  21338  uvcvvcl2  21562  uvcvv1  21563  uvcvv0  21564  coe1subfv  22008  coe1fzgsumdlem  22045  scmate  22232  mdetunilem2  22335  pmatcoe1fsupp  22423  mat2pmatlin  22457  decpmatmullem  22493  pmatcollpw1lem1  22496  pmatcollpw1lem2  22497  pm2mpghm  22538  chpscmat  22564  chp0mat  22568  chpidmat  22569  cpmadugsumlemB  22596  cpmadugsumlemC  22597  cpmadugsumlemF  22598  clsndisj  22799  neiptopnei  22856  rnelfm  23677  fmfnfmlem2  23679  fmfnfm  23682  flimss1  23697  isfcf  23758  cnextfun  23788  cnextfvval  23789  cnextf  23790  cnextcn  23791  cnextfres1  23792  ustuqtop1  23966  utopsnneiplem  23972  xblss2ps  24127  xblss2  24128  stdbdxmet  24244  metcnpi3  24275  metustexhalf  24285  nmoi  24465  nmoi2  24467  nmoco  24474  blcvx  24534  icccmplem2  24559  icccmplem3  24560  reconnlem2  24563  xrge0gsumle  24569  metds0  24586  metdstri  24587  metdseq0  24590  lebnumlem3  24709  nmoleub2lem  24861  bcthlem5  25076  csschl  25124  minveclem2  25174  minveclem3b  25176  minveclem4  25180  minveclem6  25182  icombl  25313  cncombf  25407  mbflimsup  25415  itg2monolem1  25500  itg2cnlem1  25511  itg2cnlem2  25512  bddmulibl  25588  ellimc2  25626  cpnord  25685  cpnres  25687  dvmulbr  25689  dvmulbrOLD  25690  dvcobr  25697  dvcobrOLD  25698  dvlipcn  25746  dvlip2  25747  dvivthlem1  25760  lhop1lem  25765  lhop1  25766  dvfsumlem2  25779  itgsubstlem  25800  deg1add  25856  deg1sublt  25863  ply1remlem  25915  plyeq0lem  25959  taylthlem2  26122  ulmdvlem3  26150  abelthlem7  26186  pilem2  26200  pilem3  26201  pige3ALT  26265  logccv  26407  cxpaddlelem  26495  cvxcl  26725  fsumharmonic  26752  ftalem5  26817  dvdsmulf1o  26934  bposlem1  27023  lgsqr  27090  lgsquad2lem2  27124  2lgsoddprmlem1  27147  2sqlem8a  27164  2sqlem8  27165  dchrmusum2  27233  dchrvmasumiflem1  27240  dchrisum0flblem1  27247  dchrisum0lem1b  27254  pntlem3  27348  noetasuplem4  27475  noetainflem4  27479  noetalem1  27480  divsmulwd  27880  divsclwd  27882  tgdim01  28025  axsegcon  28452  ax5seglem1  28453  ax5seglem2  28454  axlowdimlem6  28472  axeuclidlem  28487  axcontlem7  28495  axcontlem9  28497  axcontlem10  28498  nbupgr  28868  nbumgrvtx  28870  cusgrsize2inds  28977  upgriswlk  29165  2pthnloop  29255  numclwwlk2lem1  29896  frgrreg  29914  nmoub3i  30293  ubthlem3  30392  minvecolem2  30395  minvecolem4  30400  minvecolem5  30401  minvecolem6  30402  htthlem  30437  pjpjpre  30939  chscllem1  31157  chscllem2  31158  chscllem3  31159  cnlnadjlem2  31588  leopnmid  31658  br8d  32106  dvdszzq  32288  swrdf1  32387  splfv3  32389  ogrpaddlt  32505  symgcom2  32515  cyc3genpmlem  32580  archirngz  32605  ornglmullt  32695  orngrmullt  32696  dvdsruasso  32764  unitpidl1  32816  elrspunidl  32820  qsidomlem1  32845  mxidlirredi  32861  ply1gsumz  32944  lssdimle  32980  dimkerim  33000  fedgmullem2  33003  fedgmul  33004  minplyirred  33059  algextdeglem2  33063  qqhval2lem  33259  qqhnm  33268  qqhucn  33270  esumcst  33359  esumpcvgval  33374  measunl  33512  dya2iocbrsiga  33572  dya2icobrsiga  33573  omssubadd  33597  inelcarsg  33608  carsgclctunlem2  33616  sibfof  33637  sitgaddlemb  33645  oddpwdc  33651  eulerpartlemgc  33659  bayesth  33736  ftc2re  33908  breprexplemc  33942  tgoldbachgt  33973  erdszelem8  34487  2goelgoanfmla1  34713  br8  35030  gg-dvfsumlem2  35469  matunitlindflem2  36788  totbndbnd  36960  prdsbnd  36964  rrncmslem  37003  rrntotbnd  37007  isdrngo2  37129  lsatcmp  38176  lcvexchlem2  38208  lcvexchlem3  38209  ncvr1  38445  cvrletrN  38446  cvrnbtwn3  38449  cvrnrefN  38455  cvrcmp  38456  0ltat  38464  atnle0  38482  atlen0  38483  cvlcvr1  38512  cvrval3  38587  atle  38610  athgt  38630  1cvratex  38647  ps-2  38652  ps-2b  38656  llnnleat  38687  2atneat  38689  llnle  38692  atcvrlln  38694  llncmp  38696  2llnmat  38698  2at0mat0  38699  2atm  38701  ps-2c  38702  lplnle  38714  lplnnle2at  38715  llncvrlpln2  38731  llncvrlpln  38732  2lplnmN  38733  2llnmj  38734  2atmat  38735  lplncmp  38736  lplnexllnN  38738  2llnm2N  38742  2llnm4  38744  lvolnle3at  38756  4atlem3a  38771  4atlem3b  38772  4atlem10  38780  4atlem11  38783  4atlem12  38786  lplncvrlvol2  38789  lplncvrlvol  38790  lvolcmp  38791  2lplnm2N  38795  2lplnmj  38796  dalempjsen  38827  dalemcea  38834  dalem2  38835  dalemdea  38836  dalem9  38846  dalem16  38853  dalemcjden  38866  dalem21  38868  dalem23  38870  dalem39  38885  dalem54  38900  dalem60  38906  cdlemb  38968  elpadd2at  38980  paddasslem4  38997  paddasslem7  39000  paddasslem15  39008  paddasslem16  39009  pmodlem1  39020  pmodlem2  39021  llnexchb2  39043  pclfinclN  39124  osumcllem9N  39138  pmapojoinN  39142  pexmidN  39143  pl42lem1N  39153  lhp0lt  39177  lhpexle1  39182  lhpexle2lem  39183  lhpexle3lem  39185  lhprelat3N  39214  ltrnid  39309  trlval3  39361  arglem1N  39364  cdlemc5  39369  cdleme3b  39403  cdleme3c  39404  cdleme3h  39409  cdleme7e  39421  cdleme7ga  39422  cdleme20l1  39494  cdleme20l2  39495  cdleme20l  39496  cdleme22b  39515  cdlemefrs29clN  39573  cdlemefrs32fva  39574  cdlemeg46fvcl  39680  cdlemeg46c  39687  cdlemeg46fvaw  39690  cdlemeg46req  39703  cdleme48fgv  39712  cdlemf1  39735  cdlemg1cex  39762  cdlemg2dN  39764  cdlemg2ce  39766  cdlemg12e  39821  cdlemg35  39887  cdlemh  39991  tendocan  39998  cdlemk28-3  40082  tendoex  40149  dih1  40460  dihmeetlem9N  40489  dihlspsnssN  40506  dihlspsnat  40507  lcfrlem23  40739  3rspcedvdw  41336  fsuppind  41464  expgcd  41527  renegneg  41586  flt4lem4  41693  3cubes  41730  mzpsubst  41788  rencldnfi  41861  irrapx1  41868  pellexlem3  41871  pellexlem5  41873  infmrgelbi  41918  pellqrex  41919  pellfundge  41922  rmspecfund  41949  congtr  42006  acongeq  42024  jm2.20nn  42038  jm2.25lem1  42039  jm2.26  42043  expdiophlem1  42062  hbtlem2  42168  cantnftermord  42372  suprleubrd  43220  suprlubrd  43222  suprnmpt  44171  wessf1ornlem  44182  mpct  44198  upbdrech  44313  ssfiunibd  44317  uzfissfz  44334  xleadd2d  44335  suprltrp  44336  xleadd1d  44337  suprleubrnmpt  44430  iccintsng  44534  limcrecl  44643  fnlimfvre  44688  dvmulcncf  44939  dvdivcncf  44941  dvbdfbdioolem1  44942  ioodvbdlimc1lem2  44946  ioodvbdlimc2lem  44948  stoweidlem1  45015  stoweidlem20  45034  stoweidlem24  45038  stoweidlem34  45048  stoweidlem45  45059  stoweidlem60  45074  fourierdlem20  45141  fourierdlem31  45152  fourierdlem38  45159  fourierdlem64  45184  fourierdlem79  45199  fourierdlem94  45214  fourierdlem113  45233  fouriersw  45245  fouriercn  45246  sge0isum  45441  hoicvr  45562  ovnsubaddlem2  45585  hoidmv1lelem1  45605  hoidmv1lelem3  45607  hoidmvlelem1  45609  hoidmvlelem4  45612  smflimlem2  45786  fmtnof1  46501  lighneallem2  46572  upgrwlkupwlk  46816  lincresunit3  47249  elbigolo1  47330  eenglngeehlnm  47512