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 1129	. 2 ⊢ (𝜑 → (𝜃 ∧ 𝜏 ∧ 𝜂))
7		syl113anc.6	. 2 ⊢ ((𝜓 ∧ 𝜒 ∧ (𝜃 ∧ 𝜏 ∧ 𝜂)) → 𝜁)
8	1, 2, 6, 7	syl3anc 1373	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  1389  syl213anc  1391  hash7g  14525  pythagtriplem18  16870  initoeu2  18061  psgnunilem1  19511  mulmarep1gsum1  22579  mulmarep1gsum2  22580  smadiadetlem4  22675  cramerimplem2  22690  cramerlem2  22694  cramer  22697  cnhaus  23362  dishaus  23390  ordthauslem  23391  pthaus  23646  txhaus  23655  xkohaus  23661  regr1lem  23747  methaus  24533  metnrmlem3  24883  nosupres  27752  nosupbnd1lem1  27753  nosupbnd2  27761  noinfres  27767  noinfbnd1lem1  27768  iscgrad  28819  f1otrge  28880  axpaschlem  28955  wwlksnwwlksnon  29935  n4cyclfrgr  30310  br8d  32622  lt2addrd  32755  xlt2addrd  32762  br8  35756  br4  35758  btwnxfr  36057  lineext  36077  brsegle  36109  brsegle2  36110  lfl0  39066  lfladd  39067  lflsub  39068  lflmul  39069  lflnegcl  39076  lflvscl  39078  lkrlss  39096  3dimlem3  39463  3dimlem4  39466  3dim3  39471  2llnm3N  39571  2lplnja  39621  4atex  40078  4atex3  40083  trlval4  40190  cdleme7c  40247  cdleme7d  40248  cdleme7ga  40250  cdleme21h  40336  cdleme21i  40337  cdleme21j  40338  cdleme21  40339  cdleme32d  40446  cdleme32f  40448  cdleme35h2  40459  cdleme38m  40465  cdleme40m  40469  cdlemg8  40633  cdlemg11a  40639  cdlemg10a  40642  cdlemg12b  40646  cdlemg12d  40648  cdlemg12f  40650  cdlemg12g  40651  cdlemg15a  40657  cdlemg16  40659  cdlemg16z  40661  cdlemg18a  40680  cdlemg24  40690  cdlemg29  40707  cdlemg33b  40709  cdlemg38  40717  cdlemg39  40718  cdlemg40  40719  cdlemg44b  40734  cdlemj2  40824  cdlemk7  40850  cdlemk12  40852  cdlemk12u  40874  cdlemk32  40899  cdlemk25-3  40906  cdlemk34  40912  cdlemkid3N  40935  cdlemkid4  40936  cdlemk11t  40948  cdlemk53  40959  cdlemk55b  40962  cdleml3N  40980  hdmapln1  41908  tfsconcatrev  43361  isubgr3stgrlem6  47938  sepfsepc  48825