Theorem syl333anc 1404

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 1397	1 ⊢ (𝜑 → 𝜆)

Syntax hints:   → wi 4   ∧ w3a 1086

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 1088

This theorem is referenced by:  eengtrkg  28965  ofscom  36025  cgrextend  36026  segconeq  36028  ifscgr  36062  cgrsub  36063  btwnxfr  36074  fscgr  36098  linecgr  36099  btwnconn1lem4  36108  btwnconn1lem5  36109  btwnconn1lem6  36110  btwnconn1lem8  36112  btwnconn1lem11  36115  seglecgr12  36129  colinbtwnle  36136  lshpkrlem6  39133  ps-2c  39547  pmodlem1  39865  pmodlem2  39866  dalawlem4  39893  dalawlem9  39898  4atexlemc  40088  cdleme11l  40288  cdleme15c  40295  cdleme16  40304  cdleme19e  40326  cdleme20l2  40340  cdleme20l  40341  cdleme20m  40342  cdleme20  40343  cdleme21d  40349  cdleme21e  40350  cdleme26ee  40379  cdleme26eALTN  40380  cdleme27a  40386  cdleme28b  40390  cdleme28c  40391  cdleme36m  40480  cdlemg12  40669  cdlemg16ALTN  40677  cdlemg17iqN  40693  cdlemg18c  40699  cdlemg19  40703  cdlemg21  40705  cdlemg28  40723  cdlemk11  40868  cdlemk12  40869  cdlemk16a  40875  cdlemk16  40876  cdlemk18  40887  cdlemk19  40888  cdlemk11u  40890  cdlemk12u  40891  cdlemk21N  40892  cdlemk20  40893  cdlemkoatnle-2N  40894  cdlemk13-2N  40895  cdlemkole-2N  40896  cdlemk14-2N  40897  cdlemk15-2N  40898  cdlemk16-2N  40899  cdlemk17-2N  40900  cdlemk18-2N  40905  cdlemk19-2N  40906  cdlemk7u-2N  40907  cdlemk11u-2N  40908  cdlemk12u-2N  40909  cdlemk22  40912  cdlemk30  40913  cdlemk23-3  40921  cdlemk26b-3  40924  cdlemk26-3  40925  cdlemk27-3  40926  cdlemk11ta  40948  cdlemk47  40968  dia2dimlem1  41083