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 206  df-an 397  df-3an 1089

This theorem is referenced by:  eengtrkg  28241  ofscom  34974  cgrextend  34975  segconeq  34977  ifscgr  35011  cgrsub  35012  btwnxfr  35023  fscgr  35047  linecgr  35048  btwnconn1lem4  35057  btwnconn1lem5  35058  btwnconn1lem6  35059  btwnconn1lem8  35061  btwnconn1lem11  35064  seglecgr12  35078  colinbtwnle  35085  lshpkrlem6  37980  ps-2c  38394  pmodlem1  38712  pmodlem2  38713  dalawlem4  38740  dalawlem9  38745  4atexlemc  38935  cdleme11l  39135  cdleme15c  39142  cdleme16  39151  cdleme19e  39173  cdleme20l2  39187  cdleme20l  39188  cdleme20m  39189  cdleme20  39190  cdleme21d  39196  cdleme21e  39197  cdleme26ee  39226  cdleme26eALTN  39227  cdleme27a  39233  cdleme28b  39237  cdleme28c  39238  cdleme36m  39327  cdlemg12  39516  cdlemg16ALTN  39524  cdlemg17iqN  39540  cdlemg18c  39546  cdlemg19  39550  cdlemg21  39552  cdlemg28  39570  cdlemk11  39715  cdlemk12  39716  cdlemk16a  39722  cdlemk16  39723  cdlemk18  39734  cdlemk19  39735  cdlemk11u  39737  cdlemk12u  39738  cdlemk21N  39739  cdlemk20  39740  cdlemkoatnle-2N  39741  cdlemk13-2N  39742  cdlemkole-2N  39743  cdlemk14-2N  39744  cdlemk15-2N  39745  cdlemk16-2N  39746  cdlemk17-2N  39747  cdlemk18-2N  39752  cdlemk19-2N  39753  cdlemk7u-2N  39754  cdlemk11u-2N  39755  cdlemk12u-2N  39756  cdlemk22  39759  cdlemk30  39760  cdlemk23-3  39768  cdlemk26b-3  39771  cdlemk26-3  39772  cdlemk27-3  39773  cdlemk11ta  39795  cdlemk47  39815  dia2dimlem1  39930