Theorem syl121anc 1373

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

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

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 206  df-an 396  df-3an 1087

This theorem is referenced by:  syl122anc  1377  fsnunf2  7040  tfisi  7680  fnsuppeq0  7979  axdc4lem  10142  div32d  11704  div13d  11705  expdivd  13806  swrdsbslen  14305  sumeven  16024  sumodd  16025  pcqmul  16482  pcid  16502  pcneg  16503  pc2dvds  16508  pcz  16510  pcaddlem  16517  pcadd  16518  pcmpt2  16522  pcbc  16529  qexpz  16530  expnprm  16531  sylow1lem1  19118  lspsneleq  20292  lspsneq  20299  lspfixed  20305  frlmsslss2  20892  chmatval  21886  chpmat1dlem  21892  chpdmatlem2  21896  ucncn  23345  ucnextcn  23364  ssblex  23489  prdsxmslem2  23591  ncvs1  24226  voliunlem1  24619  deg1mul3le  25186  deg1pw  25190  fta1blem  25238  bcmono  26330  dchrisum0flblem1  26561  dchrisum0flblem2  26562  pntibndlem1  26642  pntlemr  26655  finsumvtxdg2sstep  27819  umgr3cyclex  28448  nv1  28938  resf1o  30967  omndmul3  31241  symgcntz  31256  cycpmco2lem6  31300  tocyccntz  31313  rngurd  31384  measun  32079  measvuni  32082  measunl  32084  ttrclss  33706  ttrclselem2  33712  nosupbnd1  33844  noinfbnd1  33859  noetalem1  33871  slerec  33940  btwnconn1lem14  34329  segcon2  34334  seglelin  34345  neibastop3  34478  upixp  35814  fdc  35830  eqlkr3  37042  lkrshp  37046  lfl1dim  37062  lfl1dim2N  37063  eqlkr4  37106  2llnneN  37350  3dim2  37409  4atlem3  37537  4atlem11  37550  4atlem12  37553  pexmidlem4N  37914  lhp2at0nle  37976  lhple  37983  ltrnideq  38116  cdlemd9  38147  cdleme0ex2N  38165  cdleme0moN  38166  cdleme11a  38201  cdleme30a  38319  cdlemefs32sn1aw  38355  cdleme43fsv1snlem  38361  cdlemefs31fv1  38365  cdlemefs45eN  38372  cdleme41sn3a  38374  cdleme35h  38397  cdleme36a  38401  cdleme40m  38408  cdleme40n  38409  cdleme41sn3aw  38415  cdleme42h  38423  cdleme42k  38425  cdleme42mN  38428  cdleme43cN  38432  cdleme17d3  38437  cdleme48fvg  38441  cdlemeg47rv2  38451  cdlemeg46c  38454  cdlemeg46sfg  38461  cdlemeg46rjgN  38463  cdlemeg46rgv  38469  cdlemeg46req  38470  cdlemeg46gfv  38471  cdlemeg46gfre  38473  cdlemeg49lebilem  38480  cdleme50trn2  38492  cdlemg2kq  38543  cdlemb3  38547  cdlemg4f  38556  cdlemg9a  38573  cdlemg9b  38574  cdlemg9  38575  cdlemg11aq  38579  cdlemg12a  38584  cdlemg12b  38585  cdlemg12c  38586  cdlemg12d  38587  cdlemg12f  38589  cdlemg12g  38590  cdlemg12  38591  cdlemg13a  38592  cdlemg16  38598  cdlemg17e  38606  cdlemg17f  38607  cdlemg17g  38608  cdlemg17ir  38611  cdlemg17  38618  cdlemg18b  38620  cdlemg18c  38621  cdlemg33e  38651  trlcoabs2N  38663  trlcocnvat  38665  trlcolem  38667  trlco  38668  cdlemg44  38674  cdlemg47  38677  ltrncom  38679  tendococl  38713  tendoplcl  38722  tendoplcom  38723  tendoplass  38724  tendodi1  38725  tendodi2  38726  tendo0pl  38732  tendoipl  38738  cdlemh1  38756  cdlemi2  38760  tendo0mul  38767  tendo0mulr  38768  cdlemk2  38773  cdlemk3  38774  cdlemk4  38775  cdlemk6  38778  cdlemk8  38779  cdlemk12  38791  cdlemkole  38794  cdlemk14  38795  cdlemk15  38796  cdlemk5u  38802  cdlemk6u  38803  cdlemk12u  38813  cdlemkfid1N  38862  cdlemk19x  38884  cdlemk48  38891  cdlemk53a  38896  cdlemk56  38912  cdleml2N  38918  cdleml3N  38919  cdleml6  38922  cdleml7  38923  dva1dim  38926  dia2dimlem4  39008  dvhlveclem  39049  doca2N  39067  djajN  39078  cdlemn2a  39137  cdlemn3  39138  dihordlem6  39154  dihord5apre  39203  dihglbcpreN  39241  dihmeetcN  39243  dihmeetbN  39244  dihmeetlem10N  39257  dihmeetlem12N  39259  dihmeetlem15N  39262  dihmeetALTN  39268  dih1dimatlem0  39269  dihjatcclem3  39361  dihjatcclem4  39362  mapdpglem22  39634  hdmap14lem1a  39807  eldioph2b  40501  jm2.19lem4  40730  jm2.19  40731  jm2.26a  40738  jm2.26  40740  hbtlem2  40865  fnchoice  42461  stoweidlem42  43473  stoweidlem59  43490  fourierdlem42  43580