Theorem syl113anc 1390

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 1134	. 2 ⊢ (𝜑 → (𝜃 ∧ 𝜏 ∧ 𝜂))
7		syl113anc.6	. 2 ⊢ ((𝜓 ∧ 𝜒 ∧ (𝜃 ∧ 𝜏 ∧ 𝜂)) → 𝜁)
8	1, 2, 6, 7	syl3anc 1379	1 ⊢ (𝜑 → 𝜁)

Syntax hints:   → wi 4   ∧ w3a 1092

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 208  df-an 397  df-3an 1094

This theorem is referenced by:  syl123anc  1395  syl213anc  1397  hash7g  14446  pythagtriplem18  16801  initoeu2  17981  psgnunilem1  19466  mulmarep1gsum1  22563  mulmarep1gsum2  22564  smadiadetlem4  22659  cramerimplem2  22674  cramerlem2  22678  cramer  22681  cnhaus  23344  dishaus  23372  ordthauslem  23373  pthaus  23628  txhaus  23637  xkohaus  23643  regr1lem  23729  methaus  24510  metnrmlem3  24852  nosupres  27696  nosupbnd1lem1  27697  nosupbnd2  27705  noinfres  27711  noinfbnd1lem1  27712  iscgrad  28904  f1otrge  28965  axpaschlem  29034  wwlksnwwlksnon  30008  n4cyclfrgr  30386  br8d  32707  lt2addrd  32849  xlt2addrd  32858  br8  35991  br4  35993  btwnxfr  36291  lineext  36311  brsegle  36343  brsegle2  36344  lfl0  39564  lfladd  39565  lflsub  39566  lflmul  39567  lflnegcl  39574  lflvscl  39576  lkrlss  39594  3dimlem3  39960  3dimlem4  39963  3dim3  39968  2llnm3N  40068  2lplnja  40118  4atex  40575  4atex3  40580  trlval4  40687  cdleme7c  40744  cdleme7d  40745  cdleme7ga  40747  cdleme21h  40833  cdleme21i  40834  cdleme21j  40835  cdleme21  40836  cdleme32d  40943  cdleme32f  40945  cdleme35h2  40956  cdleme38m  40962  cdleme40m  40966  cdlemg8  41130  cdlemg11a  41136  cdlemg10a  41139  cdlemg12b  41143  cdlemg12d  41145  cdlemg12f  41147  cdlemg12g  41148  cdlemg15a  41154  cdlemg16  41156  cdlemg16z  41158  cdlemg18a  41177  cdlemg24  41187  cdlemg29  41204  cdlemg33b  41206  cdlemg38  41214  cdlemg39  41215  cdlemg40  41216  cdlemg44b  41231  cdlemj2  41321  cdlemk7  41347  cdlemk12  41349  cdlemk12u  41371  cdlemk32  41396  cdlemk25-3  41403  cdlemk34  41409  cdlemkid3N  41432  cdlemkid4  41433  cdlemk11t  41445  cdlemk53  41456  cdlemk55b  41459  cdleml3N  41477  hdmapln1  42405  tfsconcatrev  43800  isubgr3stgrlem6  48469  sepfsepc  49425