Theorem syl31anc 1372

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

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1086

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 207  df-an 396  df-3an 1088

This theorem is referenced by:  syl32anc  1377  stoic4b  1774  3rspcedvdw  3639  elovmpt3rab1  7692  smo11  8402  omeulem2  8619  oeeui  8638  oaabs2  8685  omabs  8687  omxpenlem  9111  map2xp  9185  mapdom2  9186  fsuppsssupp  9418  cantnflt  9709  cnfcom  9737  mapdjuen  10218  pwsdompw  10240  ackbij1lem5  10260  cofsmo  10306  fin1a2lem4  10440  ltmul12a  12120  lt2msq1  12149  ledivp1  12167  lemul1ad  12204  lemul2ad  12205  suprubd  12227  supaddc  12232  supadd  12233  supmul1  12234  supmul  12237  rpnnen1lem3  13018  rpnnen1lem5  13020  lediv2ad  13096  xaddge0  13296  xadddi  13333  xadddi2  13335  supicc  13537  supicclub  13539  difelfznle  13678  flval3  13851  expcan  14205  ltexp2  14206  ltexp2r  14209  expubnd  14213  ltexp2rd  14283  ltexp2d  14286  leexp2d  14287  expcand  14288  hashmap  14470  swrds1  14700  ccatswrd  14702  pfxfv  14716  swrdccatin1  14759  pfxccatin12lem3  14766  cshwidxmod  14837  wrdl3s3  14997  o1fsum  15845  mertenslem1  15916  eftlub  16141  rpnnen2lem4  16249  ruclem12  16273  dvdsadd  16335  3dvds  16364  divalgmod  16439  bitsmod  16469  bitsinv1lem  16474  bezoutlem4  16575  gcdzeq  16585  rplpwr  16591  sqgcd  16595  expgcd  16596  rpmulgcd2  16689  rpdvds  16693  coprmproddvdslem  16695  isprm5  16740  divgcdodd  16743  dvdszzq  16754  divnumden  16781  crth  16811  phimullem  16812  modprm0  16838  modprmn0modprm0  16840  coprimeprodsq2  16842  pythagtriplem19  16866  pockthlem  16938  prmunb  16947  prmreclem3  16951  prmreclem6  16954  ramub  17046  ramz  17058  kerf1ghm  19277  pmtrprfv  19485  pmtrprfv3  19486  mndodcong  19574  odngen  19609  pgpfi  19637  sylow2blem3  19654  lsmless1  19692  lsmless2  19693  lsmless12  19694  lsmmod2  19708  pj1id  19731  odadd2  19881  gexexlem  19884  ablfacrplem  20099  ablfacrp  20100  ablfac1b  20104  ablfac1eu  20107  pgpfac1lem2  20109  elrhmunit  20526  rrgnz  20720  lsmssspx  21104  lspsncv0  21165  znunit  21599  uvcvvcl2  21825  uvcvv1  21826  uvcvv0  21827  coe1subfv  22284  coe1fzgsumdlem  22322  scmate  22531  mdetunilem2  22634  pmatcoe1fsupp  22722  mat2pmatlin  22756  decpmatmullem  22792  pmatcollpw1lem1  22795  pmatcollpw1lem2  22796  pm2mpghm  22837  chpscmat  22863  chp0mat  22867  chpidmat  22868  cpmadugsumlemB  22895  cpmadugsumlemC  22896  cpmadugsumlemF  22897  clsndisj  23098  neiptopnei  23155  rnelfm  23976  fmfnfmlem2  23978  fmfnfm  23981  flimss1  23996  isfcf  24057  cnextfun  24087  cnextfvval  24088  cnextf  24089  cnextcn  24090  cnextfres1  24091  ustuqtop1  24265  utopsnneiplem  24271  xblss2ps  24426  xblss2  24427  stdbdxmet  24543  metcnpi3  24574  metustexhalf  24584  nmoi  24764  nmoi2  24766  nmoco  24773  blcvx  24833  icccmplem2  24858  icccmplem3  24859  reconnlem2  24862  xrge0gsumle  24868  metds0  24885  metdstri  24886  metdseq0  24889  lebnumlem3  25008  nmoleub2lem  25160  bcthlem5  25375  csschl  25423  minveclem2  25473  minveclem3b  25475  minveclem4  25479  minveclem6  25481  icombl  25612  cncombf  25706  mbflimsup  25714  itg2monolem1  25799  itg2cnlem1  25810  itg2cnlem2  25811  bddmulibl  25888  ellimc2  25926  cpnord  25985  cpnres  25987  dvmulbr  25989  dvmulbrOLD  25990  dvcobr  25997  dvcobrOLD  25998  dvlipcn  26047  dvlip2  26048  dvivthlem1  26061  lhop1lem  26066  lhop1  26067  dvfsumlem2  26081  dvfsumlem2OLD  26082  itgsubstlem  26103  deg1add  26156  deg1sublt  26163  ply1remlem  26218  plyeq0lem  26263  taylthlem2  26430  taylthlem2OLD  26431  ulmdvlem3  26459  abelthlem7  26496  pilem2  26510  pilem3  26511  pige3ALT  26576  logccv  26719  cxpaddlelem  26808  cvxcl  27042  fsumharmonic  27069  ftalem5  27134  mpodvdsmulf1o  27251  dvdsmulf1o  27253  bposlem1  27342  lgsqr  27409  lgsquad2lem2  27443  2lgsoddprmlem1  27466  2sqlem8a  27483  2sqlem8  27484  dchrmusum2  27552  dchrvmasumiflem1  27559  dchrisum0flblem1  27566  dchrisum0lem1b  27573  pntlem3  27667  noetasuplem4  27795  noetainflem4  27799  noetalem1  27800  divsmulwd  28233  divsclwd  28235  uzsind  28405  tgdim01  28529  axsegcon  28956  ax5seglem1  28957  ax5seglem2  28958  axlowdimlem6  28976  axeuclidlem  28991  axcontlem7  28999  axcontlem9  29001  axcontlem10  29002  nbupgr  29375  nbumgrvtx  29377  cusgrsize2inds  29485  upgriswlk  29673  2pthnloop  29763  numclwwlk2lem1  30404  frgrreg  30422  nmoub3i  30801  ubthlem3  30900  minvecolem2  30903  minvecolem4  30908  minvecolem5  30909  minvecolem6  30910  htthlem  30945  pjpjpre  31447  chscllem1  31665  chscllem2  31666  chscllem3  31667  cnlnadjlem2  32096  leopnmid  32166  br8d  32629  swrdf1  32925  splfv3  32927  ogrpaddlt  33076  symgcom2  33086  cyc3genpmlem  33153  archirngz  33178  elrgspnlem1  33231  rlocf1  33259  subrdom  33268  ornglmullt  33316  orngrmullt  33317  dvdsruasso  33392  unitpidl1  33431  elrspunidl  33435  qsidomlem1  33459  ssdifidlprm  33465  mxidlirredi  33478  1arithidomlem2  33543  1arithidom  33544  1arithufdlem3  33553  ply1gsumz  33598  lssdimle  33634  dimkerim  33654  fedgmullem2  33657  fedgmul  33658  assalactf1o  33662  minplyirred  33718  irredminply  33721  algextdeglem2  33723  rtelextdg2lem  33731  2sqr3minply  33752  qqhval2lem  33943  qqhnm  33952  qqhucn  33954  esumcst  34043  esumpcvgval  34058  measunl  34196  dya2iocbrsiga  34256  dya2icobrsiga  34257  omssubadd  34281  inelcarsg  34292  carsgclctunlem2  34300  sibfof  34321  sitgaddlemb  34329  oddpwdc  34335  eulerpartlemgc  34343  bayesth  34420  ftc2re  34591  breprexplemc  34625  tgoldbachgt  34656  erdszelem8  35182  2goelgoanfmla1  35408  br8  35735  matunitlindflem2  37603  totbndbnd  37775  prdsbnd  37779  rrncmslem  37818  rrntotbnd  37822  isdrngo2  37944  lsatcmp  38984  lcvexchlem2  39016  lcvexchlem3  39017  ncvr1  39253  cvrletrN  39254  cvrnbtwn3  39257  cvrnrefN  39263  cvrcmp  39264  0ltat  39272  atnle0  39290  atlen0  39291  cvlcvr1  39320  cvrval3  39395  atle  39418  athgt  39438  1cvratex  39455  ps-2  39460  ps-2b  39464  llnnleat  39495  2atneat  39497  llnle  39500  atcvrlln  39502  llncmp  39504  2llnmat  39506  2at0mat0  39507  2atm  39509  ps-2c  39510  lplnle  39522  lplnnle2at  39523  llncvrlpln2  39539  llncvrlpln  39540  2lplnmN  39541  2llnmj  39542  2atmat  39543  lplncmp  39544  lplnexllnN  39546  2llnm2N  39550  2llnm4  39552  lvolnle3at  39564  4atlem3a  39579  4atlem3b  39580  4atlem10  39588  4atlem11  39591  4atlem12  39594  lplncvrlvol2  39597  lplncvrlvol  39598  lvolcmp  39599  2lplnm2N  39603  2lplnmj  39604  dalempjsen  39635  dalemcea  39642  dalem2  39643  dalemdea  39644  dalem9  39654  dalem16  39661  dalemcjden  39674  dalem21  39676  dalem23  39678  dalem39  39693  dalem54  39708  dalem60  39714  cdlemb  39776  elpadd2at  39788  paddasslem4  39805  paddasslem7  39808  paddasslem15  39816  paddasslem16  39817  pmodlem1  39828  pmodlem2  39829  llnexchb2  39851  pclfinclN  39932  osumcllem9N  39946  pmapojoinN  39950  pexmidN  39951  pl42lem1N  39961  lhp0lt  39985  lhpexle1  39990  lhpexle2lem  39991  lhpexle3lem  39993  lhprelat3N  40022  ltrnid  40117  trlval3  40169  arglem1N  40172  cdlemc5  40177  cdleme3b  40211  cdleme3c  40212  cdleme3h  40217  cdleme7e  40229  cdleme7ga  40230  cdleme20l1  40302  cdleme20l2  40303  cdleme20l  40304  cdleme22b  40323  cdlemefrs29clN  40381  cdlemefrs32fva  40382  cdlemeg46fvcl  40488  cdlemeg46c  40495  cdlemeg46fvaw  40498  cdlemeg46req  40511  cdleme48fgv  40520  cdlemf1  40543  cdlemg1cex  40570  cdlemg2dN  40572  cdlemg2ce  40574  cdlemg12e  40629  cdlemg35  40695  cdlemh  40799  tendocan  40806  cdlemk28-3  40890  tendoex  40957  dih1  41268  dihmeetlem9N  41297  dihlspsnssN  41314  dihlspsnat  41315  lcfrlem23  41547  renegneg  42417  fsuppind  42576  flt4lem4  42635  3cubes  42677  mzpsubst  42735  rencldnfi  42808  irrapx1  42815  pellexlem3  42818  pellexlem5  42820  infmrgelbi  42865  pellqrex  42866  pellfundge  42869  rmspecfund  42896  congtr  42953  acongeq  42971  jm2.20nn  42985  jm2.25lem1  42986  jm2.26  42990  expdiophlem1  43009  hbtlem2  43112  cantnftermord  43309  suprleubrd  44155  suprlubrd  44157  suprnmpt  45116  wessf1ornlem  45127  mpct  45143  upbdrech  45255  ssfiunibd  45259  uzfissfz  45275  xleadd2d  45276  suprltrp  45277  xleadd1d  45278  suprleubrnmpt  45371  iccintsng  45475  limcrecl  45584  fnlimfvre  45629  dvmulcncf  45880  dvdivcncf  45882  dvbdfbdioolem1  45883  ioodvbdlimc1lem2  45887  ioodvbdlimc2lem  45889  stoweidlem1  45956  stoweidlem20  45975  stoweidlem24  45979  stoweidlem34  45989  stoweidlem45  46000  stoweidlem60  46015  fourierdlem20  46082  fourierdlem31  46093  fourierdlem38  46100  fourierdlem64  46125  fourierdlem79  46140  fourierdlem94  46155  fourierdlem113  46174  fouriersw  46186  fouriercn  46187  sge0isum  46382  hoicvr  46503  ovnsubaddlem2  46526  hoidmv1lelem1  46546  hoidmv1lelem3  46548  hoidmvlelem1  46550  hoidmvlelem4  46553  smflimlem2  46727  fmtnof1  47459  lighneallem2  47530  uspgrlim  47894  upgrwlkupwlk  47983  lincresunit3  48326  elbigolo1  48406  eenglngeehlnm  48588