Theorem syl113anc 1507

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

Syntax hints:   → wi 4   ∧ w3a 1113

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 199  df-an 387  df-3an 1115

This theorem is referenced by:  syl123anc  1512  syl213anc  1514  pythagtriplem18  15907  initoeu2  17017  psgnunilem1  18262  mulmarep1gsum1  20746  mulmarep1gsum2  20747  smadiadetlem4  20843  cramerimplem2  20859  cramerlem2  20863  cramer  20866  cnhaus  21528  dishaus  21556  ordthauslem  21557  pthaus  21811  txhaus  21820  xkohaus  21826  regr1lem  21912  methaus  22694  metnrmlem3  23033  f1otrge  26170  axpaschlem  26238  wwlksnwwlksnon  27243  n4cyclfrgr  27671  br8d  29968  lt2addrd  30062  xlt2addrd  30069  br8  32187  br4  32189  nosupres  32391  nosupbnd1lem1  32392  nosupbnd2  32400  btwnxfr  32701  lineext  32721  brsegle  32753  brsegle2  32754  lfl0  35139  lfladd  35140  lflsub  35141  lflmul  35142  lflnegcl  35149  lflvscl  35151  lkrlss  35169  3dimlem3  35535  3dimlem4  35538  3dim3  35543  2llnm3N  35643  2lplnja  35693  4atex  36150  4atex3  36155  trlval4  36262  cdleme7c  36319  cdleme7d  36320  cdleme7ga  36322  cdleme21h  36408  cdleme21i  36409  cdleme21j  36410  cdleme21  36411  cdleme32d  36518  cdleme32f  36520  cdleme35h2  36531  cdleme38m  36537  cdleme40m  36541  cdlemg8  36705  cdlemg11a  36711  cdlemg10a  36714  cdlemg12b  36718  cdlemg12d  36720  cdlemg12f  36722  cdlemg12g  36723  cdlemg15a  36729  cdlemg16  36731  cdlemg16z  36733  cdlemg18a  36752  cdlemg24  36762  cdlemg29  36779  cdlemg33b  36781  cdlemg38  36789  cdlemg39  36790  cdlemg40  36791  cdlemg44b  36806  cdlemj2  36896  cdlemk7  36922  cdlemk12  36924  cdlemk12u  36946  cdlemk32  36971  cdlemk25-3  36978  cdlemk34  36984  cdlemkid3N  37007  cdlemkid4  37008  cdlemk11t  37020  cdlemk53  37031  cdlemk55b  37034  cdleml3N  37052  hdmapln1  37980