Theorem syl121anc 1384

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 517	. 2 ⊢ (𝜑 → (𝜒 ∧ 𝜃))
5		syl3Xanc.4	. 2 ⊢ (𝜑 → 𝜏)
6		syl121anc.5	. 2 ⊢ ((𝜓 ∧ (𝜒 ∧ 𝜃) ∧ 𝜏) → 𝜂)
7	1, 4, 5, 6	syl3anc 1380	1 ⊢ (𝜑 → 𝜂)

Syntax hints:   → wi 4   ∧ wa 397   ∧ w3a 1093

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 398  df-3an 1095

This theorem is referenced by:  syl122anc  1388  fsnunf2  7133  tfisi  7802  fnsuppeq0  8134  ttrclss  9636  ttrclselem2  9642  axdc4lem  10373  div32d  11949  div13d  11950  expdivd  14117  swrdsbslen  14622  sumeven  16351  sumodd  16352  pcqmul  16819  pcid  16839  pcneg  16840  pc2dvds  16845  pcz  16847  pcaddlem  16854  pcadd  16855  pcmpt2  16859  pcbc  16866  qexpz  16867  expnprm  16868  sylow1lem1  19567  omndmul3  20103  ringurd  20160  lspsneleq  21111  lspsneq  21118  lspfixed  21124  frlmsslss2  21753  chmatval  22815  chpmat1dlem  22821  chpdmatlem2  22825  ucncn  24270  ucnextcn  24289  ssblex  24414  prdsxmslem2  24515  ncvs1  25145  voliunlem1  25538  deg1mul3le  26103  deg1pw  26107  fta1blem  26157  bcmono  27261  dchrisum0flblem1  27492  dchrisum0flblem2  27493  pntibndlem1  27573  pntlemr  27586  nosupbnd1  27698  noinfbnd1  27713  noetalem1  27725  lesrec  27811  finsumvtxdg2sstep  29638  umgr3cyclex  30273  nv1  30766  resf1o  32824  symgcntz  33168  cycpmco2lem6  33214  tocyccntz  33227  deg1vr  33685  rtelextdg2lem  33920  measun  34405  measvuni  34408  measunl  34410  btwnconn1lem14  36341  segcon2  36346  seglelin  36357  neibastop3  36603  upixp  38109  fdc  38125  eqlkr3  39606  lkrshp  39610  lfl1dim  39626  lfl1dim2N  39627  eqlkr4  39670  2llnneN  39914  3dim2  39973  4atlem3  40101  4atlem11  40114  4atlem12  40117  pexmidlem4N  40478  lhp2at0nle  40540  lhple  40547  ltrnideq  40680  cdlemd9  40711  cdleme0ex2N  40729  cdleme0moN  40730  cdleme11a  40765  cdleme30a  40883  cdlemefs32sn1aw  40919  cdleme43fsv1snlem  40925  cdlemefs31fv1  40929  cdlemefs45eN  40936  cdleme41sn3a  40938  cdleme35h  40961  cdleme36a  40965  cdleme40m  40972  cdleme40n  40973  cdleme41sn3aw  40979  cdleme42h  40987  cdleme42k  40989  cdleme42mN  40992  cdleme43cN  40996  cdleme17d3  41001  cdleme48fvg  41005  cdlemeg47rv2  41015  cdlemeg46c  41018  cdlemeg46sfg  41025  cdlemeg46rjgN  41027  cdlemeg46rgv  41033  cdlemeg46req  41034  cdlemeg46gfv  41035  cdlemeg46gfre  41037  cdlemeg49lebilem  41044  cdleme50trn2  41056  cdlemg2kq  41107  cdlemb3  41111  cdlemg4f  41120  cdlemg9a  41137  cdlemg9b  41138  cdlemg9  41139  cdlemg11aq  41143  cdlemg12a  41148  cdlemg12b  41149  cdlemg12c  41150  cdlemg12d  41151  cdlemg12f  41153  cdlemg12g  41154  cdlemg12  41155  cdlemg13a  41156  cdlemg16  41162  cdlemg17e  41170  cdlemg17f  41171  cdlemg17g  41172  cdlemg17ir  41175  cdlemg17  41182  cdlemg18b  41184  cdlemg18c  41185  cdlemg33e  41215  trlcoabs2N  41227  trlcocnvat  41229  trlcolem  41231  trlco  41232  cdlemg44  41238  cdlemg47  41241  ltrncom  41243  tendococl  41277  tendoplcl  41286  tendoplcom  41287  tendoplass  41288  tendodi1  41289  tendodi2  41290  tendo0pl  41296  tendoipl  41302  cdlemh1  41320  cdlemi2  41324  tendo0mul  41331  tendo0mulr  41332  cdlemk2  41337  cdlemk3  41338  cdlemk4  41339  cdlemk6  41342  cdlemk8  41343  cdlemk12  41355  cdlemkole  41358  cdlemk14  41359  cdlemk15  41360  cdlemk5u  41366  cdlemk6u  41367  cdlemk12u  41377  cdlemkfid1N  41426  cdlemk19x  41448  cdlemk48  41455  cdlemk53a  41460  cdlemk56  41476  cdleml2N  41482  cdleml3N  41483  cdleml6  41486  cdleml7  41487  dva1dim  41490  dia2dimlem4  41572  dvhlveclem  41613  doca2N  41631  djajN  41642  cdlemn2a  41701  cdlemn3  41702  dihordlem6  41718  dihord5apre  41767  dihglbcpreN  41805  dihmeetcN  41807  dihmeetbN  41808  dihmeetlem10N  41821  dihmeetlem12N  41823  dihmeetlem15N  41826  dihmeetALTN  41832  dih1dimatlem0  41833  dihjatcclem3  41925  dihjatcclem4  41926  mapdpglem22  42198  hdmap14lem1a  42371  eldioph2b  43225  jm2.19lem4  43450  jm2.19  43451  jm2.26a  43458  jm2.26  43460  hbtlem2  43582  fnchoice  45490  stoweidlem42  46497  stoweidlem59  46514  fourierdlem42  46604  zplusmodne  47824  minusmod5ne  47830