Theorem syl113anc 1384

Description: Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.)

Hypotheses

Ref	Expression
syl3anc.1	⊢ (𝜑 → 𝜓)
syl3anc.2	⊢ (𝜑 → 𝜒)
syl3anc.3	⊢ (𝜑 → 𝜃)
syl3Xanc.4	⊢ (𝜑 → 𝜏)
syl23anc.5	⊢ (𝜑 → 𝜂)
syl113anc.6	⊢ ((𝜓 ∧ 𝜒 ∧ (𝜃 ∧ 𝜏 ∧ 𝜂)) → 𝜁)

Assertion

Ref	Expression
syl113anc	⊢ (𝜑 → 𝜁)

Proof of Theorem syl113anc

Step	Hyp	Ref	Expression
1		syl3anc.1	. 2 ⊢ (𝜑 → 𝜓)
2		syl3anc.2	. 2 ⊢ (𝜑 → 𝜒)
3		syl3anc.3	. . 3 ⊢ (𝜑 → 𝜃)
4		syl3Xanc.4	. . 3 ⊢ (𝜑 → 𝜏)
5		syl23anc.5	. . 3 ⊢ (𝜑 → 𝜂)
6	3, 4, 5	3jca 1128	. 2 ⊢ (𝜑 → (𝜃 ∧ 𝜏 ∧ 𝜂))
7		syl113anc.6	. 2 ⊢ ((𝜓 ∧ 𝜒 ∧ (𝜃 ∧ 𝜏 ∧ 𝜂)) → 𝜁)
8	1, 2, 6, 7	syl3anc 1373	1 ⊢ (𝜑 → 𝜁)

Syntax hints:   → wi 4   ∧ 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:  syl123anc  1389  syl213anc  1391  hash7g  14451  pythagtriplem18  16803  initoeu2  17978  psgnunilem1  19423  mulmarep1gsum1  22460  mulmarep1gsum2  22461  smadiadetlem4  22556  cramerimplem2  22571  cramerlem2  22575  cramer  22578  cnhaus  23241  dishaus  23269  ordthauslem  23270  pthaus  23525  txhaus  23534  xkohaus  23540  regr1lem  23626  methaus  24408  metnrmlem3  24750  nosupres  27619  nosupbnd1lem1  27620  nosupbnd2  27628  noinfres  27634  noinfbnd1lem1  27635  iscgrad  28738  f1otrge  28799  axpaschlem  28867  wwlksnwwlksnon  29845  n4cyclfrgr  30220  br8d  32538  lt2addrd  32674  xlt2addrd  32682  br8  35743  br4  35745  btwnxfr  36044  lineext  36064  brsegle  36096  brsegle2  36097  lfl0  39058  lfladd  39059  lflsub  39060  lflmul  39061  lflnegcl  39068  lflvscl  39070  lkrlss  39088  3dimlem3  39455  3dimlem4  39458  3dim3  39463  2llnm3N  39563  2lplnja  39613  4atex  40070  4atex3  40075  trlval4  40182  cdleme7c  40239  cdleme7d  40240  cdleme7ga  40242  cdleme21h  40328  cdleme21i  40329  cdleme21j  40330  cdleme21  40331  cdleme32d  40438  cdleme32f  40440  cdleme35h2  40451  cdleme38m  40457  cdleme40m  40461  cdlemg8  40625  cdlemg11a  40631  cdlemg10a  40634  cdlemg12b  40638  cdlemg12d  40640  cdlemg12f  40642  cdlemg12g  40643  cdlemg15a  40649  cdlemg16  40651  cdlemg16z  40653  cdlemg18a  40672  cdlemg24  40682  cdlemg29  40699  cdlemg33b  40701  cdlemg38  40709  cdlemg39  40710  cdlemg40  40711  cdlemg44b  40726  cdlemj2  40816  cdlemk7  40842  cdlemk12  40844  cdlemk12u  40866  cdlemk32  40891  cdlemk25-3  40898  cdlemk34  40904  cdlemkid3N  40927  cdlemkid4  40928  cdlemk11t  40940  cdlemk53  40951  cdlemk55b  40954  cdleml3N  40972  hdmapln1  41900  tfsconcatrev  43337  isubgr3stgrlem6  47970  sepfsepc  48916