Theorem syl121anc 1375

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

Syntax hints:   → wi 4   ∧ wa 396   ∧ w3a 1087

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 397  df-3an 1089

This theorem is referenced by:  syl122anc  1379  fsnunf2  7180  tfisi  7844  fnsuppeq0  8173  ttrclss  9711  ttrclselem2  9717  axdc4lem  10446  div32d  12009  div13d  12010  expdivd  14121  swrdsbslen  14610  sumeven  16326  sumodd  16327  pcqmul  16782  pcid  16802  pcneg  16803  pc2dvds  16808  pcz  16810  pcaddlem  16817  pcadd  16818  pcmpt2  16822  pcbc  16829  qexpz  16830  expnprm  16831  sylow1lem1  19460  lspsneleq  20720  lspsneq  20727  lspfixed  20733  frlmsslss2  21321  chmatval  22322  chpmat1dlem  22328  chpdmatlem2  22332  ucncn  23781  ucnextcn  23800  ssblex  23925  prdsxmslem2  24029  ncvs1  24665  voliunlem1  25058  deg1mul3le  25625  deg1pw  25629  fta1blem  25677  bcmono  26769  dchrisum0flblem1  27000  dchrisum0flblem2  27001  pntibndlem1  27081  pntlemr  27094  nosupbnd1  27206  noinfbnd1  27221  noetalem1  27233  slerec  27309  finsumvtxdg2sstep  28795  umgr3cyclex  29425  nv1  29915  resf1o  31942  omndmul3  32218  symgcntz  32233  cycpmco2lem6  32277  tocyccntz  32290  rngurd  32367  measun  33197  measvuni  33200  measunl  33202  btwnconn1lem14  35060  segcon2  35065  seglelin  35076  neibastop3  35235  upixp  36585  fdc  36601  eqlkr3  37959  lkrshp  37963  lfl1dim  37979  lfl1dim2N  37980  eqlkr4  38023  2llnneN  38268  3dim2  38327  4atlem3  38455  4atlem11  38468  4atlem12  38471  pexmidlem4N  38832  lhp2at0nle  38894  lhple  38901  ltrnideq  39034  cdlemd9  39065  cdleme0ex2N  39083  cdleme0moN  39084  cdleme11a  39119  cdleme30a  39237  cdlemefs32sn1aw  39273  cdleme43fsv1snlem  39279  cdlemefs31fv1  39283  cdlemefs45eN  39290  cdleme41sn3a  39292  cdleme35h  39315  cdleme36a  39319  cdleme40m  39326  cdleme40n  39327  cdleme41sn3aw  39333  cdleme42h  39341  cdleme42k  39343  cdleme42mN  39346  cdleme43cN  39350  cdleme17d3  39355  cdleme48fvg  39359  cdlemeg47rv2  39369  cdlemeg46c  39372  cdlemeg46sfg  39379  cdlemeg46rjgN  39381  cdlemeg46rgv  39387  cdlemeg46req  39388  cdlemeg46gfv  39389  cdlemeg46gfre  39391  cdlemeg49lebilem  39398  cdleme50trn2  39410  cdlemg2kq  39461  cdlemb3  39465  cdlemg4f  39474  cdlemg9a  39491  cdlemg9b  39492  cdlemg9  39493  cdlemg11aq  39497  cdlemg12a  39502  cdlemg12b  39503  cdlemg12c  39504  cdlemg12d  39505  cdlemg12f  39507  cdlemg12g  39508  cdlemg12  39509  cdlemg13a  39510  cdlemg16  39516  cdlemg17e  39524  cdlemg17f  39525  cdlemg17g  39526  cdlemg17ir  39529  cdlemg17  39536  cdlemg18b  39538  cdlemg18c  39539  cdlemg33e  39569  trlcoabs2N  39581  trlcocnvat  39583  trlcolem  39585  trlco  39586  cdlemg44  39592  cdlemg47  39595  ltrncom  39597  tendococl  39631  tendoplcl  39640  tendoplcom  39641  tendoplass  39642  tendodi1  39643  tendodi2  39644  tendo0pl  39650  tendoipl  39656  cdlemh1  39674  cdlemi2  39678  tendo0mul  39685  tendo0mulr  39686  cdlemk2  39691  cdlemk3  39692  cdlemk4  39693  cdlemk6  39696  cdlemk8  39697  cdlemk12  39709  cdlemkole  39712  cdlemk14  39713  cdlemk15  39714  cdlemk5u  39720  cdlemk6u  39721  cdlemk12u  39731  cdlemkfid1N  39780  cdlemk19x  39802  cdlemk48  39809  cdlemk53a  39814  cdlemk56  39830  cdleml2N  39836  cdleml3N  39837  cdleml6  39840  cdleml7  39841  dva1dim  39844  dia2dimlem4  39926  dvhlveclem  39967  doca2N  39985  djajN  39996  cdlemn2a  40055  cdlemn3  40056  dihordlem6  40072  dihord5apre  40121  dihglbcpreN  40159  dihmeetcN  40161  dihmeetbN  40162  dihmeetlem10N  40175  dihmeetlem12N  40177  dihmeetlem15N  40180  dihmeetALTN  40186  dih1dimatlem0  40187  dihjatcclem3  40279  dihjatcclem4  40280  mapdpglem22  40552  hdmap14lem1a  40725  eldioph2b  41486  jm2.19lem4  41716  jm2.19  41717  jm2.26a  41724  jm2.26  41726  hbtlem2  41851  fnchoice  43698  stoweidlem42  44744  stoweidlem59  44761  fourierdlem42  44851