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  7120  tfisi  7789  fnsuppeq0  8122  ttrclss  9610  ttrclselem2  9616  axdc4lem  10343  div32d  11917  div13d  11918  expdivd  14064  swrdsbslen  14569  sumeven  16295  sumodd  16296  pcqmul  16762  pcid  16782  pcneg  16783  pc2dvds  16788  pcz  16790  pcaddlem  16797  pcadd  16798  pcmpt2  16802  pcbc  16809  qexpz  16810  expnprm  16811  sylow1lem1  19508  omndmul3  20044  ringurd  20101  lspsneleq  21050  lspsneq  21057  lspfixed  21063  frlmsslss2  21710  chmatval  22742  chpmat1dlem  22748  chpdmatlem2  22752  ucncn  24197  ucnextcn  24216  ssblex  24341  prdsxmslem2  24442  ncvs1  25082  voliunlem1  25476  deg1mul3le  26047  deg1pw  26051  fta1blem  26101  bcmono  27213  dchrisum0flblem1  27444  dchrisum0flblem2  27445  pntibndlem1  27525  pntlemr  27538  nosupbnd1  27651  noinfbnd1  27666  noetalem1  27678  slerec  27758  finsumvtxdg2sstep  29526  umgr3cyclex  30158  nv1  30650  resf1o  32708  symgcntz  33049  cycpmco2lem6  33095  tocyccntz  33108  deg1vr  33548  rtelextdg2lem  33734  measun  34219  measvuni  34222  measunl  34224  btwnconn1lem14  36133  segcon2  36138  seglelin  36149  neibastop3  36395  upixp  37768  fdc  37784  eqlkr3  39139  lkrshp  39143  lfl1dim  39159  lfl1dim2N  39160  eqlkr4  39203  2llnneN  39447  3dim2  39506  4atlem3  39634  4atlem11  39647  4atlem12  39650  pexmidlem4N  40011  lhp2at0nle  40073  lhple  40080  ltrnideq  40213  cdlemd9  40244  cdleme0ex2N  40262  cdleme0moN  40263  cdleme11a  40298  cdleme30a  40416  cdlemefs32sn1aw  40452  cdleme43fsv1snlem  40458  cdlemefs31fv1  40462  cdlemefs45eN  40469  cdleme41sn3a  40471  cdleme35h  40494  cdleme36a  40498  cdleme40m  40505  cdleme40n  40506  cdleme41sn3aw  40512  cdleme42h  40520  cdleme42k  40522  cdleme42mN  40525  cdleme43cN  40529  cdleme17d3  40534  cdleme48fvg  40538  cdlemeg47rv2  40548  cdlemeg46c  40551  cdlemeg46sfg  40558  cdlemeg46rjgN  40560  cdlemeg46rgv  40566  cdlemeg46req  40567  cdlemeg46gfv  40568  cdlemeg46gfre  40570  cdlemeg49lebilem  40577  cdleme50trn2  40589  cdlemg2kq  40640  cdlemb3  40644  cdlemg4f  40653  cdlemg9a  40670  cdlemg9b  40671  cdlemg9  40672  cdlemg11aq  40676  cdlemg12a  40681  cdlemg12b  40682  cdlemg12c  40683  cdlemg12d  40684  cdlemg12f  40686  cdlemg12g  40687  cdlemg12  40688  cdlemg13a  40689  cdlemg16  40695  cdlemg17e  40703  cdlemg17f  40704  cdlemg17g  40705  cdlemg17ir  40708  cdlemg17  40715  cdlemg18b  40717  cdlemg18c  40718  cdlemg33e  40748  trlcoabs2N  40760  trlcocnvat  40762  trlcolem  40764  trlco  40765  cdlemg44  40771  cdlemg47  40774  ltrncom  40776  tendococl  40810  tendoplcl  40819  tendoplcom  40820  tendoplass  40821  tendodi1  40822  tendodi2  40823  tendo0pl  40829  tendoipl  40835  cdlemh1  40853  cdlemi2  40857  tendo0mul  40864  tendo0mulr  40865  cdlemk2  40870  cdlemk3  40871  cdlemk4  40872  cdlemk6  40875  cdlemk8  40876  cdlemk12  40888  cdlemkole  40891  cdlemk14  40892  cdlemk15  40893  cdlemk5u  40899  cdlemk6u  40900  cdlemk12u  40910  cdlemkfid1N  40959  cdlemk19x  40981  cdlemk48  40988  cdlemk53a  40993  cdlemk56  41009  cdleml2N  41015  cdleml3N  41016  cdleml6  41019  cdleml7  41020  dva1dim  41023  dia2dimlem4  41105  dvhlveclem  41146  doca2N  41164  djajN  41175  cdlemn2a  41234  cdlemn3  41235  dihordlem6  41251  dihord5apre  41300  dihglbcpreN  41338  dihmeetcN  41340  dihmeetbN  41341  dihmeetlem10N  41354  dihmeetlem12N  41356  dihmeetlem15N  41359  dihmeetALTN  41365  dih1dimatlem0  41366  dihjatcclem3  41458  dihjatcclem4  41459  mapdpglem22  41731  hdmap14lem1a  41904  eldioph2b  42795  jm2.19lem4  43024  jm2.19  43025  jm2.26a  43032  jm2.26  43034  hbtlem2  43156  fnchoice  45065  stoweidlem42  46079  stoweidlem59  46096  fourierdlem42  46186  zplusmodne  47373  minusmod5ne  47379