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  7191  tfisi  7870  fnsuppeq0  8209  ttrclss  9721  ttrclselem2  9727  axdc4lem  10533  div32d  12116  div13d  12117  expdivd  14303  swrdsbslen  14814  sumeven  16557  sumodd  16558  pcqmul  17031  pcid  17051  pcneg  17052  pc2dvds  17057  pcz  17059  pcaddlem  17066  pcadd  17067  pcmpt2  17071  pcbc  17078  qexpz  17079  expnprm  17080  sylow1lem1  19812  omndmul3  20348  ringurd  20411  lspsneleq  21393  lspsneq  21400  lspfixed  21406  frlmsslss2  22081  chmatval  23147  chpmat1dlem  23153  chpdmatlem2  23157  ucncn  24603  ucnextcn  24622  ssblex  24747  prdsxmslem2  24848  ncvs1  25478  voliunlem1  25871  deg1mul3le  26435  deg1pw  26439  fta1blem  26489  bcmono  27604  dchrisum0flblem1  27835  dchrisum0flblem2  27836  pntibndlem1  27916  pntlemr  27929  nosupbnd1  28071  noinfbnd1  28086  noetalem1  28098  lesrec  28185  finsumvtxdg2sstep  30130  umgr3cyclex  30784  nv1  31277  resf1o  33322  symgcntz  33646  cycpmco2lem6  33692  tocyccntz  33705  deg1vr  34124  rtelextdg2lem  34358  measun  34844  measvuni  34847  measunl  34849  btwnconn1lem14  36865  segcon2  36870  seglelin  36881  neibastop3  37150  upixp  38664  fdc  38680  eqlkr3  40159  lkrshp  40163  lfl1dim  40179  lfl1dim2N  40180  eqlkr4  40223  2llnneN  40467  3dim2  40526  4atlem3  40654  4atlem11  40667  4atlem12  40670  pexmidlem4N  41031  lhp2at0nle  41093  lhple  41100  ltrnideq  41233  cdlemd9  41264  cdleme0ex2N  41282  cdleme0moN  41283  cdleme11a  41318  cdleme30a  41436  cdlemefs32sn1aw  41472  cdleme43fsv1snlem  41478  cdlemefs31fv1  41482  cdlemefs45eN  41489  cdleme41sn3a  41491  cdleme35h  41514  cdleme36a  41518  cdleme40m  41525  cdleme40n  41526  cdleme41sn3aw  41532  cdleme42h  41540  cdleme42k  41542  cdleme42mN  41545  cdleme43cN  41549  cdleme17d3  41554  cdleme48fvg  41558  cdlemeg47rv2  41568  cdlemeg46c  41571  cdlemeg46sfg  41578  cdlemeg46rjgN  41580  cdlemeg46rgv  41586  cdlemeg46req  41587  cdlemeg46gfv  41588  cdlemeg46gfre  41590  cdlemeg49lebilem  41597  cdleme50trn2  41609  cdlemg2kq  41660  cdlemb3  41664  cdlemg4f  41673  cdlemg9a  41690  cdlemg9b  41691  cdlemg9  41692  cdlemg11aq  41696  cdlemg12a  41701  cdlemg12b  41702  cdlemg12c  41703  cdlemg12d  41704  cdlemg12f  41706  cdlemg12g  41707  cdlemg12  41708  cdlemg13a  41709  cdlemg16  41715  cdlemg17e  41723  cdlemg17f  41724  cdlemg17g  41725  cdlemg17ir  41728  cdlemg17  41735  cdlemg18b  41737  cdlemg18c  41738  cdlemg33e  41768  trlcoabs2N  41780  trlcocnvat  41782  trlcolem  41784  trlco  41785  cdlemg44  41791  cdlemg47  41794  ltrncom  41796  tendococl  41830  tendoplcl  41839  tendoplcom  41840  tendoplass  41841  tendodi1  41842  tendodi2  41843  tendo0pl  41849  tendoipl  41855  cdlemh1  41873  cdlemi2  41877  tendo0mul  41884  tendo0mulr  41885  cdlemk2  41890  cdlemk3  41891  cdlemk4  41892  cdlemk6  41895  cdlemk8  41896  cdlemk12  41908  cdlemkole  41911  cdlemk14  41912  cdlemk15  41913  cdlemk5u  41919  cdlemk6u  41920  cdlemk12u  41930  cdlemkfid1N  41979  cdlemk19x  42001  cdlemk48  42008  cdlemk53a  42013  cdlemk56  42029  cdleml2N  42035  cdleml3N  42036  cdleml6  42039  cdleml7  42040  dva1dim  42043  dia2dimlem4  42125  dvhlveclem  42166  doca2N  42184  djajN  42195  cdlemn2a  42254  cdlemn3  42255  dihordlem6  42271  dihord5apre  42320  dihglbcpreN  42358  dihmeetcN  42360  dihmeetbN  42361  dihmeetlem10N  42374  dihmeetlem12N  42376  dihmeetlem15N  42379  dihmeetALTN  42385  dih1dimatlem0  42386  dihjatcclem3  42478  dihjatcclem4  42479  mapdpglem22  42751  hdmap14lem1a  42924  eldioph2b  43774  jm2.19lem4  43999  jm2.19  44000  jm2.26a  44007  jm2.26  44009  hbtlem2  44126  fnchoice  46046  stoweidlem42  47052  stoweidlem59  47069  fourierdlem42  47159  zplusmodne  48419  minusmod5ne  48425