Theorem syl113anc 1379

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

Syntax hints:   → wi 4   ∧ w3a 1084

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 210  df-an 400  df-3an 1086

This theorem is referenced by:  syl123anc  1384  syl213anc  1386  pythagtriplem18  16159  initoeu2  17268  psgnunilem1  18613  mulmarep1gsum1  21178  mulmarep1gsum2  21179  smadiadetlem4  21274  cramerimplem2  21289  cramerlem2  21293  cramer  21296  cnhaus  21959  dishaus  21987  ordthauslem  21988  pthaus  22243  txhaus  22252  xkohaus  22258  regr1lem  22344  methaus  23127  metnrmlem3  23466  iscgrad  26605  f1otrge  26666  axpaschlem  26734  wwlksnwwlksnon  27701  n4cyclfrgr  28076  br8d  30374  lt2addrd  30501  xlt2addrd  30508  br8  33105  br4  33107  nosupres  33320  nosupbnd1lem1  33321  nosupbnd2  33329  btwnxfr  33630  lineext  33650  brsegle  33682  brsegle2  33683  lfl0  36361  lfladd  36362  lflsub  36363  lflmul  36364  lflnegcl  36371  lflvscl  36373  lkrlss  36391  3dimlem3  36757  3dimlem4  36760  3dim3  36765  2llnm3N  36865  2lplnja  36915  4atex  37372  4atex3  37377  trlval4  37484  cdleme7c  37541  cdleme7d  37542  cdleme7ga  37544  cdleme21h  37630  cdleme21i  37631  cdleme21j  37632  cdleme21  37633  cdleme32d  37740  cdleme32f  37742  cdleme35h2  37753  cdleme38m  37759  cdleme40m  37763  cdlemg8  37927  cdlemg11a  37933  cdlemg10a  37936  cdlemg12b  37940  cdlemg12d  37942  cdlemg12f  37944  cdlemg12g  37945  cdlemg15a  37951  cdlemg16  37953  cdlemg16z  37955  cdlemg18a  37974  cdlemg24  37984  cdlemg29  38001  cdlemg33b  38003  cdlemg38  38011  cdlemg39  38012  cdlemg40  38013  cdlemg44b  38028  cdlemj2  38118  cdlemk7  38144  cdlemk12  38146  cdlemk12u  38168  cdlemk32  38193  cdlemk25-3  38200  cdlemk34  38206  cdlemkid3N  38229  cdlemkid4  38230  cdlemk11t  38242  cdlemk53  38253  cdlemk55b  38256  cdleml3N  38274  hdmapln1  39202