Theorem syl121anc 1372

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

Syntax hints:   → wi 4   ∧ wa 394   ∧ w3a 1084

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 395  df-3an 1086

This theorem is referenced by:  syl122anc  1376  fsnunf2  7200  tfisi  7869  fnsuppeq0  8206  ttrclss  9763  ttrclselem2  9769  axdc4lem  10498  div32d  12064  div13d  12065  expdivd  14179  swrdsbslen  14672  sumeven  16389  sumodd  16390  pcqmul  16855  pcid  16875  pcneg  16876  pc2dvds  16881  pcz  16883  pcaddlem  16890  pcadd  16891  pcmpt2  16895  pcbc  16902  qexpz  16903  expnprm  16904  sylow1lem1  19596  ringurd  20168  lspsneleq  21096  lspsneq  21103  lspfixed  21109  frlmsslss2  21773  chmatval  22822  chpmat1dlem  22828  chpdmatlem2  22832  ucncn  24281  ucnextcn  24300  ssblex  24425  prdsxmslem2  24529  ncvs1  25176  voliunlem1  25570  deg1mul3le  26144  deg1pw  26148  fta1blem  26198  bcmono  27306  dchrisum0flblem1  27537  dchrisum0flblem2  27538  pntibndlem1  27618  pntlemr  27631  nosupbnd1  27744  noinfbnd1  27759  noetalem1  27771  slerec  27849  finsumvtxdg2sstep  29486  umgr3cyclex  30116  nv1  30608  resf1o  32644  omndmul3  32948  symgcntz  32963  cycpmco2lem6  33009  tocyccntz  33022  deg1vr  33461  rtelextdg2lem  33604  measun  34044  measvuni  34047  measunl  34049  btwnconn1lem14  35924  segcon2  35929  seglelin  35940  neibastop3  36074  upixp  37430  fdc  37446  eqlkr3  38799  lkrshp  38803  lfl1dim  38819  lfl1dim2N  38820  eqlkr4  38863  2llnneN  39108  3dim2  39167  4atlem3  39295  4atlem11  39308  4atlem12  39311  pexmidlem4N  39672  lhp2at0nle  39734  lhple  39741  ltrnideq  39874  cdlemd9  39905  cdleme0ex2N  39923  cdleme0moN  39924  cdleme11a  39959  cdleme30a  40077  cdlemefs32sn1aw  40113  cdleme43fsv1snlem  40119  cdlemefs31fv1  40123  cdlemefs45eN  40130  cdleme41sn3a  40132  cdleme35h  40155  cdleme36a  40159  cdleme40m  40166  cdleme40n  40167  cdleme41sn3aw  40173  cdleme42h  40181  cdleme42k  40183  cdleme42mN  40186  cdleme43cN  40190  cdleme17d3  40195  cdleme48fvg  40199  cdlemeg47rv2  40209  cdlemeg46c  40212  cdlemeg46sfg  40219  cdlemeg46rjgN  40221  cdlemeg46rgv  40227  cdlemeg46req  40228  cdlemeg46gfv  40229  cdlemeg46gfre  40231  cdlemeg49lebilem  40238  cdleme50trn2  40250  cdlemg2kq  40301  cdlemb3  40305  cdlemg4f  40314  cdlemg9a  40331  cdlemg9b  40332  cdlemg9  40333  cdlemg11aq  40337  cdlemg12a  40342  cdlemg12b  40343  cdlemg12c  40344  cdlemg12d  40345  cdlemg12f  40347  cdlemg12g  40348  cdlemg12  40349  cdlemg13a  40350  cdlemg16  40356  cdlemg17e  40364  cdlemg17f  40365  cdlemg17g  40366  cdlemg17ir  40369  cdlemg17  40376  cdlemg18b  40378  cdlemg18c  40379  cdlemg33e  40409  trlcoabs2N  40421  trlcocnvat  40423  trlcolem  40425  trlco  40426  cdlemg44  40432  cdlemg47  40435  ltrncom  40437  tendococl  40471  tendoplcl  40480  tendoplcom  40481  tendoplass  40482  tendodi1  40483  tendodi2  40484  tendo0pl  40490  tendoipl  40496  cdlemh1  40514  cdlemi2  40518  tendo0mul  40525  tendo0mulr  40526  cdlemk2  40531  cdlemk3  40532  cdlemk4  40533  cdlemk6  40536  cdlemk8  40537  cdlemk12  40549  cdlemkole  40552  cdlemk14  40553  cdlemk15  40554  cdlemk5u  40560  cdlemk6u  40561  cdlemk12u  40571  cdlemkfid1N  40620  cdlemk19x  40642  cdlemk48  40649  cdlemk53a  40654  cdlemk56  40670  cdleml2N  40676  cdleml3N  40677  cdleml6  40680  cdleml7  40681  dva1dim  40684  dia2dimlem4  40766  dvhlveclem  40807  doca2N  40825  djajN  40836  cdlemn2a  40895  cdlemn3  40896  dihordlem6  40912  dihord5apre  40961  dihglbcpreN  40999  dihmeetcN  41001  dihmeetbN  41002  dihmeetlem10N  41015  dihmeetlem12N  41017  dihmeetlem15N  41020  dihmeetALTN  41026  dih1dimatlem0  41027  dihjatcclem3  41119  dihjatcclem4  41120  mapdpglem22  41392  hdmap14lem1a  41565  eldioph2b  42420  jm2.19lem4  42650  jm2.19  42651  jm2.26a  42658  jm2.26  42660  hbtlem2  42785  fnchoice  44628  stoweidlem42  45663  stoweidlem59  45680  fourierdlem42  45770