Theorem syl121anc 1377

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 1373	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:  syl122anc  1381  fsnunf2  7160  tfisi  7835  fnsuppeq0  8171  ttrclss  9673  ttrclselem2  9679  axdc4lem  10408  div32d  11981  div13d  11982  expdivd  14125  swrdsbslen  14629  sumeven  16357  sumodd  16358  pcqmul  16824  pcid  16844  pcneg  16845  pc2dvds  16850  pcz  16852  pcaddlem  16859  pcadd  16860  pcmpt2  16864  pcbc  16871  qexpz  16872  expnprm  16873  sylow1lem1  19528  ringurd  20094  lspsneleq  21025  lspsneq  21032  lspfixed  21038  frlmsslss2  21684  chmatval  22716  chpmat1dlem  22722  chpdmatlem2  22726  ucncn  24172  ucnextcn  24191  ssblex  24316  prdsxmslem2  24417  ncvs1  25057  voliunlem1  25451  deg1mul3le  26022  deg1pw  26026  fta1blem  26076  bcmono  27188  dchrisum0flblem1  27419  dchrisum0flblem2  27420  pntibndlem1  27500  pntlemr  27513  nosupbnd1  27626  noinfbnd1  27641  noetalem1  27653  slerec  27731  finsumvtxdg2sstep  29477  umgr3cyclex  30112  nv1  30604  resf1o  32653  omndmul3  33027  symgcntz  33042  cycpmco2lem6  33088  tocyccntz  33101  deg1vr  33558  rtelextdg2lem  33716  measun  34201  measvuni  34204  measunl  34206  btwnconn1lem14  36088  segcon2  36093  seglelin  36104  neibastop3  36350  upixp  37723  fdc  37739  eqlkr3  39094  lkrshp  39098  lfl1dim  39114  lfl1dim2N  39115  eqlkr4  39158  2llnneN  39403  3dim2  39462  4atlem3  39590  4atlem11  39603  4atlem12  39606  pexmidlem4N  39967  lhp2at0nle  40029  lhple  40036  ltrnideq  40169  cdlemd9  40200  cdleme0ex2N  40218  cdleme0moN  40219  cdleme11a  40254  cdleme30a  40372  cdlemefs32sn1aw  40408  cdleme43fsv1snlem  40414  cdlemefs31fv1  40418  cdlemefs45eN  40425  cdleme41sn3a  40427  cdleme35h  40450  cdleme36a  40454  cdleme40m  40461  cdleme40n  40462  cdleme41sn3aw  40468  cdleme42h  40476  cdleme42k  40478  cdleme42mN  40481  cdleme43cN  40485  cdleme17d3  40490  cdleme48fvg  40494  cdlemeg47rv2  40504  cdlemeg46c  40507  cdlemeg46sfg  40514  cdlemeg46rjgN  40516  cdlemeg46rgv  40522  cdlemeg46req  40523  cdlemeg46gfv  40524  cdlemeg46gfre  40526  cdlemeg49lebilem  40533  cdleme50trn2  40545  cdlemg2kq  40596  cdlemb3  40600  cdlemg4f  40609  cdlemg9a  40626  cdlemg9b  40627  cdlemg9  40628  cdlemg11aq  40632  cdlemg12a  40637  cdlemg12b  40638  cdlemg12c  40639  cdlemg12d  40640  cdlemg12f  40642  cdlemg12g  40643  cdlemg12  40644  cdlemg13a  40645  cdlemg16  40651  cdlemg17e  40659  cdlemg17f  40660  cdlemg17g  40661  cdlemg17ir  40664  cdlemg17  40671  cdlemg18b  40673  cdlemg18c  40674  cdlemg33e  40704  trlcoabs2N  40716  trlcocnvat  40718  trlcolem  40720  trlco  40721  cdlemg44  40727  cdlemg47  40730  ltrncom  40732  tendococl  40766  tendoplcl  40775  tendoplcom  40776  tendoplass  40777  tendodi1  40778  tendodi2  40779  tendo0pl  40785  tendoipl  40791  cdlemh1  40809  cdlemi2  40813  tendo0mul  40820  tendo0mulr  40821  cdlemk2  40826  cdlemk3  40827  cdlemk4  40828  cdlemk6  40831  cdlemk8  40832  cdlemk12  40844  cdlemkole  40847  cdlemk14  40848  cdlemk15  40849  cdlemk5u  40855  cdlemk6u  40856  cdlemk12u  40866  cdlemkfid1N  40915  cdlemk19x  40937  cdlemk48  40944  cdlemk53a  40949  cdlemk56  40965  cdleml2N  40971  cdleml3N  40972  cdleml6  40975  cdleml7  40976  dva1dim  40979  dia2dimlem4  41061  dvhlveclem  41102  doca2N  41120  djajN  41131  cdlemn2a  41190  cdlemn3  41191  dihordlem6  41207  dihord5apre  41256  dihglbcpreN  41294  dihmeetcN  41296  dihmeetbN  41297  dihmeetlem10N  41310  dihmeetlem12N  41312  dihmeetlem15N  41315  dihmeetALTN  41321  dih1dimatlem0  41322  dihjatcclem3  41414  dihjatcclem4  41415  mapdpglem22  41687  hdmap14lem1a  41860  eldioph2b  42751  jm2.19lem4  42981  jm2.19  42982  jm2.26a  42989  jm2.26  42991  hbtlem2  43113  fnchoice  45023  stoweidlem42  46040  stoweidlem59  46057  fourierdlem42  46147  zplusmodne  47344  minusmod5ne  47350