Theorem syl121anc 1371

Description: Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.)

Hypotheses

Ref	Expression
syl3anc.1	⊢ (𝜑 → 𝜓)
syl3anc.2	⊢ (𝜑 → 𝜒)
syl3anc.3	⊢ (𝜑 → 𝜃)
syl3Xanc.4	⊢ (𝜑 → 𝜏)
syl121anc.5	⊢ ((𝜓 ∧ (𝜒 ∧ 𝜃) ∧ 𝜏) → 𝜂)

Assertion

Ref	Expression
syl121anc	⊢ (𝜑 → 𝜂)

Proof of Theorem syl121anc

Step	Hyp	Ref	Expression
1		syl3anc.1	. 2 ⊢ (𝜑 → 𝜓)
2		syl3anc.2	. . 3 ⊢ (𝜑 → 𝜒)
3		syl3anc.3	. . 3 ⊢ (𝜑 → 𝜃)
4	2, 3	jca 514	. 2 ⊢ (𝜑 → (𝜒 ∧ 𝜃))
5		syl3Xanc.4	. 2 ⊢ (𝜑 → 𝜏)
6		syl121anc.5	. 2 ⊢ ((𝜓 ∧ (𝜒 ∧ 𝜃) ∧ 𝜏) → 𝜂)
7	1, 4, 5, 6	syl3anc 1367	1 ⊢ (𝜑 → 𝜂)

Syntax hints:   → wi 4   ∧ wa 398   ∧ w3a 1083

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 209  df-an 399  df-3an 1085

This theorem is referenced by:  syl122anc  1375  fsnunf2  6948  tfisi  7573  fnsuppeq0  7858  axdc4lem  9877  div32d  11439  div13d  11440  expdivd  13525  swrdsbslen  14026  sumeven  15738  sumodd  15739  pcqmul  16190  pcid  16209  pcneg  16210  pc2dvds  16215  pcz  16217  pcaddlem  16224  pcadd  16225  pcmpt2  16229  pcbc  16236  qexpz  16237  expnprm  16238  sylow1lem1  18723  lspsneleq  19887  lspsneq  19894  lspfixed  19900  frlmsslss2  20919  chmatval  21437  chpmat1dlem  21443  chpdmatlem2  21447  ucncn  22894  ucnextcn  22913  ssblex  23038  prdsxmslem2  23139  ncvs1  23761  voliunlem1  24151  deg1mul3le  24710  deg1pw  24714  fta1blem  24762  bcmono  25853  dchrisum0flblem1  26084  dchrisum0flblem2  26085  pntibndlem1  26165  pntlemr  26178  finsumvtxdg2sstep  27331  umgr3cyclex  27962  nv1  28452  resf1o  30466  omndmul3  30714  symgcntz  30729  cycpmco2lem6  30773  tocyccntz  30786  rngurd  30857  measun  31470  measvuni  31473  measunl  31475  nosupbnd1  33214  slerec  33277  btwnconn1lem14  33561  segcon2  33566  seglelin  33577  neibastop3  33710  upixp  35019  fdc  35035  eqlkr3  36252  lkrshp  36256  lfl1dim  36272  lfl1dim2N  36273  eqlkr4  36316  2llnneN  36560  3dim2  36619  4atlem3  36747  4atlem11  36760  4atlem12  36763  pexmidlem4N  37124  lhp2at0nle  37186  lhple  37193  ltrnideq  37326  cdlemd9  37357  cdleme0ex2N  37375  cdleme0moN  37376  cdleme11a  37411  cdleme30a  37529  cdlemefs32sn1aw  37565  cdleme43fsv1snlem  37571  cdlemefs31fv1  37575  cdlemefs45eN  37582  cdleme41sn3a  37584  cdleme35h  37607  cdleme36a  37611  cdleme40m  37618  cdleme40n  37619  cdleme41sn3aw  37625  cdleme42h  37633  cdleme42k  37635  cdleme42mN  37638  cdleme43cN  37642  cdleme17d3  37647  cdleme48fvg  37651  cdlemeg47rv2  37661  cdlemeg46c  37664  cdlemeg46sfg  37671  cdlemeg46rjgN  37673  cdlemeg46rgv  37679  cdlemeg46req  37680  cdlemeg46gfv  37681  cdlemeg46gfre  37683  cdlemeg49lebilem  37690  cdleme50trn2  37702  cdlemg2kq  37753  cdlemb3  37757  cdlemg4f  37766  cdlemg9a  37783  cdlemg9b  37784  cdlemg9  37785  cdlemg11aq  37789  cdlemg12a  37794  cdlemg12b  37795  cdlemg12c  37796  cdlemg12d  37797  cdlemg12f  37799  cdlemg12g  37800  cdlemg12  37801  cdlemg13a  37802  cdlemg16  37808  cdlemg17e  37816  cdlemg17f  37817  cdlemg17g  37818  cdlemg17ir  37821  cdlemg17  37828  cdlemg18b  37830  cdlemg18c  37831  cdlemg33e  37861  trlcoabs2N  37873  trlcocnvat  37875  trlcolem  37877  trlco  37878  cdlemg44  37884  cdlemg47  37887  ltrncom  37889  tendococl  37923  tendoplcl  37932  tendoplcom  37933  tendoplass  37934  tendodi1  37935  tendodi2  37936  tendo0pl  37942  tendoipl  37948  cdlemh1  37966  cdlemi2  37970  tendo0mul  37977  tendo0mulr  37978  cdlemk2  37983  cdlemk3  37984  cdlemk4  37985  cdlemk6  37988  cdlemk8  37989  cdlemk12  38001  cdlemkole  38004  cdlemk14  38005  cdlemk15  38006  cdlemk5u  38012  cdlemk6u  38013  cdlemk12u  38023  cdlemkfid1N  38072  cdlemk19x  38094  cdlemk48  38101  cdlemk53a  38106  cdlemk56  38122  cdleml2N  38128  cdleml3N  38129  cdleml6  38132  cdleml7  38133  dva1dim  38136  dia2dimlem4  38218  dvhlveclem  38259  doca2N  38277  djajN  38288  cdlemn2a  38347  cdlemn3  38348  dihordlem6  38364  dihord5apre  38413  dihglbcpreN  38451  dihmeetcN  38453  dihmeetbN  38454  dihmeetlem10N  38467  dihmeetlem12N  38469  dihmeetlem15N  38472  dihmeetALTN  38478  dih1dimatlem0  38479  dihjatcclem3  38571  dihjatcclem4  38572  mapdpglem22  38844  hdmap14lem1a  39017  eldioph2b  39409  jm2.19lem4  39638  jm2.19  39639  jm2.26a  39646  jm2.26  39648  hbtlem2  39773  fnchoice  41335  stoweidlem42  42376  stoweidlem59  42393  fourierdlem42  42483