Theorem syl31anc 1375

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

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

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 1089

This theorem is referenced by:  syl32anc  1380  stoic4b  1778  3rspcedvdw  3640  elovmpt3rab1  7693  smo11  8404  omeulem2  8621  oeeui  8640  oaabs2  8687  omabs  8689  omxpenlem  9113  map2xp  9187  mapdom2  9188  fsuppsssupp  9421  cantnflt  9712  cnfcom  9740  mapdjuen  10221  pwsdompw  10243  ackbij1lem5  10263  cofsmo  10309  fin1a2lem4  10443  ltmul12a  12123  lt2msq1  12152  ledivp1  12170  lemul1ad  12207  lemul2ad  12208  suprubd  12230  supaddc  12235  supadd  12236  supmul1  12237  supmul  12240  rpnnen1lem3  13021  rpnnen1lem5  13023  lediv2ad  13099  xaddge0  13300  xadddi  13337  xadddi2  13339  supicc  13541  supicclub  13543  difelfznle  13682  flval3  13855  expcan  14209  ltexp2  14210  ltexp2r  14213  expubnd  14217  ltexp2rd  14287  ltexp2d  14290  leexp2d  14291  expcand  14292  hashmap  14474  swrds1  14704  ccatswrd  14706  pfxfv  14720  swrdccatin1  14763  pfxccatin12lem3  14770  cshwidxmod  14841  wrdl3s3  15001  o1fsum  15849  mertenslem1  15920  eftlub  16145  rpnnen2lem4  16253  ruclem12  16277  dvdsadd  16339  3dvds  16368  divalgmod  16443  bitsmod  16473  bitsinv1lem  16478  bezoutlem4  16579  gcdzeq  16589  rplpwr  16595  sqgcd  16599  expgcd  16600  rpmulgcd2  16693  rpdvds  16697  coprmproddvdslem  16699  isprm5  16744  divgcdodd  16747  dvdszzq  16758  divnumden  16785  crth  16815  phimullem  16816  modprm0  16843  modprmn0modprm0  16845  coprimeprodsq2  16847  pythagtriplem19  16871  pockthlem  16943  prmunb  16952  prmreclem3  16956  prmreclem6  16959  ramub  17051  ramz  17063  kerf1ghm  19265  pmtrprfv  19471  pmtrprfv3  19472  mndodcong  19560  odngen  19595  pgpfi  19623  sylow2blem3  19640  lsmless1  19678  lsmless2  19679  lsmless12  19680  lsmmod2  19694  pj1id  19717  odadd2  19867  gexexlem  19870  ablfacrplem  20085  ablfacrp  20086  ablfac1b  20090  ablfac1eu  20093  pgpfac1lem2  20095  elrhmunit  20510  rrgnz  20704  lsmssspx  21087  lspsncv0  21148  znunit  21582  uvcvvcl2  21808  uvcvv1  21809  uvcvv0  21810  coe1subfv  22269  coe1fzgsumdlem  22307  scmate  22516  mdetunilem2  22619  pmatcoe1fsupp  22707  mat2pmatlin  22741  decpmatmullem  22777  pmatcollpw1lem1  22780  pmatcollpw1lem2  22781  pm2mpghm  22822  chpscmat  22848  chp0mat  22852  chpidmat  22853  cpmadugsumlemB  22880  cpmadugsumlemC  22881  cpmadugsumlemF  22882  clsndisj  23083  neiptopnei  23140  rnelfm  23961  fmfnfmlem2  23963  fmfnfm  23966  flimss1  23981  isfcf  24042  cnextfun  24072  cnextfvval  24073  cnextf  24074  cnextcn  24075  cnextfres1  24076  ustuqtop1  24250  utopsnneiplem  24256  xblss2ps  24411  xblss2  24412  stdbdxmet  24528  metcnpi3  24559  metustexhalf  24569  nmoi  24749  nmoi2  24751  nmoco  24758  blcvx  24819  icccmplem2  24845  icccmplem3  24846  reconnlem2  24849  xrge0gsumle  24855  metds0  24872  metdstri  24873  metdseq0  24876  lebnumlem3  24995  nmoleub2lem  25147  bcthlem5  25362  csschl  25410  minveclem2  25460  minveclem3b  25462  minveclem4  25466  minveclem6  25468  icombl  25599  cncombf  25693  mbflimsup  25701  itg2monolem1  25785  itg2cnlem1  25796  itg2cnlem2  25797  bddmulibl  25874  ellimc2  25912  cpnord  25971  cpnres  25973  dvmulbr  25975  dvmulbrOLD  25976  dvcobr  25983  dvcobrOLD  25984  dvlipcn  26033  dvlip2  26034  dvivthlem1  26047  lhop1lem  26052  lhop1  26053  dvfsumlem2  26067  dvfsumlem2OLD  26068  itgsubstlem  26089  deg1add  26142  deg1sublt  26149  ply1remlem  26204  plyeq0lem  26249  taylthlem2  26416  taylthlem2OLD  26417  ulmdvlem3  26445  abelthlem7  26482  pilem2  26496  pilem3  26497  pige3ALT  26562  logccv  26705  cxpaddlelem  26794  cvxcl  27028  fsumharmonic  27055  ftalem5  27120  mpodvdsmulf1o  27237  dvdsmulf1o  27239  bposlem1  27328  lgsqr  27395  lgsquad2lem2  27429  2lgsoddprmlem1  27452  2sqlem8a  27469  2sqlem8  27470  dchrmusum2  27538  dchrvmasumiflem1  27545  dchrisum0flblem1  27552  dchrisum0lem1b  27559  pntlem3  27653  noetasuplem4  27781  noetainflem4  27785  noetalem1  27786  divsmulwd  28219  divsclwd  28221  uzsind  28391  tgdim01  28515  axsegcon  28942  ax5seglem1  28943  ax5seglem2  28944  axlowdimlem6  28962  axeuclidlem  28977  axcontlem7  28985  axcontlem9  28987  axcontlem10  28988  nbupgr  29361  nbumgrvtx  29363  cusgrsize2inds  29471  upgriswlk  29659  2pthnloop  29751  numclwwlk2lem1  30395  frgrreg  30413  nmoub3i  30792  ubthlem3  30891  minvecolem2  30894  minvecolem4  30899  minvecolem5  30900  minvecolem6  30901  htthlem  30936  pjpjpre  31438  chscllem1  31656  chscllem2  31657  chscllem3  31658  cnlnadjlem2  32087  leopnmid  32157  br8d  32622  swrdf1  32941  splfv3  32943  ogrpaddlt  33094  symgcom2  33104  cyc3genpmlem  33171  archirngz  33196  elrgspnlem1  33246  rlocf1  33277  subrdom  33288  ornglmullt  33337  orngrmullt  33338  dvdsruasso  33413  unitpidl1  33452  elrspunidl  33456  qsidomlem1  33480  ssdifidlprm  33486  mxidlirredi  33499  1arithidomlem2  33564  1arithidom  33565  1arithufdlem3  33574  ply1gsumz  33619  lssdimle  33658  dimkerim  33678  fedgmullem2  33681  fedgmul  33682  assalactf1o  33686  fldextrspundglemul  33729  fldextrspundgdvds  33731  minplyirred  33754  irredminply  33757  algextdeglem2  33759  rtelextdg2lem  33767  2sqr3minply  33791  qqhval2lem  33982  qqhnm  33991  qqhucn  33993  esumcst  34064  esumpcvgval  34079  measunl  34217  dya2iocbrsiga  34277  dya2icobrsiga  34278  omssubadd  34302  inelcarsg  34313  carsgclctunlem2  34321  sibfof  34342  sitgaddlemb  34350  oddpwdc  34356  eulerpartlemgc  34364  bayesth  34441  ftc2re  34613  breprexplemc  34647  tgoldbachgt  34678  erdszelem8  35203  2goelgoanfmla1  35429  br8  35756  matunitlindflem2  37624  totbndbnd  37796  prdsbnd  37800  rrncmslem  37839  rrntotbnd  37843  isdrngo2  37965  lsatcmp  39004  lcvexchlem2  39036  lcvexchlem3  39037  ncvr1  39273  cvrletrN  39274  cvrnbtwn3  39277  cvrnrefN  39283  cvrcmp  39284  0ltat  39292  atnle0  39310  atlen0  39311  cvlcvr1  39340  cvrval3  39415  atle  39438  athgt  39458  1cvratex  39475  ps-2  39480  ps-2b  39484  llnnleat  39515  2atneat  39517  llnle  39520  atcvrlln  39522  llncmp  39524  2llnmat  39526  2at0mat0  39527  2atm  39529  ps-2c  39530  lplnle  39542  lplnnle2at  39543  llncvrlpln2  39559  llncvrlpln  39560  2lplnmN  39561  2llnmj  39562  2atmat  39563  lplncmp  39564  lplnexllnN  39566  2llnm2N  39570  2llnm4  39572  lvolnle3at  39584  4atlem3a  39599  4atlem3b  39600  4atlem10  39608  4atlem11  39611  4atlem12  39614  lplncvrlvol2  39617  lplncvrlvol  39618  lvolcmp  39619  2lplnm2N  39623  2lplnmj  39624  dalempjsen  39655  dalemcea  39662  dalem2  39663  dalemdea  39664  dalem9  39674  dalem16  39681  dalemcjden  39694  dalem21  39696  dalem23  39698  dalem39  39713  dalem54  39728  dalem60  39734  cdlemb  39796  elpadd2at  39808  paddasslem4  39825  paddasslem7  39828  paddasslem15  39836  paddasslem16  39837  pmodlem1  39848  pmodlem2  39849  llnexchb2  39871  pclfinclN  39952  osumcllem9N  39966  pmapojoinN  39970  pexmidN  39971  pl42lem1N  39981  lhp0lt  40005  lhpexle1  40010  lhpexle2lem  40011  lhpexle3lem  40013  lhprelat3N  40042  ltrnid  40137  trlval3  40189  arglem1N  40192  cdlemc5  40197  cdleme3b  40231  cdleme3c  40232  cdleme3h  40237  cdleme7e  40249  cdleme7ga  40250  cdleme20l1  40322  cdleme20l2  40323  cdleme20l  40324  cdleme22b  40343  cdlemefrs29clN  40401  cdlemefrs32fva  40402  cdlemeg46fvcl  40508  cdlemeg46c  40515  cdlemeg46fvaw  40518  cdlemeg46req  40531  cdleme48fgv  40540  cdlemf1  40563  cdlemg1cex  40590  cdlemg2dN  40592  cdlemg2ce  40594  cdlemg12e  40649  cdlemg35  40715  cdlemh  40819  tendocan  40826  cdlemk28-3  40910  tendoex  40977  dih1  41288  dihmeetlem9N  41317  dihlspsnssN  41334  dihlspsnat  41335  lcfrlem23  41567  renegneg  42441  fsuppind  42600  flt4lem4  42659  3cubes  42701  mzpsubst  42759  rencldnfi  42832  irrapx1  42839  pellexlem3  42842  pellexlem5  42844  infmrgelbi  42889  pellqrex  42890  pellfundge  42893  rmspecfund  42920  congtr  42977  acongeq  42995  jm2.20nn  43009  jm2.25lem1  43010  jm2.26  43014  expdiophlem1  43033  hbtlem2  43136  cantnftermord  43333  suprleubrd  44179  suprlubrd  44181  suprnmpt  45179  wessf1ornlem  45190  mpct  45206  upbdrech  45317  ssfiunibd  45321  uzfissfz  45337  xleadd2d  45338  suprltrp  45339  xleadd1d  45340  suprleubrnmpt  45433  iccintsng  45536  limcrecl  45644  fnlimfvre  45689  dvmulcncf  45940  dvdivcncf  45942  dvbdfbdioolem1  45943  ioodvbdlimc1lem2  45947  ioodvbdlimc2lem  45949  stoweidlem1  46016  stoweidlem20  46035  stoweidlem24  46039  stoweidlem34  46049  stoweidlem45  46060  stoweidlem60  46075  fourierdlem20  46142  fourierdlem31  46153  fourierdlem38  46160  fourierdlem64  46185  fourierdlem79  46200  fourierdlem94  46215  fourierdlem113  46234  fouriersw  46246  fouriercn  46247  sge0isum  46442  hoicvr  46563  ovnsubaddlem2  46586  hoidmv1lelem1  46606  hoidmv1lelem3  46608  hoidmvlelem1  46610  hoidmvlelem4  46613  smflimlem2  46787  fmtnof1  47522  lighneallem2  47593  uspgrlim  47959  upgrwlkupwlk  48056  lincresunit3  48398  elbigolo1  48478  eenglngeehlnm  48660