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  14421  pythagtriplem18  16772  initoeu2  17952  psgnunilem1  19434  mulmarep1gsum1  22529  mulmarep1gsum2  22530  smadiadetlem4  22625  cramerimplem2  22640  cramerlem2  22644  cramer  22647  cnhaus  23310  dishaus  23338  ordthauslem  23339  pthaus  23594  txhaus  23603  xkohaus  23609  regr1lem  23695  methaus  24476  metnrmlem3  24818  nosupres  27687  nosupbnd1lem1  27688  nosupbnd2  27696  noinfres  27702  noinfbnd1lem1  27703  iscgrad  28895  f1otrge  28956  axpaschlem  29025  wwlksnwwlksnon  30000  n4cyclfrgr  30378  br8d  32697  lt2addrd  32840  xlt2addrd  32849  br8  35969  br4  35971  btwnxfr  36269  lineext  36289  brsegle  36321  brsegle2  36322  lfl0  39435  lfladd  39436  lflsub  39437  lflmul  39438  lflnegcl  39445  lflvscl  39447  lkrlss  39465  3dimlem3  39831  3dimlem4  39834  3dim3  39839  2llnm3N  39939  2lplnja  39989  4atex  40446  4atex3  40451  trlval4  40558  cdleme7c  40615  cdleme7d  40616  cdleme7ga  40618  cdleme21h  40704  cdleme21i  40705  cdleme21j  40706  cdleme21  40707  cdleme32d  40814  cdleme32f  40816  cdleme35h2  40827  cdleme38m  40833  cdleme40m  40837  cdlemg8  41001  cdlemg11a  41007  cdlemg10a  41010  cdlemg12b  41014  cdlemg12d  41016  cdlemg12f  41018  cdlemg12g  41019  cdlemg15a  41025  cdlemg16  41027  cdlemg16z  41029  cdlemg18a  41048  cdlemg24  41058  cdlemg29  41075  cdlemg33b  41077  cdlemg38  41085  cdlemg39  41086  cdlemg40  41087  cdlemg44b  41102  cdlemj2  41192  cdlemk7  41218  cdlemk12  41220  cdlemk12u  41242  cdlemk32  41267  cdlemk25-3  41274  cdlemk34  41280  cdlemkid3N  41303  cdlemkid4  41304  cdlemk11t  41316  cdlemk53  41327  cdlemk55b  41330  cdleml3N  41348  hdmapln1  42276  tfsconcatrev  43699  isubgr3stgrlem6  48325  sepfsepc  49281