Theorem syl333anc 1402

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 1128	. 2 ⊢ (𝜑 → (𝜎 ∧ 𝜌 ∧ 𝜇))
11		syl333anc.10	. 2 ⊢ (((𝜓 ∧ 𝜒 ∧ 𝜃) ∧ (𝜏 ∧ 𝜂 ∧ 𝜁) ∧ (𝜎 ∧ 𝜌 ∧ 𝜇)) → 𝜆)
12	1, 2, 3, 4, 5, 6, 10, 11	syl331anc 1395	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:  eengtrkg  29019  ofscom  35971  cgrextend  35972  segconeq  35974  ifscgr  36008  cgrsub  36009  btwnxfr  36020  fscgr  36044  linecgr  36045  btwnconn1lem4  36054  btwnconn1lem5  36055  btwnconn1lem6  36056  btwnconn1lem8  36058  btwnconn1lem11  36061  seglecgr12  36075  colinbtwnle  36082  lshpkrlem6  39071  ps-2c  39485  pmodlem1  39803  pmodlem2  39804  dalawlem4  39831  dalawlem9  39836  4atexlemc  40026  cdleme11l  40226  cdleme15c  40233  cdleme16  40242  cdleme19e  40264  cdleme20l2  40278  cdleme20l  40279  cdleme20m  40280  cdleme20  40281  cdleme21d  40287  cdleme21e  40288  cdleme26ee  40317  cdleme26eALTN  40318  cdleme27a  40324  cdleme28b  40328  cdleme28c  40329  cdleme36m  40418  cdlemg12  40607  cdlemg16ALTN  40615  cdlemg17iqN  40631  cdlemg18c  40637  cdlemg19  40641  cdlemg21  40643  cdlemg28  40661  cdlemk11  40806  cdlemk12  40807  cdlemk16a  40813  cdlemk16  40814  cdlemk18  40825  cdlemk19  40826  cdlemk11u  40828  cdlemk12u  40829  cdlemk21N  40830  cdlemk20  40831  cdlemkoatnle-2N  40832  cdlemk13-2N  40833  cdlemkole-2N  40834  cdlemk14-2N  40835  cdlemk15-2N  40836  cdlemk16-2N  40837  cdlemk17-2N  40838  cdlemk18-2N  40843  cdlemk19-2N  40844  cdlemk7u-2N  40845  cdlemk11u-2N  40846  cdlemk12u-2N  40847  cdlemk22  40850  cdlemk30  40851  cdlemk23-3  40859  cdlemk26b-3  40862  cdlemk26-3  40863  cdlemk27-3  40864  cdlemk11ta  40886  cdlemk47  40906  dia2dimlem1  41021