Theorem syl121anc 1374

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 1370	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  1378  fsnunf2  7205  tfisi  7879  fnsuppeq0  8215  ttrclss  9757  ttrclselem2  9763  axdc4lem  10492  div32d  12063  div13d  12064  expdivd  14196  swrdsbslen  14698  sumeven  16420  sumodd  16421  pcqmul  16886  pcid  16906  pcneg  16907  pc2dvds  16912  pcz  16914  pcaddlem  16921  pcadd  16922  pcmpt2  16926  pcbc  16933  qexpz  16934  expnprm  16935  sylow1lem1  19630  ringurd  20202  lspsneleq  21134  lspsneq  21141  lspfixed  21147  frlmsslss2  21812  chmatval  22850  chpmat1dlem  22856  chpdmatlem2  22860  ucncn  24309  ucnextcn  24328  ssblex  24453  prdsxmslem2  24557  ncvs1  25204  voliunlem1  25598  deg1mul3le  26170  deg1pw  26174  fta1blem  26224  bcmono  27335  dchrisum0flblem1  27566  dchrisum0flblem2  27567  pntibndlem1  27647  pntlemr  27660  nosupbnd1  27773  noinfbnd1  27788  noetalem1  27800  slerec  27878  finsumvtxdg2sstep  29581  umgr3cyclex  30211  nv1  30703  resf1o  32747  omndmul3  33072  symgcntz  33087  cycpmco2lem6  33133  tocyccntz  33146  deg1vr  33593  rtelextdg2lem  33731  measun  34191  measvuni  34194  measunl  34196  btwnconn1lem14  36081  segcon2  36086  seglelin  36097  neibastop3  36344  upixp  37715  fdc  37731  eqlkr3  39082  lkrshp  39086  lfl1dim  39102  lfl1dim2N  39103  eqlkr4  39146  2llnneN  39391  3dim2  39450  4atlem3  39578  4atlem11  39591  4atlem12  39594  pexmidlem4N  39955  lhp2at0nle  40017  lhple  40024  ltrnideq  40157  cdlemd9  40188  cdleme0ex2N  40206  cdleme0moN  40207  cdleme11a  40242  cdleme30a  40360  cdlemefs32sn1aw  40396  cdleme43fsv1snlem  40402  cdlemefs31fv1  40406  cdlemefs45eN  40413  cdleme41sn3a  40415  cdleme35h  40438  cdleme36a  40442  cdleme40m  40449  cdleme40n  40450  cdleme41sn3aw  40456  cdleme42h  40464  cdleme42k  40466  cdleme42mN  40469  cdleme43cN  40473  cdleme17d3  40478  cdleme48fvg  40482  cdlemeg47rv2  40492  cdlemeg46c  40495  cdlemeg46sfg  40502  cdlemeg46rjgN  40504  cdlemeg46rgv  40510  cdlemeg46req  40511  cdlemeg46gfv  40512  cdlemeg46gfre  40514  cdlemeg49lebilem  40521  cdleme50trn2  40533  cdlemg2kq  40584  cdlemb3  40588  cdlemg4f  40597  cdlemg9a  40614  cdlemg9b  40615  cdlemg9  40616  cdlemg11aq  40620  cdlemg12a  40625  cdlemg12b  40626  cdlemg12c  40627  cdlemg12d  40628  cdlemg12f  40630  cdlemg12g  40631  cdlemg12  40632  cdlemg13a  40633  cdlemg16  40639  cdlemg17e  40647  cdlemg17f  40648  cdlemg17g  40649  cdlemg17ir  40652  cdlemg17  40659  cdlemg18b  40661  cdlemg18c  40662  cdlemg33e  40692  trlcoabs2N  40704  trlcocnvat  40706  trlcolem  40708  trlco  40709  cdlemg44  40715  cdlemg47  40718  ltrncom  40720  tendococl  40754  tendoplcl  40763  tendoplcom  40764  tendoplass  40765  tendodi1  40766  tendodi2  40767  tendo0pl  40773  tendoipl  40779  cdlemh1  40797  cdlemi2  40801  tendo0mul  40808  tendo0mulr  40809  cdlemk2  40814  cdlemk3  40815  cdlemk4  40816  cdlemk6  40819  cdlemk8  40820  cdlemk12  40832  cdlemkole  40835  cdlemk14  40836  cdlemk15  40837  cdlemk5u  40843  cdlemk6u  40844  cdlemk12u  40854  cdlemkfid1N  40903  cdlemk19x  40925  cdlemk48  40932  cdlemk53a  40937  cdlemk56  40953  cdleml2N  40959  cdleml3N  40960  cdleml6  40963  cdleml7  40964  dva1dim  40967  dia2dimlem4  41049  dvhlveclem  41090  doca2N  41108  djajN  41119  cdlemn2a  41178  cdlemn3  41179  dihordlem6  41195  dihord5apre  41244  dihglbcpreN  41282  dihmeetcN  41284  dihmeetbN  41285  dihmeetlem10N  41298  dihmeetlem12N  41300  dihmeetlem15N  41303  dihmeetALTN  41309  dih1dimatlem0  41310  dihjatcclem3  41402  dihjatcclem4  41403  mapdpglem22  41675  hdmap14lem1a  41848  eldioph2b  42750  jm2.19lem4  42980  jm2.19  42981  jm2.26a  42988  jm2.26  42990  hbtlem2  43112  fnchoice  44966  stoweidlem42  45997  stoweidlem59  46014  fourierdlem42  46104  zplusmodne  47282  minusmod5ne  47288