Theorem syl121anc 1374

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

Syntax hints:   → wi 4   ∧ wa 396   ∧ 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 206  df-an 397  df-3an 1088

This theorem is referenced by:  syl122anc  1378  fsnunf2  7067  tfisi  7714  fnsuppeq0  8017  ttrclss  9487  ttrclselem2  9493  axdc4lem  10220  div32d  11783  div13d  11784  expdivd  13887  swrdsbslen  14386  sumeven  16105  sumodd  16106  pcqmul  16563  pcid  16583  pcneg  16584  pc2dvds  16589  pcz  16591  pcaddlem  16598  pcadd  16599  pcmpt2  16603  pcbc  16610  qexpz  16611  expnprm  16612  sylow1lem1  19212  lspsneleq  20386  lspsneq  20393  lspfixed  20399  frlmsslss2  20991  chmatval  21987  chpmat1dlem  21993  chpdmatlem2  21997  ucncn  23446  ucnextcn  23465  ssblex  23590  prdsxmslem2  23694  ncvs1  24330  voliunlem1  24723  deg1mul3le  25290  deg1pw  25294  fta1blem  25342  bcmono  26434  dchrisum0flblem1  26665  dchrisum0flblem2  26666  pntibndlem1  26746  pntlemr  26759  finsumvtxdg2sstep  27925  umgr3cyclex  28556  nv1  29046  resf1o  31074  omndmul3  31348  symgcntz  31363  cycpmco2lem6  31407  tocyccntz  31420  rngurd  31491  measun  32188  measvuni  32191  measunl  32193  nosupbnd1  33926  noinfbnd1  33941  noetalem1  33953  slerec  34022  btwnconn1lem14  34411  segcon2  34416  seglelin  34427  neibastop3  34560  upixp  35896  fdc  35912  eqlkr3  37122  lkrshp  37126  lfl1dim  37142  lfl1dim2N  37143  eqlkr4  37186  2llnneN  37430  3dim2  37489  4atlem3  37617  4atlem11  37630  4atlem12  37633  pexmidlem4N  37994  lhp2at0nle  38056  lhple  38063  ltrnideq  38196  cdlemd9  38227  cdleme0ex2N  38245  cdleme0moN  38246  cdleme11a  38281  cdleme30a  38399  cdlemefs32sn1aw  38435  cdleme43fsv1snlem  38441  cdlemefs31fv1  38445  cdlemefs45eN  38452  cdleme41sn3a  38454  cdleme35h  38477  cdleme36a  38481  cdleme40m  38488  cdleme40n  38489  cdleme41sn3aw  38495  cdleme42h  38503  cdleme42k  38505  cdleme42mN  38508  cdleme43cN  38512  cdleme17d3  38517  cdleme48fvg  38521  cdlemeg47rv2  38531  cdlemeg46c  38534  cdlemeg46sfg  38541  cdlemeg46rjgN  38543  cdlemeg46rgv  38549  cdlemeg46req  38550  cdlemeg46gfv  38551  cdlemeg46gfre  38553  cdlemeg49lebilem  38560  cdleme50trn2  38572  cdlemg2kq  38623  cdlemb3  38627  cdlemg4f  38636  cdlemg9a  38653  cdlemg9b  38654  cdlemg9  38655  cdlemg11aq  38659  cdlemg12a  38664  cdlemg12b  38665  cdlemg12c  38666  cdlemg12d  38667  cdlemg12f  38669  cdlemg12g  38670  cdlemg12  38671  cdlemg13a  38672  cdlemg16  38678  cdlemg17e  38686  cdlemg17f  38687  cdlemg17g  38688  cdlemg17ir  38691  cdlemg17  38698  cdlemg18b  38700  cdlemg18c  38701  cdlemg33e  38731  trlcoabs2N  38743  trlcocnvat  38745  trlcolem  38747  trlco  38748  cdlemg44  38754  cdlemg47  38757  ltrncom  38759  tendococl  38793  tendoplcl  38802  tendoplcom  38803  tendoplass  38804  tendodi1  38805  tendodi2  38806  tendo0pl  38812  tendoipl  38818  cdlemh1  38836  cdlemi2  38840  tendo0mul  38847  tendo0mulr  38848  cdlemk2  38853  cdlemk3  38854  cdlemk4  38855  cdlemk6  38858  cdlemk8  38859  cdlemk12  38871  cdlemkole  38874  cdlemk14  38875  cdlemk15  38876  cdlemk5u  38882  cdlemk6u  38883  cdlemk12u  38893  cdlemkfid1N  38942  cdlemk19x  38964  cdlemk48  38971  cdlemk53a  38976  cdlemk56  38992  cdleml2N  38998  cdleml3N  38999  cdleml6  39002  cdleml7  39003  dva1dim  39006  dia2dimlem4  39088  dvhlveclem  39129  doca2N  39147  djajN  39158  cdlemn2a  39217  cdlemn3  39218  dihordlem6  39234  dihord5apre  39283  dihglbcpreN  39321  dihmeetcN  39323  dihmeetbN  39324  dihmeetlem10N  39337  dihmeetlem12N  39339  dihmeetlem15N  39342  dihmeetALTN  39348  dih1dimatlem0  39349  dihjatcclem3  39441  dihjatcclem4  39442  mapdpglem22  39714  hdmap14lem1a  39887  eldioph2b  40592  jm2.19lem4  40821  jm2.19  40822  jm2.26a  40829  jm2.26  40831  hbtlem2  40956  fnchoice  42579  stoweidlem42  43590  stoweidlem59  43607  fourierdlem42  43697