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  14395  pythagtriplem18  16746  initoeu2  17925  psgnunilem1  19407  mulmarep1gsum1  22489  mulmarep1gsum2  22490  smadiadetlem4  22585  cramerimplem2  22600  cramerlem2  22604  cramer  22607  cnhaus  23270  dishaus  23298  ordthauslem  23299  pthaus  23554  txhaus  23563  xkohaus  23569  regr1lem  23655  methaus  24436  metnrmlem3  24778  nosupres  27647  nosupbnd1lem1  27648  nosupbnd2  27656  noinfres  27662  noinfbnd1lem1  27663  iscgrad  28790  f1otrge  28851  axpaschlem  28920  wwlksnwwlksnon  29895  n4cyclfrgr  30273  br8d  32593  lt2addrd  32738  xlt2addrd  32746  br8  35821  br4  35823  btwnxfr  36121  lineext  36141  brsegle  36173  brsegle2  36174  lfl0  39184  lfladd  39185  lflsub  39186  lflmul  39187  lflnegcl  39194  lflvscl  39196  lkrlss  39214  3dimlem3  39580  3dimlem4  39583  3dim3  39588  2llnm3N  39688  2lplnja  39738  4atex  40195  4atex3  40200  trlval4  40307  cdleme7c  40364  cdleme7d  40365  cdleme7ga  40367  cdleme21h  40453  cdleme21i  40454  cdleme21j  40455  cdleme21  40456  cdleme32d  40563  cdleme32f  40565  cdleme35h2  40576  cdleme38m  40582  cdleme40m  40586  cdlemg8  40750  cdlemg11a  40756  cdlemg10a  40759  cdlemg12b  40763  cdlemg12d  40765  cdlemg12f  40767  cdlemg12g  40768  cdlemg15a  40774  cdlemg16  40776  cdlemg16z  40778  cdlemg18a  40797  cdlemg24  40807  cdlemg29  40824  cdlemg33b  40826  cdlemg38  40834  cdlemg39  40835  cdlemg40  40836  cdlemg44b  40851  cdlemj2  40941  cdlemk7  40967  cdlemk12  40969  cdlemk12u  40991  cdlemk32  41016  cdlemk25-3  41023  cdlemk34  41029  cdlemkid3N  41052  cdlemkid4  41053  cdlemk11t  41065  cdlemk53  41076  cdlemk55b  41079  cdleml3N  41097  hdmapln1  42025  tfsconcatrev  43465  isubgr3stgrlem6  48095  sepfsepc  49052