Theorem syl113anc 1330

Description: Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.)

Hypotheses

Ref	Expression
syl12anc.1	⊢ (𝜑 → 𝜓)
syl12anc.2	⊢ (𝜑 → 𝜒)
syl12anc.3	⊢ (𝜑 → 𝜃)
syl22anc.4	⊢ (𝜑 → 𝜏)
syl23anc.5	⊢ (𝜑 → 𝜂)
syl113anc.6	⊢ ((𝜓 ∧ 𝜒 ∧ (𝜃 ∧ 𝜏 ∧ 𝜂)) → 𝜁)

Assertion

Ref	Expression
syl113anc	⊢ (𝜑 → 𝜁)

Proof of Theorem syl113anc

Step	Hyp	Ref	Expression
1		syl12anc.1	. 2 ⊢ (𝜑 → 𝜓)
2		syl12anc.2	. 2 ⊢ (𝜑 → 𝜒)
3		syl12anc.3	. . 3 ⊢ (𝜑 → 𝜃)
4		syl22anc.4	. . 3 ⊢ (𝜑 → 𝜏)
5		syl23anc.5	. . 3 ⊢ (𝜑 → 𝜂)
6	3, 4, 5	3jca 1235	. 2 ⊢ (𝜑 → (𝜃 ∧ 𝜏 ∧ 𝜂))
7		syl113anc.6	. 2 ⊢ ((𝜓 ∧ 𝜒 ∧ (𝜃 ∧ 𝜏 ∧ 𝜂)) → 𝜁)
8	1, 2, 6, 7	syl3anc 1318	1 ⊢ (𝜑 → 𝜁)

Syntax hints:   → wi 4   ∧ w3a 1031

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 196  df-an 385  df-3an 1033

This theorem is referenced by:  syl123anc  1335  syl213anc  1337  pythagtriplem18  15375  initoeu2  16489  psgnunilem1  17736  mulmarep1gsum1  20198  mulmarep1gsum2  20199  smadiadetlem4  20294  cramerimplem2  20309  cramerlem2  20313  cramer  20316  cnhaus  20968  dishaus  20996  ordthauslem  20997  pthaus  21251  txhaus  21260  xkohaus  21266  regr1lem  21352  methaus  22135  metnrmlem3  22472  f1otrge  25552  axpaschlem  25620  n4cyclfrgra  26545  br8d  28802  lt2addrd  28903  xlt2addrd  28913  br8  30899  br4  30901  btwnxfr  31333  lineext  31353  brsegle  31385  brsegle2  31386  lfl0  33370  lfladd  33371  lflsub  33372  lflmul  33373  lflnegcl  33380  lflvscl  33382  lkrlss  33400  3dimlem3  33765  3dimlem4  33768  3dim3  33773  2llnm3N  33873  2lplnja  33923  4atex  34380  4atex3  34385  trlval4  34493  cdleme7c  34550  cdleme7d  34551  cdleme7ga  34553  cdleme21h  34640  cdleme21i  34641  cdleme21j  34642  cdleme21  34643  cdleme32d  34750  cdleme32f  34752  cdleme35h2  34763  cdleme38m  34769  cdleme40m  34773  cdlemg8  34937  cdlemg11a  34943  cdlemg10a  34946  cdlemg12b  34950  cdlemg12d  34952  cdlemg12f  34954  cdlemg12g  34955  cdlemg15a  34961  cdlemg16  34963  cdlemg16z  34965  cdlemg18a  34984  cdlemg24  34994  cdlemg29  35011  cdlemg33b  35013  cdlemg38  35021  cdlemg39  35022  cdlemg40  35023  cdlemg44b  35038  cdlemj2  35128  cdlemk7  35154  cdlemk12  35156  cdlemk12u  35178  cdlemk32  35203  cdlemk25-3  35210  cdlemk34  35216  cdlemkid3N  35239  cdlemkid4  35240  cdlemk11t  35252  cdlemk53  35263  cdlemk55b  35266  cdleml3N  35284  hdmapln1  36216  wwlksnwwlksnon  41121  n4cyclfrgr  41461