Theorem syl113anc 1410

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

This proof depends on syntax axioms:   → wi 4   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  syl123anc  1415  syl213anc  1417  hash7g  14661  pythagtriplem18  17042  initoeu2  18223  psgnunilem1  19740  mulmarep1gsum1  22921  mulmarep1gsum2  22922  smadiadetlem4  23017  cramerimplem2  23035  cramerlem2  23039  cramer  23042  cnhaus  23705  dishaus  23733  ordthauslem  23734  pthaus  23990  txhaus  23999  xkohaus  24005  regr1lem  24091  methaus  24872  metnrmlem3  25214  nosupres  28097  nosupbnd1lem1  28098  nosupbnd2  28106  noinfres  28112  noinfbnd1lem1  28113  iscgrad  29351  f1otrge  29482  axpaschlem  29551  wwlksnwwlksnon  30537  n4cyclfrgr  30925  br8d  33277  lt2addrd  33415  xlt2addrd  33424  br8  36712  br4  36714  btwnxfr  37012  lineext  37032  brsegle  37064  brsegle2  37065  lfl0  40325  lfladd  40326  lflsub  40327  lflmul  40328  lflnegcl  40335  lflvscl  40337  lkrlss  40355  3dimlem3  40721  3dimlem4  40724  3dim3  40729  2llnm3N  40829  2lplnja  40879  4atex  41336  4atex3  41341  trlval4  41448  cdleme7c  41505  cdleme7d  41506  cdleme7ga  41508  cdleme21h  41594  cdleme21i  41595  cdleme21j  41596  cdleme21  41597  cdleme32d  41704  cdleme32f  41706  cdleme35h2  41717  cdleme38m  41723  cdleme40m  41727  cdlemg8  41891  cdlemg11a  41897  cdlemg10a  41900  cdlemg12b  41904  cdlemg12d  41906  cdlemg12f  41908  cdlemg12g  41909  cdlemg15a  41915  cdlemg16  41917  cdlemg16z  41919  cdlemg18a  41938  cdlemg24  41948  cdlemg29  41965  cdlemg33b  41967  cdlemg38  41975  cdlemg39  41976  cdlemg40  41977  cdlemg44b  41992  cdlemj2  42082  cdlemk7  42108  cdlemk12  42110  cdlemk12u  42132  cdlemk32  42157  cdlemk25-3  42164  cdlemk34  42170  cdlemkid3N  42193  cdlemkid4  42194  cdlemk11t  42206  cdlemk53  42217  cdlemk55b  42220  cdleml3N  42238  hdmapln1  43166  tfsconcatrev  44553  isubgr3stgrlem6  49284  sepfsepc  50257