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 1128	. 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  1380  stoic4b  1778  3rspcedvdw  3609  elovmpt3rab1  7652  smo11  8336  omeulem2  8550  oeeui  8569  oaabs2  8616  omabs  8618  omxpenlem  9047  map2xp  9117  mapdom2  9118  fsuppsssupp  9339  cantnflt  9632  cnfcom  9660  mapdjuen  10141  pwsdompw  10163  ackbij1lem5  10183  cofsmo  10229  fin1a2lem4  10363  ltmul12a  12045  lt2msq1  12074  ledivp1  12092  lemul1ad  12129  lemul2ad  12130  suprubd  12152  supaddc  12157  supadd  12158  supmul1  12159  supmul  12162  rpnnen1lem3  12945  rpnnen1lem5  12947  lediv2ad  13024  xaddge0  13225  xadddi  13262  xadddi2  13264  supicc  13469  supicclub  13471  difelfznle  13610  flval3  13784  expcan  14141  ltexp2  14142  ltexp2r  14145  expubnd  14150  ltexp2rd  14220  ltexp2d  14223  leexp2d  14224  expcand  14225  hashmap  14407  swrds1  14638  ccatswrd  14640  pfxfv  14654  swrdccatin1  14697  pfxccatin12lem3  14704  cshwidxmod  14775  wrdl3s3  14935  o1fsum  15786  mertenslem1  15857  eftlub  16084  rpnnen2lem4  16192  ruclem12  16216  dvdsadd  16279  3dvds  16308  divalgmod  16383  bitsmod  16413  bitsinv1lem  16418  bezoutlem4  16519  gcdzeq  16529  rplpwr  16535  sqgcd  16539  expgcd  16540  rpmulgcd2  16633  rpdvds  16637  coprmproddvdslem  16639  isprm5  16684  divgcdodd  16687  dvdszzq  16698  divnumden  16725  crth  16755  phimullem  16756  modprm0  16783  modprmn0modprm0  16785  coprimeprodsq2  16787  pythagtriplem19  16811  pockthlem  16883  prmunb  16892  prmreclem3  16896  prmreclem6  16899  ramub  16991  ramz  17003  kerf1ghm  19186  pmtrprfv  19390  pmtrprfv3  19391  mndodcong  19479  odngen  19514  pgpfi  19542  sylow2blem3  19559  lsmless1  19597  lsmless2  19598  lsmless12  19599  lsmmod2  19613  pj1id  19636  odadd2  19786  gexexlem  19789  ablfacrplem  20004  ablfacrp  20005  ablfac1b  20009  ablfac1eu  20012  pgpfac1lem2  20014  elrhmunit  20426  rrgnz  20620  lsmssspx  21002  lspsncv0  21063  znunit  21480  uvcvvcl2  21704  uvcvv1  21705  uvcvv0  21706  coe1subfv  22159  coe1fzgsumdlem  22197  scmate  22404  mdetunilem2  22507  pmatcoe1fsupp  22595  mat2pmatlin  22629  decpmatmullem  22665  pmatcollpw1lem1  22668  pmatcollpw1lem2  22669  pm2mpghm  22710  chpscmat  22736  chp0mat  22740  chpidmat  22741  cpmadugsumlemB  22768  cpmadugsumlemC  22769  cpmadugsumlemF  22770  clsndisj  22969  neiptopnei  23026  rnelfm  23847  fmfnfmlem2  23849  fmfnfm  23852  flimss1  23867  isfcf  23928  cnextfun  23958  cnextfvval  23959  cnextf  23960  cnextcn  23961  cnextfres1  23962  ustuqtop1  24136  utopsnneiplem  24142  xblss2ps  24296  xblss2  24297  stdbdxmet  24410  metcnpi3  24441  metustexhalf  24451  nmoi  24623  nmoi2  24625  nmoco  24632  blcvx  24693  icccmplem2  24719  icccmplem3  24720  reconnlem2  24723  xrge0gsumle  24729  metds0  24746  metdstri  24747  metdseq0  24750  lebnumlem3  24869  nmoleub2lem  25021  bcthlem5  25235  csschl  25283  minveclem2  25333  minveclem3b  25335  minveclem4  25339  minveclem6  25341  icombl  25472  cncombf  25566  mbflimsup  25574  itg2monolem1  25658  itg2cnlem1  25669  itg2cnlem2  25670  bddmulibl  25747  ellimc2  25785  cpnord  25844  cpnres  25846  dvmulbr  25848  dvmulbrOLD  25849  dvcobr  25856  dvcobrOLD  25857  dvlipcn  25906  dvlip2  25907  dvivthlem1  25920  lhop1lem  25925  lhop1  25926  dvfsumlem2  25940  dvfsumlem2OLD  25941  itgsubstlem  25962  deg1add  26015  deg1sublt  26022  ply1remlem  26077  plyeq0lem  26122  taylthlem2  26289  taylthlem2OLD  26290  ulmdvlem3  26318  abelthlem7  26355  pilem2  26369  pilem3  26370  pige3ALT  26436  logccv  26579  cxpaddlelem  26668  cvxcl  26902  fsumharmonic  26929  ftalem5  26994  mpodvdsmulf1o  27111  dvdsmulf1o  27113  bposlem1  27202  lgsqr  27269  lgsquad2lem2  27303  2lgsoddprmlem1  27326  2sqlem8a  27343  2sqlem8  27344  dchrmusum2  27412  dchrvmasumiflem1  27419  dchrisum0flblem1  27426  dchrisum0lem1b  27433  pntlem3  27527  noetasuplem4  27655  noetainflem4  27659  noetalem1  27660  divsmulwd  28104  divsclwd  28106  uzsind  28300  tgdim01  28441  axsegcon  28861  ax5seglem1  28862  ax5seglem2  28863  axlowdimlem6  28881  axeuclidlem  28896  axcontlem7  28904  axcontlem9  28906  axcontlem10  28907  nbupgr  29278  nbumgrvtx  29280  cusgrsize2inds  29388  upgriswlk  29576  2pthnloop  29668  numclwwlk2lem1  30312  frgrreg  30330  nmoub3i  30709  ubthlem3  30808  minvecolem2  30811  minvecolem4  30816  minvecolem5  30817  minvecolem6  30818  htthlem  30853  pjpjpre  31355  chscllem1  31573  chscllem2  31574  chscllem3  31575  cnlnadjlem2  32004  leopnmid  32074  tpssad  32475  br8d  32545  swrdf1  32885  splfv3  32887  ogrpaddlt  33038  symgcom2  33048  cyc3genpmlem  33115  archirngz  33150  elrgspnlem1  33200  rlocf1  33231  subrdom  33242  ornglmullt  33292  orngrmullt  33293  dvdsruasso  33363  unitpidl1  33402  elrspunidl  33406  qsidomlem1  33430  ssdifidlprm  33436  mxidlirredi  33449  1arithidomlem2  33514  1arithidom  33515  1arithufdlem3  33524  ply1gsumz  33571  lssdimle  33610  dimkerim  33630  fedgmullem2  33633  fedgmul  33634  assalactf1o  33638  fldextrspundglemul  33681  fldextrspundgdvds  33683  minplyirred  33708  irredminply  33713  algextdeglem2  33715  rtelextdg2lem  33723  constrext2chnlem  33747  constrresqrtcl  33774  2sqr3minply  33777  cos9thpiminplylem2  33780  cos9thpiminply  33785  qqhval2lem  33978  qqhnm  33987  qqhucn  33989  esumcst  34060  esumpcvgval  34075  measunl  34213  dya2iocbrsiga  34273  dya2icobrsiga  34274  omssubadd  34298  inelcarsg  34309  carsgclctunlem2  34317  sibfof  34338  sitgaddlemb  34346  oddpwdc  34352  eulerpartlemgc  34360  bayesth  34437  ftc2re  34596  breprexplemc  34630  tgoldbachgt  34661  erdszelem8  35192  2goelgoanfmla1  35418  br8  35750  matunitlindflem2  37618  totbndbnd  37790  prdsbnd  37794  rrncmslem  37833  rrntotbnd  37837  isdrngo2  37959  lsatcmp  39003  lcvexchlem2  39035  lcvexchlem3  39036  ncvr1  39272  cvrletrN  39273  cvrnbtwn3  39276  cvrnrefN  39282  cvrcmp  39283  0ltat  39291  atnle0  39309  atlen0  39310  cvlcvr1  39339  cvrval3  39414  atle  39437  athgt  39457  1cvratex  39474  ps-2  39479  ps-2b  39483  llnnleat  39514  2atneat  39516  llnle  39519  atcvrlln  39521  llncmp  39523  2llnmat  39525  2at0mat0  39526  2atm  39528  ps-2c  39529  lplnle  39541  lplnnle2at  39542  llncvrlpln2  39558  llncvrlpln  39559  2lplnmN  39560  2llnmj  39561  2atmat  39562  lplncmp  39563  lplnexllnN  39565  2llnm2N  39569  2llnm4  39571  lvolnle3at  39583  4atlem3a  39598  4atlem3b  39599  4atlem10  39607  4atlem11  39610  4atlem12  39613  lplncvrlvol2  39616  lplncvrlvol  39617  lvolcmp  39618  2lplnm2N  39622  2lplnmj  39623  dalempjsen  39654  dalemcea  39661  dalem2  39662  dalemdea  39663  dalem9  39673  dalem16  39680  dalemcjden  39693  dalem21  39695  dalem23  39697  dalem39  39712  dalem54  39727  dalem60  39733  cdlemb  39795  elpadd2at  39807  paddasslem4  39824  paddasslem7  39827  paddasslem15  39835  paddasslem16  39836  pmodlem1  39847  pmodlem2  39848  llnexchb2  39870  pclfinclN  39951  osumcllem9N  39965  pmapojoinN  39969  pexmidN  39970  pl42lem1N  39980  lhp0lt  40004  lhpexle1  40009  lhpexle2lem  40010  lhpexle3lem  40012  lhprelat3N  40041  ltrnid  40136  trlval3  40188  arglem1N  40191  cdlemc5  40196  cdleme3b  40230  cdleme3c  40231  cdleme3h  40236  cdleme7e  40248  cdleme7ga  40249  cdleme20l1  40321  cdleme20l2  40322  cdleme20l  40323  cdleme22b  40342  cdlemefrs29clN  40400  cdlemefrs32fva  40401  cdlemeg46fvcl  40507  cdlemeg46c  40514  cdlemeg46fvaw  40517  cdlemeg46req  40530  cdleme48fgv  40539  cdlemf1  40562  cdlemg1cex  40589  cdlemg2dN  40591  cdlemg2ce  40593  cdlemg12e  40648  cdlemg35  40714  cdlemh  40818  tendocan  40825  cdlemk28-3  40909  tendoex  40976  dih1  41287  dihmeetlem9N  41316  dihlspsnssN  41333  dihlspsnat  41334  lcfrlem23  41566  renegneg  42407  fsuppind  42585  flt4lem4  42644  3cubes  42685  mzpsubst  42743  rencldnfi  42816  irrapx1  42823  pellexlem3  42826  pellexlem5  42828  infmrgelbi  42873  pellqrex  42874  pellfundge  42877  rmspecfund  42904  congtr  42961  acongeq  42979  jm2.20nn  42993  jm2.25lem1  42994  jm2.26  42998  expdiophlem1  43017  hbtlem2  43120  cantnftermord  43316  suprleubrd  44162  suprlubrd  44164  suprnmpt  45175  wessf1ornlem  45186  mpct  45202  upbdrech  45310  ssfiunibd  45314  uzfissfz  45329  xleadd2d  45330  suprltrp  45331  xleadd1d  45332  suprleubrnmpt  45425  iccintsng  45528  limcrecl  45634  fnlimfvre  45679  dvmulcncf  45930  dvdivcncf  45932  dvbdfbdioolem1  45933  ioodvbdlimc1lem2  45937  ioodvbdlimc2lem  45939  stoweidlem1  46006  stoweidlem20  46025  stoweidlem24  46029  stoweidlem34  46039  stoweidlem45  46050  stoweidlem60  46065  fourierdlem20  46132  fourierdlem31  46143  fourierdlem38  46150  fourierdlem64  46175  fourierdlem79  46190  fourierdlem94  46205  fourierdlem113  46224  fouriersw  46236  fouriercn  46237  sge0isum  46432  hoicvr  46553  ovnsubaddlem2  46576  hoidmv1lelem1  46596  hoidmv1lelem3  46598  hoidmvlelem1  46600  hoidmvlelem4  46603  smflimlem2  46777  fmtnof1  47540  lighneallem2  47611  uspgrlim  47995  upgrwlkupwlk  48132  lincresunit3  48474  elbigolo1  48550  eenglngeehlnm  48732