Theorem syl113anc 1385

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

Syntax hints:   → wi 4   ∧ w3a 1087

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 1089

This theorem is referenced by:  syl123anc  1390  syl213anc  1392  hash7g  14439  pythagtriplem18  16794  initoeu2  17974  psgnunilem1  19459  mulmarep1gsum1  22548  mulmarep1gsum2  22549  smadiadetlem4  22644  cramerimplem2  22659  cramerlem2  22663  cramer  22666  cnhaus  23329  dishaus  23357  ordthauslem  23358  pthaus  23613  txhaus  23622  xkohaus  23628  regr1lem  23714  methaus  24495  metnrmlem3  24837  nosupres  27685  nosupbnd1lem1  27686  nosupbnd2  27694  noinfres  27700  noinfbnd1lem1  27701  iscgrad  28893  f1otrge  28954  axpaschlem  29023  wwlksnwwlksnon  29998  n4cyclfrgr  30376  br8d  32696  lt2addrd  32838  xlt2addrd  32847  br8  35954  br4  35956  btwnxfr  36254  lineext  36274  brsegle  36306  brsegle2  36307  lfl0  39525  lfladd  39526  lflsub  39527  lflmul  39528  lflnegcl  39535  lflvscl  39537  lkrlss  39555  3dimlem3  39921  3dimlem4  39924  3dim3  39929  2llnm3N  40029  2lplnja  40079  4atex  40536  4atex3  40541  trlval4  40648  cdleme7c  40705  cdleme7d  40706  cdleme7ga  40708  cdleme21h  40794  cdleme21i  40795  cdleme21j  40796  cdleme21  40797  cdleme32d  40904  cdleme32f  40906  cdleme35h2  40917  cdleme38m  40923  cdleme40m  40927  cdlemg8  41091  cdlemg11a  41097  cdlemg10a  41100  cdlemg12b  41104  cdlemg12d  41106  cdlemg12f  41108  cdlemg12g  41109  cdlemg15a  41115  cdlemg16  41117  cdlemg16z  41119  cdlemg18a  41138  cdlemg24  41148  cdlemg29  41165  cdlemg33b  41167  cdlemg38  41175  cdlemg39  41176  cdlemg40  41177  cdlemg44b  41192  cdlemj2  41282  cdlemk7  41308  cdlemk12  41310  cdlemk12u  41332  cdlemk32  41357  cdlemk25-3  41364  cdlemk34  41370  cdlemkid3N  41393  cdlemkid4  41394  cdlemk11t  41406  cdlemk53  41417  cdlemk55b  41420  cdleml3N  41438  hdmapln1  42366  tfsconcatrev  43794  isubgr3stgrlem6  48459  sepfsepc  49415