Theorem syl121anc 1400

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 1396	1 ⊢ (𝜑 → 𝜂)

Syntax hints:   → wi 4   ∧ wa 400   ∧ w3a 1101

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

This theorem is referenced by:  syl122anc  1404  fsnunf2  7184  tfisi  7854  fnsuppeq0  8187  ttrclss  9688  ttrclselem2  9694  axdc4lem  10438  div32d  12013  div13d  12014  expdivd  14195  swrdsbslen  14701  sumeven  16444  sumodd  16445  pcqmul  16912  pcid  16932  pcneg  16933  pc2dvds  16938  pcz  16940  pcaddlem  16947  pcadd  16948  pcmpt2  16952  pcbc  16959  qexpz  16960  expnprm  16961  sylow1lem1  19667  omndmul3  20203  ringurd  20266  lspsneleq  21218  lspsneq  21225  lspfixed  21231  frlmsslss2  21904  chmatval  22965  chpmat1dlem  22971  chpdmatlem2  22975  ucncn  24420  ucnextcn  24439  ssblex  24564  prdsxmslem2  24665  ncvs1  25295  voliunlem1  25688  deg1mul3le  26253  deg1pw  26257  fta1blem  26307  bcmono  27417  dchrisum0flblem1  27648  dchrisum0flblem2  27649  pntibndlem1  27729  pntlemr  27742  nosupbnd1  27854  noinfbnd1  27869  noetalem1  27881  lesrec  27968  finsumvtxdg2sstep  29865  umgr3cyclex  30500  nv1  30993  resf1o  33041  symgcntz  33371  cycpmco2lem6  33417  tocyccntz  33430  deg1vr  33848  rtelextdg2lem  34082  measun  34567  measvuni  34570  measunl  34572  btwnconn1lem14  36546  segcon2  36551  seglelin  36562  neibastop3  36817  upixp  38324  fdc  38340  eqlkr3  39821  lkrshp  39825  lfl1dim  39841  lfl1dim2N  39842  eqlkr4  39885  2llnneN  40129  3dim2  40188  4atlem3  40316  4atlem11  40329  4atlem12  40332  pexmidlem4N  40693  lhp2at0nle  40755  lhple  40762  ltrnideq  40895  cdlemd9  40926  cdleme0ex2N  40944  cdleme0moN  40945  cdleme11a  40980  cdleme30a  41098  cdlemefs32sn1aw  41134  cdleme43fsv1snlem  41140  cdlemefs31fv1  41144  cdlemefs45eN  41151  cdleme41sn3a  41153  cdleme35h  41176  cdleme36a  41180  cdleme40m  41187  cdleme40n  41188  cdleme41sn3aw  41194  cdleme42h  41202  cdleme42k  41204  cdleme42mN  41207  cdleme43cN  41211  cdleme17d3  41216  cdleme48fvg  41220  cdlemeg47rv2  41230  cdlemeg46c  41233  cdlemeg46sfg  41240  cdlemeg46rjgN  41242  cdlemeg46rgv  41248  cdlemeg46req  41249  cdlemeg46gfv  41250  cdlemeg46gfre  41252  cdlemeg49lebilem  41259  cdleme50trn2  41271  cdlemg2kq  41322  cdlemb3  41326  cdlemg4f  41335  cdlemg9a  41352  cdlemg9b  41353  cdlemg9  41354  cdlemg11aq  41358  cdlemg12a  41363  cdlemg12b  41364  cdlemg12c  41365  cdlemg12d  41366  cdlemg12f  41368  cdlemg12g  41369  cdlemg12  41370  cdlemg13a  41371  cdlemg16  41377  cdlemg17e  41385  cdlemg17f  41386  cdlemg17g  41387  cdlemg17ir  41390  cdlemg17  41397  cdlemg18b  41399  cdlemg18c  41400  cdlemg33e  41430  trlcoabs2N  41442  trlcocnvat  41444  trlcolem  41446  trlco  41447  cdlemg44  41453  cdlemg47  41456  ltrncom  41458  tendococl  41492  tendoplcl  41501  tendoplcom  41502  tendoplass  41503  tendodi1  41504  tendodi2  41505  tendo0pl  41511  tendoipl  41517  cdlemh1  41535  cdlemi2  41539  tendo0mul  41546  tendo0mulr  41547  cdlemk2  41552  cdlemk3  41553  cdlemk4  41554  cdlemk6  41557  cdlemk8  41558  cdlemk12  41570  cdlemkole  41573  cdlemk14  41574  cdlemk15  41575  cdlemk5u  41581  cdlemk6u  41582  cdlemk12u  41592  cdlemkfid1N  41641  cdlemk19x  41663  cdlemk48  41670  cdlemk53a  41675  cdlemk56  41691  cdleml2N  41697  cdleml3N  41698  cdleml6  41701  cdleml7  41702  dva1dim  41705  dia2dimlem4  41787  dvhlveclem  41828  doca2N  41846  djajN  41857  cdlemn2a  41916  cdlemn3  41917  dihordlem6  41933  dihord5apre  41982  dihglbcpreN  42020  dihmeetcN  42022  dihmeetbN  42023  dihmeetlem10N  42036  dihmeetlem12N  42038  dihmeetlem15N  42041  dihmeetALTN  42047  dih1dimatlem0  42048  dihjatcclem3  42140  dihjatcclem4  42141  mapdpglem22  42413  hdmap14lem1a  42586  eldioph2b  43442  jm2.19lem4  43667  jm2.19  43668  jm2.26a  43675  jm2.26  43677  hbtlem2  43799  fnchoice  45697  stoweidlem42  46704  stoweidlem59  46721  fourierdlem42  46811  zplusmodne  48031  minusmod5ne  48037