Theorem syl121anc 1372

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

Syntax hints:   → wi 4   ∧ wa 399   ∧ w3a 1084

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 400  df-3an 1086

This theorem is referenced by:  syl122anc  1376  fsnunf2  6925  tfisi  7553  fnsuppeq0  7841  axdc4lem  9866  div32d  11428  div13d  11429  expdivd  13520  swrdsbslen  14017  sumeven  15728  sumodd  15729  pcqmul  16180  pcid  16199  pcneg  16200  pc2dvds  16205  pcz  16207  pcaddlem  16214  pcadd  16215  pcmpt2  16219  pcbc  16226  qexpz  16227  expnprm  16228  sylow1lem1  18715  lspsneleq  19880  lspsneq  19887  lspfixed  19893  frlmsslss2  20464  chmatval  21434  chpmat1dlem  21440  chpdmatlem2  21444  ucncn  22891  ucnextcn  22910  ssblex  23035  prdsxmslem2  23136  ncvs1  23762  voliunlem1  24154  deg1mul3le  24717  deg1pw  24721  fta1blem  24769  bcmono  25861  dchrisum0flblem1  26092  dchrisum0flblem2  26093  pntibndlem1  26173  pntlemr  26186  finsumvtxdg2sstep  27339  umgr3cyclex  27968  nv1  28458  resf1o  30492  omndmul3  30764  symgcntz  30779  cycpmco2lem6  30823  tocyccntz  30836  rngurd  30907  measun  31580  measvuni  31583  measunl  31585  nosupbnd1  33327  slerec  33390  btwnconn1lem14  33674  segcon2  33679  seglelin  33690  neibastop3  33823  upixp  35167  fdc  35183  eqlkr3  36397  lkrshp  36401  lfl1dim  36417  lfl1dim2N  36418  eqlkr4  36461  2llnneN  36705  3dim2  36764  4atlem3  36892  4atlem11  36905  4atlem12  36908  pexmidlem4N  37269  lhp2at0nle  37331  lhple  37338  ltrnideq  37471  cdlemd9  37502  cdleme0ex2N  37520  cdleme0moN  37521  cdleme11a  37556  cdleme30a  37674  cdlemefs32sn1aw  37710  cdleme43fsv1snlem  37716  cdlemefs31fv1  37720  cdlemefs45eN  37727  cdleme41sn3a  37729  cdleme35h  37752  cdleme36a  37756  cdleme40m  37763  cdleme40n  37764  cdleme41sn3aw  37770  cdleme42h  37778  cdleme42k  37780  cdleme42mN  37783  cdleme43cN  37787  cdleme17d3  37792  cdleme48fvg  37796  cdlemeg47rv2  37806  cdlemeg46c  37809  cdlemeg46sfg  37816  cdlemeg46rjgN  37818  cdlemeg46rgv  37824  cdlemeg46req  37825  cdlemeg46gfv  37826  cdlemeg46gfre  37828  cdlemeg49lebilem  37835  cdleme50trn2  37847  cdlemg2kq  37898  cdlemb3  37902  cdlemg4f  37911  cdlemg9a  37928  cdlemg9b  37929  cdlemg9  37930  cdlemg11aq  37934  cdlemg12a  37939  cdlemg12b  37940  cdlemg12c  37941  cdlemg12d  37942  cdlemg12f  37944  cdlemg12g  37945  cdlemg12  37946  cdlemg13a  37947  cdlemg16  37953  cdlemg17e  37961  cdlemg17f  37962  cdlemg17g  37963  cdlemg17ir  37966  cdlemg17  37973  cdlemg18b  37975  cdlemg18c  37976  cdlemg33e  38006  trlcoabs2N  38018  trlcocnvat  38020  trlcolem  38022  trlco  38023  cdlemg44  38029  cdlemg47  38032  ltrncom  38034  tendococl  38068  tendoplcl  38077  tendoplcom  38078  tendoplass  38079  tendodi1  38080  tendodi2  38081  tendo0pl  38087  tendoipl  38093  cdlemh1  38111  cdlemi2  38115  tendo0mul  38122  tendo0mulr  38123  cdlemk2  38128  cdlemk3  38129  cdlemk4  38130  cdlemk6  38133  cdlemk8  38134  cdlemk12  38146  cdlemkole  38149  cdlemk14  38150  cdlemk15  38151  cdlemk5u  38157  cdlemk6u  38158  cdlemk12u  38168  cdlemkfid1N  38217  cdlemk19x  38239  cdlemk48  38246  cdlemk53a  38251  cdlemk56  38267  cdleml2N  38273  cdleml3N  38274  cdleml6  38277  cdleml7  38278  dva1dim  38281  dia2dimlem4  38363  dvhlveclem  38404  doca2N  38422  djajN  38433  cdlemn2a  38492  cdlemn3  38493  dihordlem6  38509  dihord5apre  38558  dihglbcpreN  38596  dihmeetcN  38598  dihmeetbN  38599  dihmeetlem10N  38612  dihmeetlem12N  38614  dihmeetlem15N  38617  dihmeetALTN  38623  dih1dimatlem0  38624  dihjatcclem3  38716  dihjatcclem4  38717  mapdpglem22  38989  hdmap14lem1a  39162  eldioph2b  39704  jm2.19lem4  39933  jm2.19  39934  jm2.26a  39941  jm2.26  39943  hbtlem2  40068  fnchoice  41658  stoweidlem42  42684  stoweidlem59  42701  fourierdlem42  42791