Theorem syl121anc 1402

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  syl122anc  1406  fsnunf2  7180  tfisi  7854  fnsuppeq0  8188  ttrclss  9699  ttrclselem2  9705  axdc4lem  10490  div32d  12071  div13d  12072  expdivd  14257  swrdsbslen  14767  sumeven  16510  sumodd  16511  pcqmul  16978  pcid  16998  pcneg  16999  pc2dvds  17004  pcz  17006  pcaddlem  17013  pcadd  17014  pcmpt2  17018  pcbc  17025  qexpz  17026  expnprm  17027  sylow1lem1  19759  omndmul3  20295  ringurd  20358  lspsneleq  21340  lspsneq  21347  lspfixed  21353  frlmsslss2  22028  chmatval  23094  chpmat1dlem  23100  chpdmatlem2  23104  ucncn  24550  ucnextcn  24569  ssblex  24694  prdsxmslem2  24795  ncvs1  25425  voliunlem1  25818  deg1mul3le  26382  deg1pw  26386  fta1blem  26436  bcmono  27553  dchrisum0flblem1  27784  dchrisum0flblem2  27785  pntibndlem1  27865  pntlemr  27878  nosupbnd1  27990  noinfbnd1  28005  noetalem1  28017  lesrec  28104  finsumvtxdg2sstep  30049  umgr3cyclex  30703  nv1  31196  resf1o  33241  symgcntz  33565  cycpmco2lem6  33611  tocyccntz  33624  deg1vr  34043  rtelextdg2lem  34277  measun  34763  measvuni  34766  measunl  34768  btwnconn1lem14  36781  segcon2  36786  seglelin  36797  neibastop3  37066  upixp  38577  fdc  38593  eqlkr3  40072  lkrshp  40076  lfl1dim  40092  lfl1dim2N  40093  eqlkr4  40136  2llnneN  40380  3dim2  40439  4atlem3  40567  4atlem11  40580  4atlem12  40583  pexmidlem4N  40944  lhp2at0nle  41006  lhple  41013  ltrnideq  41146  cdlemd9  41177  cdleme0ex2N  41195  cdleme0moN  41196  cdleme11a  41231  cdleme30a  41349  cdlemefs32sn1aw  41385  cdleme43fsv1snlem  41391  cdlemefs31fv1  41395  cdlemefs45eN  41402  cdleme41sn3a  41404  cdleme35h  41427  cdleme36a  41431  cdleme40m  41438  cdleme40n  41439  cdleme41sn3aw  41445  cdleme42h  41453  cdleme42k  41455  cdleme42mN  41458  cdleme43cN  41462  cdleme17d3  41467  cdleme48fvg  41471  cdlemeg47rv2  41481  cdlemeg46c  41484  cdlemeg46sfg  41491  cdlemeg46rjgN  41493  cdlemeg46rgv  41499  cdlemeg46req  41500  cdlemeg46gfv  41501  cdlemeg46gfre  41503  cdlemeg49lebilem  41510  cdleme50trn2  41522  cdlemg2kq  41573  cdlemb3  41577  cdlemg4f  41586  cdlemg9a  41603  cdlemg9b  41604  cdlemg9  41605  cdlemg11aq  41609  cdlemg12a  41614  cdlemg12b  41615  cdlemg12c  41616  cdlemg12d  41617  cdlemg12f  41619  cdlemg12g  41620  cdlemg12  41621  cdlemg13a  41622  cdlemg16  41628  cdlemg17e  41636  cdlemg17f  41637  cdlemg17g  41638  cdlemg17ir  41641  cdlemg17  41648  cdlemg18b  41650  cdlemg18c  41651  cdlemg33e  41681  trlcoabs2N  41693  trlcocnvat  41695  trlcolem  41697  trlco  41698  cdlemg44  41704  cdlemg47  41707  ltrncom  41709  tendococl  41743  tendoplcl  41752  tendoplcom  41753  tendoplass  41754  tendodi1  41755  tendodi2  41756  tendo0pl  41762  tendoipl  41768  cdlemh1  41786  cdlemi2  41790  tendo0mul  41797  tendo0mulr  41798  cdlemk2  41803  cdlemk3  41804  cdlemk4  41805  cdlemk6  41808  cdlemk8  41809  cdlemk12  41821  cdlemkole  41824  cdlemk14  41825  cdlemk15  41826  cdlemk5u  41832  cdlemk6u  41833  cdlemk12u  41843  cdlemkfid1N  41892  cdlemk19x  41914  cdlemk48  41921  cdlemk53a  41926  cdlemk56  41942  cdleml2N  41948  cdleml3N  41949  cdleml6  41952  cdleml7  41953  dva1dim  41956  dia2dimlem4  42038  dvhlveclem  42079  doca2N  42097  djajN  42108  cdlemn2a  42167  cdlemn3  42168  dihordlem6  42184  dihord5apre  42233  dihglbcpreN  42271  dihmeetcN  42273  dihmeetbN  42274  dihmeetlem10N  42287  dihmeetlem12N  42289  dihmeetlem15N  42292  dihmeetALTN  42298  dih1dimatlem0  42299  dihjatcclem3  42391  dihjatcclem4  42392  mapdpglem22  42664  hdmap14lem1a  42837  eldioph2b  43706  jm2.19lem4  43931  jm2.19  43932  jm2.26a  43939  jm2.26  43941  hbtlem2  44063  fnchoice  45961  stoweidlem42  46968  stoweidlem59  46985  fourierdlem42  47075  zplusmodne  48335  minusmod5ne  48341