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  7122  tfisi  7792  fnsuppeq0  8125  ttrclss  9616  ttrclselem2  9622  axdc4lem  10349  div32d  11923  div13d  11924  expdivd  14067  swrdsbslen  14571  sumeven  16298  sumodd  16299  pcqmul  16765  pcid  16785  pcneg  16786  pc2dvds  16791  pcz  16793  pcaddlem  16800  pcadd  16801  pcmpt2  16805  pcbc  16812  qexpz  16813  expnprm  16814  sylow1lem1  19477  omndmul3  20013  ringurd  20070  lspsneleq  21022  lspsneq  21029  lspfixed  21035  frlmsslss2  21682  chmatval  22714  chpmat1dlem  22720  chpdmatlem2  22724  ucncn  24170  ucnextcn  24189  ssblex  24314  prdsxmslem2  24415  ncvs1  25055  voliunlem1  25449  deg1mul3le  26020  deg1pw  26024  fta1blem  26074  bcmono  27186  dchrisum0flblem1  27417  dchrisum0flblem2  27418  pntibndlem1  27498  pntlemr  27511  nosupbnd1  27624  noinfbnd1  27639  noetalem1  27651  slerec  27731  finsumvtxdg2sstep  29499  umgr3cyclex  30131  nv1  30623  resf1o  32682  symgcntz  33036  cycpmco2lem6  33082  tocyccntz  33095  deg1vr  33534  rtelextdg2lem  33709  measun  34194  measvuni  34197  measunl  34199  btwnconn1lem14  36094  segcon2  36099  seglelin  36110  neibastop3  36356  upixp  37729  fdc  37745  eqlkr3  39100  lkrshp  39104  lfl1dim  39120  lfl1dim2N  39121  eqlkr4  39164  2llnneN  39408  3dim2  39467  4atlem3  39595  4atlem11  39608  4atlem12  39611  pexmidlem4N  39972  lhp2at0nle  40034  lhple  40041  ltrnideq  40174  cdlemd9  40205  cdleme0ex2N  40223  cdleme0moN  40224  cdleme11a  40259  cdleme30a  40377  cdlemefs32sn1aw  40413  cdleme43fsv1snlem  40419  cdlemefs31fv1  40423  cdlemefs45eN  40430  cdleme41sn3a  40432  cdleme35h  40455  cdleme36a  40459  cdleme40m  40466  cdleme40n  40467  cdleme41sn3aw  40473  cdleme42h  40481  cdleme42k  40483  cdleme42mN  40486  cdleme43cN  40490  cdleme17d3  40495  cdleme48fvg  40499  cdlemeg47rv2  40509  cdlemeg46c  40512  cdlemeg46sfg  40519  cdlemeg46rjgN  40521  cdlemeg46rgv  40527  cdlemeg46req  40528  cdlemeg46gfv  40529  cdlemeg46gfre  40531  cdlemeg49lebilem  40538  cdleme50trn2  40550  cdlemg2kq  40601  cdlemb3  40605  cdlemg4f  40614  cdlemg9a  40631  cdlemg9b  40632  cdlemg9  40633  cdlemg11aq  40637  cdlemg12a  40642  cdlemg12b  40643  cdlemg12c  40644  cdlemg12d  40645  cdlemg12f  40647  cdlemg12g  40648  cdlemg12  40649  cdlemg13a  40650  cdlemg16  40656  cdlemg17e  40664  cdlemg17f  40665  cdlemg17g  40666  cdlemg17ir  40669  cdlemg17  40676  cdlemg18b  40678  cdlemg18c  40679  cdlemg33e  40709  trlcoabs2N  40721  trlcocnvat  40723  trlcolem  40725  trlco  40726  cdlemg44  40732  cdlemg47  40735  ltrncom  40737  tendococl  40771  tendoplcl  40780  tendoplcom  40781  tendoplass  40782  tendodi1  40783  tendodi2  40784  tendo0pl  40790  tendoipl  40796  cdlemh1  40814  cdlemi2  40818  tendo0mul  40825  tendo0mulr  40826  cdlemk2  40831  cdlemk3  40832  cdlemk4  40833  cdlemk6  40836  cdlemk8  40837  cdlemk12  40849  cdlemkole  40852  cdlemk14  40853  cdlemk15  40854  cdlemk5u  40860  cdlemk6u  40861  cdlemk12u  40871  cdlemkfid1N  40920  cdlemk19x  40942  cdlemk48  40949  cdlemk53a  40954  cdlemk56  40970  cdleml2N  40976  cdleml3N  40977  cdleml6  40980  cdleml7  40981  dva1dim  40984  dia2dimlem4  41066  dvhlveclem  41107  doca2N  41125  djajN  41136  cdlemn2a  41195  cdlemn3  41196  dihordlem6  41212  dihord5apre  41261  dihglbcpreN  41299  dihmeetcN  41301  dihmeetbN  41302  dihmeetlem10N  41315  dihmeetlem12N  41317  dihmeetlem15N  41320  dihmeetALTN  41326  dih1dimatlem0  41327  dihjatcclem3  41419  dihjatcclem4  41420  mapdpglem22  41692  hdmap14lem1a  41865  eldioph2b  42756  jm2.19lem4  42985  jm2.19  42986  jm2.26a  42993  jm2.26  42995  hbtlem2  43117  fnchoice  45027  stoweidlem42  46043  stoweidlem59  46060  fourierdlem42  46150  zplusmodne  47347  minusmod5ne  47353