Theorem syl31anc 1381

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

Syntax hints:   → wi 4   ∧ wa 396   ∧ w3a 1092

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 208  df-an 397  df-3an 1094

This theorem is referenced by:  syl32anc  1386  stoic4b  1785  3rspcedvdw  3585  elovmpt3rab1  7623  smo11  8301  omeulem2  8515  oeeui  8535  oaabs2  8582  omabs  8584  omxpenlem  9013  map2xp  9082  mapdom2  9083  fsuppsssupp  9291  cantnflt  9591  cnfcom  9619  mapdjuen  10101  pwsdompw  10123  ackbij1lem5  10143  cofsmo  10189  fin1a2lem4  10323  ltmul12a  12009  lt2msq1  12038  ledivp1  12056  lemul1ad  12093  lemul2ad  12094  suprubd  12116  supaddc  12121  supadd  12122  supmul1  12123  supmul  12126  rpnnen1lem3  12927  rpnnen1lem5  12929  lediv2ad  13006  xaddge0  13208  xadddi  13245  xadddi2  13247  supicc  13452  supicclub  13454  difelfznle  13594  flval3  13772  expcan  14129  ltexp2  14130  ltexp2r  14133  expubnd  14138  ltexp2rd  14208  ltexp2d  14211  leexp2d  14212  expcand  14213  hashmap  14395  swrds1  14627  ccatswrd  14629  pfxfv  14643  swrdccatin1  14685  pfxccatin12lem3  14692  cshwidxmod  14763  wrdl3s3  14922  o1fsum  15774  mertenslem1  15847  eftlub  16074  rpnnen2lem4  16182  ruclem12  16206  dvdsadd  16269  3dvds  16298  divalgmod  16373  bitsmod  16403  bitsinv1lem  16408  bezoutlem4  16509  gcdzeq  16519  rplpwr  16525  sqgcd  16529  expgcd  16530  rpmulgcd2  16623  rpdvds  16627  coprmproddvdslem  16629  isprm5  16675  divgcdodd  16678  dvdszzq  16689  divnumden  16716  crth  16746  phimullem  16747  modprm0  16774  modprmn0modprm0  16776  coprimeprodsq2  16778  pythagtriplem19  16802  pockthlem  16874  prmunb  16883  prmreclem3  16887  prmreclem6  16890  ramub  16982  ramz  16994  kerf1ghm  19220  pmtrprfv  19426  pmtrprfv3  19427  mndodcong  19515  odngen  19550  pgpfi  19578  sylow2blem3  19595  lsmless1  19633  lsmless2  19634  lsmless12  19635  lsmmod2  19649  pj1id  19672  odadd2  19822  gexexlem  19825  ablfacrplem  20040  ablfacrp  20041  ablfac1b  20045  ablfac1eu  20048  pgpfac1lem2  20050  ogrpaddlt  20111  elrhmunit  20489  rrgnz  20683  ornglmullt  20848  orngrmullt  20849  lsmssspx  21085  lspsncv0  21146  znunit  21545  uvcvvcl2  21770  uvcvv1  21771  uvcvv0  21772  coe1subfv  22259  coe1fzgsumdlem  22296  scmate  22500  mdetunilem2  22603  pmatcoe1fsupp  22691  mat2pmatlin  22725  decpmatmullem  22761  pmatcollpw1lem1  22764  pmatcollpw1lem2  22765  pm2mpghm  22806  chpscmat  22832  chp0mat  22836  chpidmat  22837  cpmadugsumlemB  22864  cpmadugsumlemC  22865  cpmadugsumlemF  22866  clsndisj  23065  neiptopnei  23122  rnelfm  23943  fmfnfmlem2  23945  fmfnfm  23948  flimss1  23963  isfcf  24024  cnextfun  24054  cnextfvval  24055  cnextf  24056  cnextcn  24057  cnextfres1  24058  ustuqtop1  24231  utopsnneiplem  24237  xblss2ps  24391  xblss2  24392  stdbdxmet  24505  metcnpi3  24536  metustexhalf  24546  nmoi  24718  nmoi2  24720  nmoco  24727  blcvx  24788  icccmplem2  24814  icccmplem3  24815  reconnlem2  24818  xrge0gsumle  24824  metds0  24841  metdstri  24842  metdseq0  24845  lebnumlem3  24955  nmoleub2lem  25106  bcthlem5  25320  csschl  25368  minveclem2  25418  minveclem3b  25420  minveclem4  25424  minveclem6  25426  icombl  25556  cncombf  25650  mbflimsup  25658  itg2monolem1  25742  itg2cnlem1  25753  itg2cnlem2  25754  bddmulibl  25831  ellimc2  25869  cpnord  25927  cpnres  25929  dvmulbr  25931  dvcobr  25938  dvlipcn  25986  dvlip2  25987  dvivthlem1  26000  lhop1lem  26005  lhop1  26006  dvfsumlem2  26019  itgsubstlem  26040  deg1add  26093  deg1sublt  26100  ply1remlem  26155  plyeq0lem  26200  taylthlem2  26364  ulmdvlem3  26392  abelthlem7  26428  pilem2  26442  pilem3  26443  pige3ALT  26509  logccv  26652  cxpaddlelem  26740  cvxcl  26973  fsumharmonic  27000  ftalem5  27065  mpodvdsmulf1o  27182  dvdsmulf1o  27184  bposlem1  27272  lgsqr  27339  lgsquad2lem2  27373  2lgsoddprmlem1  27396  2sqlem8a  27413  2sqlem8  27414  dchrmusum2  27482  dchrvmasumiflem1  27489  dchrisum0flblem1  27496  dchrisum0lem1b  27503  pntlem3  27597  noetasuplem4  27725  noetainflem4  27729  noetalem1  27730  divmulswd  28211  divsclwd  28213  uzsind  28422  tgdim01  28600  axsegcon  29021  ax5seglem1  29022  ax5seglem2  29023  axlowdimlem6  29041  axeuclidlem  29056  axcontlem7  29064  axcontlem9  29066  axcontlem10  29067  nbupgr  29438  nbumgrvtx  29440  cusgrsize2inds  29547  upgriswlk  29734  2pthnloop  29824  numclwwlk2lem1  30471  frgrreg  30489  nmoub3i  30869  ubthlem3  30968  minvecolem2  30971  minvecolem4  30976  minvecolem5  30977  minvecolem6  30978  htthlem  31013  pjpjpre  31515  chscllem1  31733  chscllem2  31734  chscllem3  31735  cnlnadjlem2  32164  leopnmid  32234  tpssad  32634  br8d  32707  swrdf1  33042  splfv3  33044  symgcom2  33172  cyc3genpmlem  33239  archirngz  33277  elrgspnlem1  33330  rlocf1  33361  subrdom  33373  ricdomn1  33377  dvdsruasso  33475  unitpidl1  33514  elrspunidl  33518  qsidomlem1  33542  ssdifidlprm  33548  mxidlirredi  33561  1arithidomlem2  33626  1arithidom  33627  1arithufdlem3  33636  ply1gsumz  33689  mplidomlem  33718  esplymhp  33759  esplyfvaln  33765  vietadeg1  33769  lssdimle  33799  dimkerim  33818  fedgmullem2  33821  fedgmul  33822  assalactf1o  33826  fldextrspundglemul  33870  fldextrspundgdvds  33872  minplyirred  33902  irredminply  33907  algextdeglem2  33909  rtelextdg2lem  33917  constrext2chnlem  33941  constrresqrtcl  33968  2sqr3minply  33971  cos9thpiminplylem2  33974  cos9thpiminply  33979  qqhval2lem  34172  qqhnm  34181  qqhucn  34183  esumcst  34254  esumpcvgval  34269  measunl  34407  dya2iocbrsiga  34466  dya2icobrsiga  34467  omssubadd  34491  inelcarsg  34502  carsgclctunlem2  34510  sibfof  34531  sitgaddlemb  34539  oddpwdc  34545  eulerpartlemgc  34553  bayesth  34630  ftc2re  34789  breprexplemc  34823  tgoldbachgt  34854  erdszelem8  35433  2goelgoanfmla1  35659  br8  35991  matunitlindflem2  37991  totbndbnd  38163  prdsbnd  38167  rrncmslem  38206  rrntotbnd  38210  isdrngo2  38332  lsatcmp  39502  lcvexchlem2  39534  lcvexchlem3  39535  ncvr1  39771  cvrletrN  39772  cvrnbtwn3  39775  cvrnrefN  39781  cvrcmp  39782  0ltat  39790  atnle0  39808  atlen0  39809  cvlcvr1  39838  cvrval3  39912  atle  39935  athgt  39955  1cvratex  39972  ps-2  39977  ps-2b  39981  llnnleat  40012  2atneat  40014  llnle  40017  atcvrlln  40019  llncmp  40021  2llnmat  40023  2at0mat0  40024  2atm  40026  ps-2c  40027  lplnle  40039  lplnnle2at  40040  llncvrlpln2  40056  llncvrlpln  40057  2lplnmN  40058  2llnmj  40059  2atmat  40060  lplncmp  40061  lplnexllnN  40063  2llnm2N  40067  2llnm4  40069  lvolnle3at  40081  4atlem3a  40096  4atlem3b  40097  4atlem10  40105  4atlem11  40108  4atlem12  40111  lplncvrlvol2  40114  lplncvrlvol  40115  lvolcmp  40116  2lplnm2N  40120  2lplnmj  40121  dalempjsen  40152  dalemcea  40159  dalem2  40160  dalemdea  40161  dalem9  40171  dalem16  40178  dalemcjden  40191  dalem21  40193  dalem23  40195  dalem39  40210  dalem54  40225  dalem60  40231  cdlemb  40293  elpadd2at  40305  paddasslem4  40322  paddasslem7  40325  paddasslem15  40333  paddasslem16  40334  pmodlem1  40345  pmodlem2  40346  llnexchb2  40368  pclfinclN  40449  osumcllem9N  40463  pmapojoinN  40467  pexmidN  40468  pl42lem1N  40478  lhp0lt  40502  lhpexle1  40507  lhpexle2lem  40508  lhpexle3lem  40510  lhprelat3N  40539  ltrnid  40634  trlval3  40686  arglem1N  40689  cdlemc5  40694  cdleme3b  40728  cdleme3c  40729  cdleme3h  40734  cdleme7e  40746  cdleme7ga  40747  cdleme20l1  40819  cdleme20l2  40820  cdleme20l  40821  cdleme22b  40840  cdlemefrs29clN  40898  cdlemefrs32fva  40899  cdlemeg46fvcl  41005  cdlemeg46c  41012  cdlemeg46fvaw  41015  cdlemeg46req  41028  cdleme48fgv  41037  cdlemf1  41060  cdlemg1cex  41087  cdlemg2dN  41089  cdlemg2ce  41091  cdlemg12e  41146  cdlemg35  41212  cdlemh  41316  tendocan  41323  cdlemk28-3  41407  tendoex  41474  dih1  41785  dihmeetlem9N  41814  dihlspsnssN  41831  dihlspsnat  41832  lcfrlem23  42064  renegneg  42896  fsuppind  43047  flt4lem4  43106  3cubes  43146  mzpsubst  43204  rencldnfi  43273  irrapx1  43280  pellexlem3  43283  pellexlem5  43285  infmrgelbi  43330  pellqrex  43331  pellfundge  43334  rmspecfund  43361  congtr  43417  acongeq  43435  jm2.20nn  43449  jm2.25lem1  43450  jm2.26  43454  expdiophlem1  43473  hbtlem2  43576  cantnftermord  43772  suprleubrd  44617  suprlubrd  44619  suprnmpt  45628  wessf1ornlem  45639  mpct  45654  upbdrech  45760  ssfiunibd  45764  uzfissfz  45778  xleadd2d  45779  suprltrp  45780  xleadd1d  45781  suprleubrnmpt  45872  iccintsng  45975  limcrecl  46081  fnlimfvre  46124  dvmulcncf  46375  dvdivcncf  46377  dvbdfbdioolem1  46378  ioodvbdlimc1lem2  46382  ioodvbdlimc2lem  46384  stoweidlem1  46451  stoweidlem20  46470  stoweidlem24  46474  stoweidlem34  46484  stoweidlem45  46495  stoweidlem60  46510  fourierdlem20  46577  fourierdlem31  46588  fourierdlem38  46595  fourierdlem64  46620  fourierdlem79  46635  fourierdlem94  46650  fourierdlem113  46669  fouriersw  46681  fouriercn  46682  sge0isum  46877  hoicvr  46998  ovnsubaddlem2  47021  hoidmv1lelem1  47041  hoidmv1lelem3  47043  hoidmvlelem1  47045  hoidmvlelem4  47048  smflimlem2  47222  2timesltsq  47848  fmtnof1  48020  lighneallem2  48091  uspgrlim  48490  upgrwlkupwlk  48638  lincresunit3  48979  elbigolo1  49055  eenglngeehlnm  49237