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  39325  lfladd  39326  lflsub  39327  lflmul  39328  lflnegcl  39335  lflvscl  39337  lkrlss  39355  3dimlem3  39721  3dimlem4  39724  3dim3  39729  2llnm3N  39829  2lplnja  39879  4atex  40336  4atex3  40341  trlval4  40448  cdleme7c  40505  cdleme7d  40506  cdleme7ga  40508  cdleme21h  40594  cdleme21i  40595  cdleme21j  40596  cdleme21  40597  cdleme32d  40704  cdleme32f  40706  cdleme35h2  40717  cdleme38m  40723  cdleme40m  40727  cdlemg8  40891  cdlemg11a  40897  cdlemg10a  40900  cdlemg12b  40904  cdlemg12d  40906  cdlemg12f  40908  cdlemg12g  40909  cdlemg15a  40915  cdlemg16  40917  cdlemg16z  40919  cdlemg18a  40938  cdlemg24  40948  cdlemg29  40965  cdlemg33b  40967  cdlemg38  40975  cdlemg39  40976  cdlemg40  40977  cdlemg44b  40992  cdlemj2  41082  cdlemk7  41108  cdlemk12  41110  cdlemk12u  41132  cdlemk32  41157  cdlemk25-3  41164  cdlemk34  41170  cdlemkid3N  41193  cdlemkid4  41194  cdlemk11t  41206  cdlemk53  41217  cdlemk55b  41220  cdleml3N  41238  hdmapln1  42166  tfsconcatrev  43590  isubgr3stgrlem6  48217  sepfsepc  49173