Theorem syl333anc 1525

Description: A syllogism inference combined with contraction. (Contributed by NM, 10-Mar-2012.)

Hypotheses

Ref	Expression
syl3anc.1	⊢ (𝜑 → 𝜓)
syl3anc.2	⊢ (𝜑 → 𝜒)
syl3anc.3	⊢ (𝜑 → 𝜃)
syl3Xanc.4	⊢ (𝜑 → 𝜏)
syl23anc.5	⊢ (𝜑 → 𝜂)
syl33anc.6	⊢ (𝜑 → 𝜁)
syl133anc.7	⊢ (𝜑 → 𝜎)
syl233anc.8	⊢ (𝜑 → 𝜌)
syl333anc.9	⊢ (𝜑 → 𝜇)
syl333anc.10	⊢ (((𝜓 ∧ 𝜒 ∧ 𝜃) ∧ (𝜏 ∧ 𝜂 ∧ 𝜁) ∧ (𝜎 ∧ 𝜌 ∧ 𝜇)) → 𝜆)

Assertion

Ref	Expression
syl333anc	⊢ (𝜑 → 𝜆)

Proof of Theorem syl333anc

Step	Hyp	Ref	Expression
1		syl3anc.1	. 2 ⊢ (𝜑 → 𝜓)
2		syl3anc.2	. 2 ⊢ (𝜑 → 𝜒)
3		syl3anc.3	. 2 ⊢ (𝜑 → 𝜃)
4		syl3Xanc.4	. 2 ⊢ (𝜑 → 𝜏)
5		syl23anc.5	. 2 ⊢ (𝜑 → 𝜂)
6		syl33anc.6	. 2 ⊢ (𝜑 → 𝜁)
7		syl133anc.7	. . 3 ⊢ (𝜑 → 𝜎)
8		syl233anc.8	. . 3 ⊢ (𝜑 → 𝜌)
9		syl333anc.9	. . 3 ⊢ (𝜑 → 𝜇)
10	7, 8, 9	3jca 1162	. 2 ⊢ (𝜑 → (𝜎 ∧ 𝜌 ∧ 𝜇))
11		syl333anc.10	. 2 ⊢ (((𝜓 ∧ 𝜒 ∧ 𝜃) ∧ (𝜏 ∧ 𝜂 ∧ 𝜁) ∧ (𝜎 ∧ 𝜌 ∧ 𝜇)) → 𝜆)
12	1, 2, 3, 4, 5, 6, 10, 11	syl331anc 1518	1 ⊢ (𝜑 → 𝜆)

Syntax hints:   → wi 4   ∧ w3a 1111

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 1113

This theorem is referenced by:  eengtrkg  26285  ofscom  32642  cgrextend  32643  segconeq  32645  ifscgr  32679  cgrsub  32680  btwnxfr  32691  fscgr  32715  linecgr  32716  btwnconn1lem4  32725  btwnconn1lem5  32726  btwnconn1lem6  32727  btwnconn1lem8  32729  btwnconn1lem11  32732  seglecgr12  32746  colinbtwnle  32753  lshpkrlem6  35183  ps-2c  35596  pmodlem1  35914  pmodlem2  35915  dalawlem4  35942  dalawlem9  35947  4atexlemc  36137  cdleme11l  36337  cdleme15c  36344  cdleme16  36353  cdleme19e  36375  cdleme20l2  36389  cdleme20l  36390  cdleme20m  36391  cdleme20  36392  cdleme21d  36398  cdleme21e  36399  cdleme26ee  36428  cdleme26eALTN  36429  cdleme27a  36435  cdleme28b  36439  cdleme28c  36440  cdleme36m  36529  cdlemg12  36718  cdlemg16ALTN  36726  cdlemg17iqN  36742  cdlemg18c  36748  cdlemg19  36752  cdlemg21  36754  cdlemg28  36772  cdlemk11  36917  cdlemk12  36918  cdlemk16a  36924  cdlemk16  36925  cdlemk18  36936  cdlemk19  36937  cdlemk11u  36939  cdlemk12u  36940  cdlemk21N  36941  cdlemk20  36942  cdlemkoatnle-2N  36943  cdlemk13-2N  36944  cdlemkole-2N  36945  cdlemk14-2N  36946  cdlemk15-2N  36947  cdlemk16-2N  36948  cdlemk17-2N  36949  cdlemk18-2N  36954  cdlemk19-2N  36955  cdlemk7u-2N  36956  cdlemk11u-2N  36957  cdlemk12u-2N  36958  cdlemk22  36961  cdlemk30  36962  cdlemk23-3  36970  cdlemk26b-3  36973  cdlemk26-3  36974  cdlemk27-3  36975  cdlemk11ta  36997  cdlemk47  37017  dia2dimlem1  37132