Theorem syl121anc 1377

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

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1086

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 207  df-an 396  df-3an 1088

This theorem is referenced by:  syl122anc  1381  fsnunf2  7177  tfisi  7852  fnsuppeq0  8189  ttrclss  9732  ttrclselem2  9738  axdc4lem  10467  div32d  12038  div13d  12039  expdivd  14176  swrdsbslen  14680  sumeven  16404  sumodd  16405  pcqmul  16871  pcid  16891  pcneg  16892  pc2dvds  16897  pcz  16899  pcaddlem  16906  pcadd  16907  pcmpt2  16911  pcbc  16918  qexpz  16919  expnprm  16920  sylow1lem1  19577  ringurd  20143  lspsneleq  21074  lspsneq  21081  lspfixed  21087  frlmsslss2  21733  chmatval  22765  chpmat1dlem  22771  chpdmatlem2  22775  ucncn  24221  ucnextcn  24240  ssblex  24365  prdsxmslem2  24466  ncvs1  25107  voliunlem1  25501  deg1mul3le  26072  deg1pw  26076  fta1blem  26126  bcmono  27238  dchrisum0flblem1  27469  dchrisum0flblem2  27470  pntibndlem1  27550  pntlemr  27563  nosupbnd1  27676  noinfbnd1  27691  noetalem1  27703  slerec  27781  finsumvtxdg2sstep  29475  umgr3cyclex  30110  nv1  30602  resf1o  32653  omndmul3  33027  symgcntz  33042  cycpmco2lem6  33088  tocyccntz  33101  deg1vr  33548  rtelextdg2lem  33706  measun  34188  measvuni  34191  measunl  34193  btwnconn1lem14  36064  segcon2  36069  seglelin  36080  neibastop3  36326  upixp  37699  fdc  37715  eqlkr3  39065  lkrshp  39069  lfl1dim  39085  lfl1dim2N  39086  eqlkr4  39129  2llnneN  39374  3dim2  39433  4atlem3  39561  4atlem11  39574  4atlem12  39577  pexmidlem4N  39938  lhp2at0nle  40000  lhple  40007  ltrnideq  40140  cdlemd9  40171  cdleme0ex2N  40189  cdleme0moN  40190  cdleme11a  40225  cdleme30a  40343  cdlemefs32sn1aw  40379  cdleme43fsv1snlem  40385  cdlemefs31fv1  40389  cdlemefs45eN  40396  cdleme41sn3a  40398  cdleme35h  40421  cdleme36a  40425  cdleme40m  40432  cdleme40n  40433  cdleme41sn3aw  40439  cdleme42h  40447  cdleme42k  40449  cdleme42mN  40452  cdleme43cN  40456  cdleme17d3  40461  cdleme48fvg  40465  cdlemeg47rv2  40475  cdlemeg46c  40478  cdlemeg46sfg  40485  cdlemeg46rjgN  40487  cdlemeg46rgv  40493  cdlemeg46req  40494  cdlemeg46gfv  40495  cdlemeg46gfre  40497  cdlemeg49lebilem  40504  cdleme50trn2  40516  cdlemg2kq  40567  cdlemb3  40571  cdlemg4f  40580  cdlemg9a  40597  cdlemg9b  40598  cdlemg9  40599  cdlemg11aq  40603  cdlemg12a  40608  cdlemg12b  40609  cdlemg12c  40610  cdlemg12d  40611  cdlemg12f  40613  cdlemg12g  40614  cdlemg12  40615  cdlemg13a  40616  cdlemg16  40622  cdlemg17e  40630  cdlemg17f  40631  cdlemg17g  40632  cdlemg17ir  40635  cdlemg17  40642  cdlemg18b  40644  cdlemg18c  40645  cdlemg33e  40675  trlcoabs2N  40687  trlcocnvat  40689  trlcolem  40691  trlco  40692  cdlemg44  40698  cdlemg47  40701  ltrncom  40703  tendococl  40737  tendoplcl  40746  tendoplcom  40747  tendoplass  40748  tendodi1  40749  tendodi2  40750  tendo0pl  40756  tendoipl  40762  cdlemh1  40780  cdlemi2  40784  tendo0mul  40791  tendo0mulr  40792  cdlemk2  40797  cdlemk3  40798  cdlemk4  40799  cdlemk6  40802  cdlemk8  40803  cdlemk12  40815  cdlemkole  40818  cdlemk14  40819  cdlemk15  40820  cdlemk5u  40826  cdlemk6u  40827  cdlemk12u  40837  cdlemkfid1N  40886  cdlemk19x  40908  cdlemk48  40915  cdlemk53a  40920  cdlemk56  40936  cdleml2N  40942  cdleml3N  40943  cdleml6  40946  cdleml7  40947  dva1dim  40950  dia2dimlem4  41032  dvhlveclem  41073  doca2N  41091  djajN  41102  cdlemn2a  41161  cdlemn3  41162  dihordlem6  41178  dihord5apre  41227  dihglbcpreN  41265  dihmeetcN  41267  dihmeetbN  41268  dihmeetlem10N  41281  dihmeetlem12N  41283  dihmeetlem15N  41286  dihmeetALTN  41292  dih1dimatlem0  41293  dihjatcclem3  41385  dihjatcclem4  41386  mapdpglem22  41658  hdmap14lem1a  41831  eldioph2b  42733  jm2.19lem4  42963  jm2.19  42964  jm2.26a  42971  jm2.26  42973  hbtlem2  43095  fnchoice  45001  stoweidlem42  46019  stoweidlem59  46036  fourierdlem42  46126  zplusmodne  47320  minusmod5ne  47326