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  14409  pythagtriplem18  16760  initoeu2  17940  psgnunilem1  19422  mulmarep1gsum1  22517  mulmarep1gsum2  22518  smadiadetlem4  22613  cramerimplem2  22628  cramerlem2  22632  cramer  22635  cnhaus  23298  dishaus  23326  ordthauslem  23327  pthaus  23582  txhaus  23591  xkohaus  23597  regr1lem  23683  methaus  24464  metnrmlem3  24806  nosupres  27675  nosupbnd1lem1  27676  nosupbnd2  27684  noinfres  27690  noinfbnd1lem1  27691  iscgrad  28883  f1otrge  28944  axpaschlem  29013  wwlksnwwlksnon  29988  n4cyclfrgr  30366  br8d  32686  lt2addrd  32830  xlt2addrd  32839  br8  35950  br4  35952  btwnxfr  36250  lineext  36270  brsegle  36302  brsegle2  36303  lfl0  39321  lfladd  39322  lflsub  39323  lflmul  39324  lflnegcl  39331  lflvscl  39333  lkrlss  39351  3dimlem3  39717  3dimlem4  39720  3dim3  39725  2llnm3N  39825  2lplnja  39875  4atex  40332  4atex3  40337  trlval4  40444  cdleme7c  40501  cdleme7d  40502  cdleme7ga  40504  cdleme21h  40590  cdleme21i  40591  cdleme21j  40592  cdleme21  40593  cdleme32d  40700  cdleme32f  40702  cdleme35h2  40713  cdleme38m  40719  cdleme40m  40723  cdlemg8  40887  cdlemg11a  40893  cdlemg10a  40896  cdlemg12b  40900  cdlemg12d  40902  cdlemg12f  40904  cdlemg12g  40905  cdlemg15a  40911  cdlemg16  40913  cdlemg16z  40915  cdlemg18a  40934  cdlemg24  40944  cdlemg29  40961  cdlemg33b  40963  cdlemg38  40971  cdlemg39  40972  cdlemg40  40973  cdlemg44b  40988  cdlemj2  41078  cdlemk7  41104  cdlemk12  41106  cdlemk12u  41128  cdlemk32  41153  cdlemk25-3  41160  cdlemk34  41166  cdlemkid3N  41189  cdlemkid4  41190  cdlemk11t  41202  cdlemk53  41213  cdlemk55b  41216  cdleml3N  41234  hdmapln1  42162  tfsconcatrev  43586  isubgr3stgrlem6  48213  sepfsepc  49169