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  14390  pythagtriplem18  16741  initoeu2  17920  psgnunilem1  19403  mulmarep1gsum1  22486  mulmarep1gsum2  22487  smadiadetlem4  22582  cramerimplem2  22597  cramerlem2  22601  cramer  22604  cnhaus  23267  dishaus  23295  ordthauslem  23296  pthaus  23551  txhaus  23560  xkohaus  23566  regr1lem  23652  methaus  24433  metnrmlem3  24775  nosupres  27644  nosupbnd1lem1  27645  nosupbnd2  27653  noinfres  27659  noinfbnd1lem1  27660  iscgrad  28787  f1otrge  28848  axpaschlem  28916  wwlksnwwlksnon  29891  n4cyclfrgr  30266  br8d  32586  lt2addrd  32729  xlt2addrd  32737  br8  35788  br4  35790  btwnxfr  36089  lineext  36109  brsegle  36141  brsegle2  36142  lfl0  39103  lfladd  39104  lflsub  39105  lflmul  39106  lflnegcl  39113  lflvscl  39115  lkrlss  39133  3dimlem3  39499  3dimlem4  39502  3dim3  39507  2llnm3N  39607  2lplnja  39657  4atex  40114  4atex3  40119  trlval4  40226  cdleme7c  40283  cdleme7d  40284  cdleme7ga  40286  cdleme21h  40372  cdleme21i  40373  cdleme21j  40374  cdleme21  40375  cdleme32d  40482  cdleme32f  40484  cdleme35h2  40495  cdleme38m  40501  cdleme40m  40505  cdlemg8  40669  cdlemg11a  40675  cdlemg10a  40678  cdlemg12b  40682  cdlemg12d  40684  cdlemg12f  40686  cdlemg12g  40687  cdlemg15a  40693  cdlemg16  40695  cdlemg16z  40697  cdlemg18a  40716  cdlemg24  40726  cdlemg29  40743  cdlemg33b  40745  cdlemg38  40753  cdlemg39  40754  cdlemg40  40755  cdlemg44b  40770  cdlemj2  40860  cdlemk7  40886  cdlemk12  40888  cdlemk12u  40910  cdlemk32  40935  cdlemk25-3  40942  cdlemk34  40948  cdlemkid3N  40971  cdlemkid4  40972  cdlemk11t  40984  cdlemk53  40995  cdlemk55b  40998  cdleml3N  41016  hdmapln1  41944  tfsconcatrev  43380  isubgr3stgrlem6  48001  sepfsepc  48958