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  14504  pythagtriplem18  16852  initoeu2  18029  psgnunilem1  19474  mulmarep1gsum1  22511  mulmarep1gsum2  22512  smadiadetlem4  22607  cramerimplem2  22622  cramerlem2  22626  cramer  22629  cnhaus  23292  dishaus  23320  ordthauslem  23321  pthaus  23576  txhaus  23585  xkohaus  23591  regr1lem  23677  methaus  24459  metnrmlem3  24801  nosupres  27671  nosupbnd1lem1  27672  nosupbnd2  27680  noinfres  27686  noinfbnd1lem1  27687  iscgrad  28790  f1otrge  28851  axpaschlem  28919  wwlksnwwlksnon  29897  n4cyclfrgr  30272  br8d  32590  lt2addrd  32728  xlt2addrd  32736  br8  35773  br4  35775  btwnxfr  36074  lineext  36094  brsegle  36126  brsegle2  36127  lfl0  39083  lfladd  39084  lflsub  39085  lflmul  39086  lflnegcl  39093  lflvscl  39095  lkrlss  39113  3dimlem3  39480  3dimlem4  39483  3dim3  39488  2llnm3N  39588  2lplnja  39638  4atex  40095  4atex3  40100  trlval4  40207  cdleme7c  40264  cdleme7d  40265  cdleme7ga  40267  cdleme21h  40353  cdleme21i  40354  cdleme21j  40355  cdleme21  40356  cdleme32d  40463  cdleme32f  40465  cdleme35h2  40476  cdleme38m  40482  cdleme40m  40486  cdlemg8  40650  cdlemg11a  40656  cdlemg10a  40659  cdlemg12b  40663  cdlemg12d  40665  cdlemg12f  40667  cdlemg12g  40668  cdlemg15a  40674  cdlemg16  40676  cdlemg16z  40678  cdlemg18a  40697  cdlemg24  40707  cdlemg29  40724  cdlemg33b  40726  cdlemg38  40734  cdlemg39  40735  cdlemg40  40736  cdlemg44b  40751  cdlemj2  40841  cdlemk7  40867  cdlemk12  40869  cdlemk12u  40891  cdlemk32  40916  cdlemk25-3  40923  cdlemk34  40929  cdlemkid3N  40952  cdlemkid4  40953  cdlemk11t  40965  cdlemk53  40976  cdlemk55b  40979  cdleml3N  40997  hdmapln1  41925  tfsconcatrev  43372  isubgr3stgrlem6  47983  sepfsepc  48902