Theorem syl121anc 1396

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

Syntax hints:   → wi 4   ∧ wa 399   ∧ w3a 1099

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 209  df-an 400  df-3an 1101

This theorem is referenced by:  syl122anc  1400  fsnunf2  7172  tfisi  7841  fnsuppeq0  8174  ttrclss  9677  ttrclselem2  9683  axdc4lem  10414  div32d  11992  div13d  11993  expdivd  14175  swrdsbslen  14680  sumeven  16423  sumodd  16424  pcqmul  16891  pcid  16911  pcneg  16912  pc2dvds  16917  pcz  16919  pcaddlem  16926  pcadd  16927  pcmpt2  16931  pcbc  16938  qexpz  16939  expnprm  16940  sylow1lem1  19640  omndmul3  20176  ringurd  20237  lspsneleq  21187  lspsneq  21194  lspfixed  21200  frlmsslss2  21829  chmatval  22891  chpmat1dlem  22897  chpdmatlem2  22901  ucncn  24346  ucnextcn  24365  ssblex  24490  prdsxmslem2  24591  ncvs1  25221  voliunlem1  25614  deg1mul3le  26179  deg1pw  26183  fta1blem  26233  bcmono  27343  dchrisum0flblem1  27574  dchrisum0flblem2  27575  pntibndlem1  27655  pntlemr  27668  nosupbnd1  27780  noinfbnd1  27795  noetalem1  27807  lesrec  27894  finsumvtxdg2sstep  29752  umgr3cyclex  30387  nv1  30880  resf1o  32934  symgcntz  33267  cycpmco2lem6  33313  tocyccntz  33326  deg1vr  33790  rtelextdg2lem  34025  measun  34510  measvuni  34513  measunl  34515  btwnconn1lem14  36455  segcon2  36460  seglelin  36471  neibastop3  36727  upixp  38233  fdc  38249  eqlkr3  39730  lkrshp  39734  lfl1dim  39750  lfl1dim2N  39751  eqlkr4  39794  2llnneN  40038  3dim2  40097  4atlem3  40225  4atlem11  40238  4atlem12  40241  pexmidlem4N  40602  lhp2at0nle  40664  lhple  40671  ltrnideq  40804  cdlemd9  40835  cdleme0ex2N  40853  cdleme0moN  40854  cdleme11a  40889  cdleme30a  41007  cdlemefs32sn1aw  41043  cdleme43fsv1snlem  41049  cdlemefs31fv1  41053  cdlemefs45eN  41060  cdleme41sn3a  41062  cdleme35h  41085  cdleme36a  41089  cdleme40m  41096  cdleme40n  41097  cdleme41sn3aw  41103  cdleme42h  41111  cdleme42k  41113  cdleme42mN  41116  cdleme43cN  41120  cdleme17d3  41125  cdleme48fvg  41129  cdlemeg47rv2  41139  cdlemeg46c  41142  cdlemeg46sfg  41149  cdlemeg46rjgN  41151  cdlemeg46rgv  41157  cdlemeg46req  41158  cdlemeg46gfv  41159  cdlemeg46gfre  41161  cdlemeg49lebilem  41168  cdleme50trn2  41180  cdlemg2kq  41231  cdlemb3  41235  cdlemg4f  41244  cdlemg9a  41261  cdlemg9b  41262  cdlemg9  41263  cdlemg11aq  41267  cdlemg12a  41272  cdlemg12b  41273  cdlemg12c  41274  cdlemg12d  41275  cdlemg12f  41277  cdlemg12g  41278  cdlemg12  41279  cdlemg13a  41280  cdlemg16  41286  cdlemg17e  41294  cdlemg17f  41295  cdlemg17g  41296  cdlemg17ir  41299  cdlemg17  41306  cdlemg18b  41308  cdlemg18c  41309  cdlemg33e  41339  trlcoabs2N  41351  trlcocnvat  41353  trlcolem  41355  trlco  41356  cdlemg44  41362  cdlemg47  41365  ltrncom  41367  tendococl  41401  tendoplcl  41410  tendoplcom  41411  tendoplass  41412  tendodi1  41413  tendodi2  41414  tendo0pl  41420  tendoipl  41426  cdlemh1  41444  cdlemi2  41448  tendo0mul  41455  tendo0mulr  41456  cdlemk2  41461  cdlemk3  41462  cdlemk4  41463  cdlemk6  41466  cdlemk8  41467  cdlemk12  41479  cdlemkole  41482  cdlemk14  41483  cdlemk15  41484  cdlemk5u  41490  cdlemk6u  41491  cdlemk12u  41501  cdlemkfid1N  41550  cdlemk19x  41572  cdlemk48  41579  cdlemk53a  41584  cdlemk56  41600  cdleml2N  41606  cdleml3N  41607  cdleml6  41610  cdleml7  41611  dva1dim  41614  dia2dimlem4  41696  dvhlveclem  41737  doca2N  41755  djajN  41766  cdlemn2a  41825  cdlemn3  41826  dihordlem6  41842  dihord5apre  41891  dihglbcpreN  41929  dihmeetcN  41931  dihmeetbN  41932  dihmeetlem10N  41945  dihmeetlem12N  41947  dihmeetlem15N  41950  dihmeetALTN  41956  dih1dimatlem0  41957  dihjatcclem3  42049  dihjatcclem4  42050  mapdpglem22  42322  hdmap14lem1a  42495  eldioph2b  43349  jm2.19lem4  43574  jm2.19  43575  jm2.26a  43582  jm2.26  43584  hbtlem2  43706  fnchoice  45614  stoweidlem42  46621  stoweidlem59  46638  fourierdlem42  46728  zplusmodne  47948  minusmod5ne  47954