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  7186  tfisi  7850  fnsuppeq0  8179  ttrclss  9717  ttrclselem2  9723  axdc4lem  10452  div32d  12015  div13d  12016  expdivd  14127  swrdsbslen  14616  sumeven  16332  sumodd  16333  pcqmul  16788  pcid  16808  pcneg  16809  pc2dvds  16814  pcz  16816  pcaddlem  16823  pcadd  16824  pcmpt2  16828  pcbc  16835  qexpz  16836  expnprm  16837  sylow1lem1  19468  ringurd  20010  lspsneleq  20734  lspsneq  20741  lspfixed  20747  frlmsslss2  21336  chmatval  22338  chpmat1dlem  22344  chpdmatlem2  22348  ucncn  23797  ucnextcn  23816  ssblex  23941  prdsxmslem2  24045  ncvs1  24681  voliunlem1  25074  deg1mul3le  25641  deg1pw  25645  fta1blem  25693  bcmono  26787  dchrisum0flblem1  27018  dchrisum0flblem2  27019  pntibndlem1  27099  pntlemr  27112  nosupbnd1  27224  noinfbnd1  27239  noetalem1  27251  slerec  27328  finsumvtxdg2sstep  28844  umgr3cyclex  29474  nv1  29966  resf1o  31993  omndmul3  32272  symgcntz  32287  cycpmco2lem6  32331  tocyccntz  32344  measun  33278  measvuni  33281  measunl  33283  btwnconn1lem14  35141  segcon2  35146  seglelin  35157  neibastop3  35333  upixp  36683  fdc  36699  eqlkr3  38057  lkrshp  38061  lfl1dim  38077  lfl1dim2N  38078  eqlkr4  38121  2llnneN  38366  3dim2  38425  4atlem3  38553  4atlem11  38566  4atlem12  38569  pexmidlem4N  38930  lhp2at0nle  38992  lhple  38999  ltrnideq  39132  cdlemd9  39163  cdleme0ex2N  39181  cdleme0moN  39182  cdleme11a  39217  cdleme30a  39335  cdlemefs32sn1aw  39371  cdleme43fsv1snlem  39377  cdlemefs31fv1  39381  cdlemefs45eN  39388  cdleme41sn3a  39390  cdleme35h  39413  cdleme36a  39417  cdleme40m  39424  cdleme40n  39425  cdleme41sn3aw  39431  cdleme42h  39439  cdleme42k  39441  cdleme42mN  39444  cdleme43cN  39448  cdleme17d3  39453  cdleme48fvg  39457  cdlemeg47rv2  39467  cdlemeg46c  39470  cdlemeg46sfg  39477  cdlemeg46rjgN  39479  cdlemeg46rgv  39485  cdlemeg46req  39486  cdlemeg46gfv  39487  cdlemeg46gfre  39489  cdlemeg49lebilem  39496  cdleme50trn2  39508  cdlemg2kq  39559  cdlemb3  39563  cdlemg4f  39572  cdlemg9a  39589  cdlemg9b  39590  cdlemg9  39591  cdlemg11aq  39595  cdlemg12a  39600  cdlemg12b  39601  cdlemg12c  39602  cdlemg12d  39603  cdlemg12f  39605  cdlemg12g  39606  cdlemg12  39607  cdlemg13a  39608  cdlemg16  39614  cdlemg17e  39622  cdlemg17f  39623  cdlemg17g  39624  cdlemg17ir  39627  cdlemg17  39634  cdlemg18b  39636  cdlemg18c  39637  cdlemg33e  39667  trlcoabs2N  39679  trlcocnvat  39681  trlcolem  39683  trlco  39684  cdlemg44  39690  cdlemg47  39693  ltrncom  39695  tendococl  39729  tendoplcl  39738  tendoplcom  39739  tendoplass  39740  tendodi1  39741  tendodi2  39742  tendo0pl  39748  tendoipl  39754  cdlemh1  39772  cdlemi2  39776  tendo0mul  39783  tendo0mulr  39784  cdlemk2  39789  cdlemk3  39790  cdlemk4  39791  cdlemk6  39794  cdlemk8  39795  cdlemk12  39807  cdlemkole  39810  cdlemk14  39811  cdlemk15  39812  cdlemk5u  39818  cdlemk6u  39819  cdlemk12u  39829  cdlemkfid1N  39878  cdlemk19x  39900  cdlemk48  39907  cdlemk53a  39912  cdlemk56  39928  cdleml2N  39934  cdleml3N  39935  cdleml6  39938  cdleml7  39939  dva1dim  39942  dia2dimlem4  40024  dvhlveclem  40065  doca2N  40083  djajN  40094  cdlemn2a  40153  cdlemn3  40154  dihordlem6  40170  dihord5apre  40219  dihglbcpreN  40257  dihmeetcN  40259  dihmeetbN  40260  dihmeetlem10N  40273  dihmeetlem12N  40275  dihmeetlem15N  40278  dihmeetALTN  40284  dih1dimatlem0  40285  dihjatcclem3  40377  dihjatcclem4  40378  mapdpglem22  40650  hdmap14lem1a  40823  eldioph2b  41583  jm2.19lem4  41813  jm2.19  41814  jm2.26a  41821  jm2.26  41823  hbtlem2  41948  fnchoice  43795  stoweidlem42  44837  stoweidlem59  44854  fourierdlem42  44944