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  7187  tfisi  7858  fnsuppeq0  8193  ttrclss  9702  ttrclselem2  9708  axdc4lem  10460  div32d  12041  div13d  12042  expdivd  14226  swrdsbslen  14736  sumeven  16481  sumodd  16482  pcqmul  16949  pcid  16969  pcneg  16970  pc2dvds  16975  pcz  16977  pcaddlem  16984  pcadd  16985  pcmpt2  16989  pcbc  16996  qexpz  16997  expnprm  16998  sylow1lem1  19726  omndmul3  20262  ringurd  20325  lspsneleq  21303  lspsneq  21310  lspfixed  21316  frlmsslss2  21989  chmatval  23055  chpmat1dlem  23061  chpdmatlem2  23065  ucncn  24511  ucnextcn  24530  ssblex  24655  prdsxmslem2  24756  ncvs1  25386  voliunlem1  25779  deg1mul3le  26344  deg1pw  26348  fta1blem  26398  bcmono  27511  dchrisum0flblem1  27742  dchrisum0flblem2  27743  pntibndlem1  27823  pntlemr  27836  nosupbnd1  27948  noinfbnd1  27963  noetalem1  27975  lesrec  28062  finsumvtxdg2sstep  29995  umgr3cyclex  30649  nv1  31142  resf1o  33188  symgcntz  33512  cycpmco2lem6  33558  tocyccntz  33571  deg1vr  33989  rtelextdg2lem  34223  measun  34709  measvuni  34712  measunl  34714  btwnconn1lem14  36667  segcon2  36672  seglelin  36683  neibastop3  36968  upixp  38466  fdc  38482  eqlkr3  39961  lkrshp  39965  lfl1dim  39981  lfl1dim2N  39982  eqlkr4  40025  2llnneN  40269  3dim2  40328  4atlem3  40456  4atlem11  40469  4atlem12  40472  pexmidlem4N  40833  lhp2at0nle  40895  lhple  40902  ltrnideq  41035  cdlemd9  41066  cdleme0ex2N  41084  cdleme0moN  41085  cdleme11a  41120  cdleme30a  41238  cdlemefs32sn1aw  41274  cdleme43fsv1snlem  41280  cdlemefs31fv1  41284  cdlemefs45eN  41291  cdleme41sn3a  41293  cdleme35h  41316  cdleme36a  41320  cdleme40m  41327  cdleme40n  41328  cdleme41sn3aw  41334  cdleme42h  41342  cdleme42k  41344  cdleme42mN  41347  cdleme43cN  41351  cdleme17d3  41356  cdleme48fvg  41360  cdlemeg47rv2  41370  cdlemeg46c  41373  cdlemeg46sfg  41380  cdlemeg46rjgN  41382  cdlemeg46rgv  41388  cdlemeg46req  41389  cdlemeg46gfv  41390  cdlemeg46gfre  41392  cdlemeg49lebilem  41399  cdleme50trn2  41411  cdlemg2kq  41462  cdlemb3  41466  cdlemg4f  41475  cdlemg9a  41492  cdlemg9b  41493  cdlemg9  41494  cdlemg11aq  41498  cdlemg12a  41503  cdlemg12b  41504  cdlemg12c  41505  cdlemg12d  41506  cdlemg12f  41508  cdlemg12g  41509  cdlemg12  41510  cdlemg13a  41511  cdlemg16  41517  cdlemg17e  41525  cdlemg17f  41526  cdlemg17g  41527  cdlemg17ir  41530  cdlemg17  41537  cdlemg18b  41539  cdlemg18c  41540  cdlemg33e  41570  trlcoabs2N  41582  trlcocnvat  41584  trlcolem  41586  trlco  41587  cdlemg44  41593  cdlemg47  41596  ltrncom  41598  tendococl  41632  tendoplcl  41641  tendoplcom  41642  tendoplass  41643  tendodi1  41644  tendodi2  41645  tendo0pl  41651  tendoipl  41657  cdlemh1  41675  cdlemi2  41679  tendo0mul  41686  tendo0mulr  41687  cdlemk2  41692  cdlemk3  41693  cdlemk4  41694  cdlemk6  41697  cdlemk8  41698  cdlemk12  41710  cdlemkole  41713  cdlemk14  41714  cdlemk15  41715  cdlemk5u  41721  cdlemk6u  41722  cdlemk12u  41732  cdlemkfid1N  41781  cdlemk19x  41803  cdlemk48  41810  cdlemk53a  41815  cdlemk56  41831  cdleml2N  41837  cdleml3N  41838  cdleml6  41841  cdleml7  41842  dva1dim  41845  dia2dimlem4  41927  dvhlveclem  41968  doca2N  41986  djajN  41997  cdlemn2a  42056  cdlemn3  42057  dihordlem6  42073  dihord5apre  42122  dihglbcpreN  42160  dihmeetcN  42162  dihmeetbN  42163  dihmeetlem10N  42176  dihmeetlem12N  42178  dihmeetlem15N  42181  dihmeetALTN  42187  dih1dimatlem0  42188  dihjatcclem3  42280  dihjatcclem4  42281  mapdpglem22  42553  hdmap14lem1a  42726  eldioph2b  43595  jm2.19lem4  43820  jm2.19  43821  jm2.26a  43828  jm2.26  43830  hbtlem2  43952  fnchoice  45850  stoweidlem42  46857  stoweidlem59  46874  fourierdlem42  46964  zplusmodne  48224  minusmod5ne  48230