Theorem syl121anc 1401

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 400   ∧ w3a 1102

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 401  df-3an 1104

This theorem is used by:  syl122anc  1405  fsnunf2  7184  tfisi  7853  fnsuppeq0  8186  ttrclss  9687  ttrclselem2  9693  axdc4lem  10445  div32d  12020  div13d  12021  expdivd  14203  swrdsbslen  14709  sumeven  16451  sumodd  16452  pcqmul  16919  pcid  16939  pcneg  16940  pc2dvds  16945  pcz  16947  pcaddlem  16954  pcadd  16955  pcmpt2  16959  pcbc  16966  qexpz  16967  expnprm  16968  sylow1lem1  19674  omndmul3  20210  ringurd  20273  lspsneleq  21250  lspsneq  21257  lspfixed  21263  frlmsslss2  21936  chmatval  22997  chpmat1dlem  23003  chpdmatlem2  23007  ucncn  24452  ucnextcn  24471  ssblex  24596  prdsxmslem2  24697  ncvs1  25327  voliunlem1  25720  deg1mul3le  26285  deg1pw  26289  fta1blem  26339  bcmono  27452  dchrisum0flblem1  27683  dchrisum0flblem2  27684  pntibndlem1  27764  pntlemr  27777  nosupbnd1  27889  noinfbnd1  27904  noetalem1  27916  lesrec  28003  finsumvtxdg2sstep  29910  umgr3cyclex  30545  nv1  31038  resf1o  33086  symgcntz  33414  cycpmco2lem6  33460  tocyccntz  33473  deg1vr  33891  rtelextdg2lem  34125  measun  34610  measvuni  34613  measunl  34615  btwnconn1lem14  36600  segcon2  36605  seglelin  36616  neibastop3  36901  upixp  38408  fdc  38424  eqlkr3  39903  lkrshp  39907  lfl1dim  39923  lfl1dim2N  39924  eqlkr4  39967  2llnneN  40211  3dim2  40270  4atlem3  40398  4atlem11  40411  4atlem12  40414  pexmidlem4N  40775  lhp2at0nle  40837  lhple  40844  ltrnideq  40977  cdlemd9  41008  cdleme0ex2N  41026  cdleme0moN  41027  cdleme11a  41062  cdleme30a  41180  cdlemefs32sn1aw  41216  cdleme43fsv1snlem  41222  cdlemefs31fv1  41226  cdlemefs45eN  41233  cdleme41sn3a  41235  cdleme35h  41258  cdleme36a  41262  cdleme40m  41269  cdleme40n  41270  cdleme41sn3aw  41276  cdleme42h  41284  cdleme42k  41286  cdleme42mN  41289  cdleme43cN  41293  cdleme17d3  41298  cdleme48fvg  41302  cdlemeg47rv2  41312  cdlemeg46c  41315  cdlemeg46sfg  41322  cdlemeg46rjgN  41324  cdlemeg46rgv  41330  cdlemeg46req  41331  cdlemeg46gfv  41332  cdlemeg46gfre  41334  cdlemeg49lebilem  41341  cdleme50trn2  41353  cdlemg2kq  41404  cdlemb3  41408  cdlemg4f  41417  cdlemg9a  41434  cdlemg9b  41435  cdlemg9  41436  cdlemg11aq  41440  cdlemg12a  41445  cdlemg12b  41446  cdlemg12c  41447  cdlemg12d  41448  cdlemg12f  41450  cdlemg12g  41451  cdlemg12  41452  cdlemg13a  41453  cdlemg16  41459  cdlemg17e  41467  cdlemg17f  41468  cdlemg17g  41469  cdlemg17ir  41472  cdlemg17  41479  cdlemg18b  41481  cdlemg18c  41482  cdlemg33e  41512  trlcoabs2N  41524  trlcocnvat  41526  trlcolem  41528  trlco  41529  cdlemg44  41535  cdlemg47  41538  ltrncom  41540  tendococl  41574  tendoplcl  41583  tendoplcom  41584  tendoplass  41585  tendodi1  41586  tendodi2  41587  tendo0pl  41593  tendoipl  41599  cdlemh1  41617  cdlemi2  41621  tendo0mul  41628  tendo0mulr  41629  cdlemk2  41634  cdlemk3  41635  cdlemk4  41636  cdlemk6  41639  cdlemk8  41640  cdlemk12  41652  cdlemkole  41655  cdlemk14  41656  cdlemk15  41657  cdlemk5u  41663  cdlemk6u  41664  cdlemk12u  41674  cdlemkfid1N  41723  cdlemk19x  41745  cdlemk48  41752  cdlemk53a  41757  cdlemk56  41773  cdleml2N  41779  cdleml3N  41780  cdleml6  41783  cdleml7  41784  dva1dim  41787  dia2dimlem4  41869  dvhlveclem  41910  doca2N  41928  djajN  41939  cdlemn2a  41998  cdlemn3  41999  dihordlem6  42015  dihord5apre  42064  dihglbcpreN  42102  dihmeetcN  42104  dihmeetbN  42105  dihmeetlem10N  42118  dihmeetlem12N  42120  dihmeetlem15N  42123  dihmeetALTN  42129  dih1dimatlem0  42130  dihjatcclem3  42222  dihjatcclem4  42223  mapdpglem22  42495  hdmap14lem1a  42668  eldioph2b  43522  jm2.19lem4  43747  jm2.19  43748  jm2.26a  43755  jm2.26  43757  hbtlem2  43879  fnchoice  45777  stoweidlem42  46784  stoweidlem59  46801  fourierdlem42  46891  zplusmodne  48114  minusmod5ne  48120