Theorem syl113anc 1385

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

Syntax hints:   → wi 4   ∧ w3a 1087

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 1089

This theorem is referenced by:  syl123anc  1390  syl213anc  1392  hash7g  14448  pythagtriplem18  16803  initoeu2  17983  psgnunilem1  19468  mulmarep1gsum1  22538  mulmarep1gsum2  22539  smadiadetlem4  22634  cramerimplem2  22649  cramerlem2  22653  cramer  22656  cnhaus  23319  dishaus  23347  ordthauslem  23348  pthaus  23603  txhaus  23612  xkohaus  23618  regr1lem  23704  methaus  24485  metnrmlem3  24827  nosupres  27671  nosupbnd1lem1  27672  nosupbnd2  27680  noinfres  27686  noinfbnd1lem1  27687  iscgrad  28879  f1otrge  28940  axpaschlem  29009  wwlksnwwlksnon  29983  n4cyclfrgr  30361  br8d  32681  lt2addrd  32823  xlt2addrd  32832  br8  35938  br4  35940  btwnxfr  36238  lineext  36258  brsegle  36290  brsegle2  36291  lfl0  39511  lfladd  39512  lflsub  39513  lflmul  39514  lflnegcl  39521  lflvscl  39523  lkrlss  39541  3dimlem3  39907  3dimlem4  39910  3dim3  39915  2llnm3N  40015  2lplnja  40065  4atex  40522  4atex3  40527  trlval4  40634  cdleme7c  40691  cdleme7d  40692  cdleme7ga  40694  cdleme21h  40780  cdleme21i  40781  cdleme21j  40782  cdleme21  40783  cdleme32d  40890  cdleme32f  40892  cdleme35h2  40903  cdleme38m  40909  cdleme40m  40913  cdlemg8  41077  cdlemg11a  41083  cdlemg10a  41086  cdlemg12b  41090  cdlemg12d  41092  cdlemg12f  41094  cdlemg12g  41095  cdlemg15a  41101  cdlemg16  41103  cdlemg16z  41105  cdlemg18a  41124  cdlemg24  41134  cdlemg29  41151  cdlemg33b  41153  cdlemg38  41161  cdlemg39  41162  cdlemg40  41163  cdlemg44b  41178  cdlemj2  41268  cdlemk7  41294  cdlemk12  41296  cdlemk12u  41318  cdlemk32  41343  cdlemk25-3  41350  cdlemk34  41356  cdlemkid3N  41379  cdlemkid4  41380  cdlemk11t  41392  cdlemk53  41403  cdlemk55b  41406  cdleml3N  41424  hdmapln1  42352  tfsconcatrev  43776  isubgr3stgrlem6  48447  sepfsepc  49403