Theorem syl113anc 1409

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

Syntax hints:   → wi 4   ∧ w3a 1103

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 210  df-an 401  df-3an 1105

This theorem is referenced by:  syl123anc  1414  syl213anc  1416  hash7g  14525  pythagtriplem18  16893  initoeu2  18074  psgnunilem1  19564  mulmarep1gsum1  22711  mulmarep1gsum2  22712  smadiadetlem4  22807  cramerimplem2  22822  cramerlem2  22826  cramer  22829  cnhaus  23492  dishaus  23520  ordthauslem  23521  pthaus  23776  txhaus  23785  xkohaus  23791  regr1lem  23877  methaus  24658  metnrmlem3  25000  nosupres  27852  nosupbnd1lem1  27853  nosupbnd2  27861  noinfres  27867  noinfbnd1lem1  27868  iscgrad  29103  f1otrge  29202  axpaschlem  29271  wwlksnwwlksnon  30245  n4cyclfrgr  30623  br8d  32934  lt2addrd  33076  xlt2addrd  33085  br8  36229  br4  36231  btwnxfr  36529  lineext  36549  brsegle  36581  brsegle2  36582  lfl0  39820  lfladd  39821  lflsub  39822  lflmul  39823  lflnegcl  39830  lflvscl  39832  lkrlss  39850  3dimlem3  40216  3dimlem4  40219  3dim3  40224  2llnm3N  40324  2lplnja  40374  4atex  40831  4atex3  40836  trlval4  40943  cdleme7c  41000  cdleme7d  41001  cdleme7ga  41003  cdleme21h  41089  cdleme21i  41090  cdleme21j  41091  cdleme21  41092  cdleme32d  41199  cdleme32f  41201  cdleme35h2  41212  cdleme38m  41218  cdleme40m  41222  cdlemg8  41386  cdlemg11a  41392  cdlemg10a  41395  cdlemg12b  41399  cdlemg12d  41401  cdlemg12f  41403  cdlemg12g  41404  cdlemg15a  41410  cdlemg16  41412  cdlemg16z  41414  cdlemg18a  41433  cdlemg24  41443  cdlemg29  41460  cdlemg33b  41462  cdlemg38  41470  cdlemg39  41471  cdlemg40  41472  cdlemg44b  41487  cdlemj2  41577  cdlemk7  41603  cdlemk12  41605  cdlemk12u  41627  cdlemk32  41652  cdlemk25-3  41659  cdlemk34  41665  cdlemkid3N  41688  cdlemkid4  41689  cdlemk11t  41701  cdlemk53  41712  cdlemk55b  41715  cdleml3N  41733  hdmapln1  42661  tfsconcatrev  44058  isubgr3stgrlem6  48719  sepfsepc  49689