Theorem syl333anc 1403

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 1129	. 2 ⊢ (𝜑 → (𝜎 ∧ 𝜌 ∧ 𝜇))
11		syl333anc.10	. 2 ⊢ (((𝜓 ∧ 𝜒 ∧ 𝜃) ∧ (𝜏 ∧ 𝜂 ∧ 𝜁) ∧ (𝜎 ∧ 𝜌 ∧ 𝜇)) → 𝜆)
12	1, 2, 3, 4, 5, 6, 10, 11	syl331anc 1396	1 ⊢ (𝜑 → 𝜆)

Syntax hints:   → wi 4   ∧ w3a 1088

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 398  df-3an 1090

This theorem is referenced by:  eengtrkg  28244  ofscom  34979  cgrextend  34980  segconeq  34982  ifscgr  35016  cgrsub  35017  btwnxfr  35028  fscgr  35052  linecgr  35053  btwnconn1lem4  35062  btwnconn1lem5  35063  btwnconn1lem6  35064  btwnconn1lem8  35066  btwnconn1lem11  35069  seglecgr12  35083  colinbtwnle  35090  lshpkrlem6  37985  ps-2c  38399  pmodlem1  38717  pmodlem2  38718  dalawlem4  38745  dalawlem9  38750  4atexlemc  38940  cdleme11l  39140  cdleme15c  39147  cdleme16  39156  cdleme19e  39178  cdleme20l2  39192  cdleme20l  39193  cdleme20m  39194  cdleme20  39195  cdleme21d  39201  cdleme21e  39202  cdleme26ee  39231  cdleme26eALTN  39232  cdleme27a  39238  cdleme28b  39242  cdleme28c  39243  cdleme36m  39332  cdlemg12  39521  cdlemg16ALTN  39529  cdlemg17iqN  39545  cdlemg18c  39551  cdlemg19  39555  cdlemg21  39557  cdlemg28  39575  cdlemk11  39720  cdlemk12  39721  cdlemk16a  39727  cdlemk16  39728  cdlemk18  39739  cdlemk19  39740  cdlemk11u  39742  cdlemk12u  39743  cdlemk21N  39744  cdlemk20  39745  cdlemkoatnle-2N  39746  cdlemk13-2N  39747  cdlemkole-2N  39748  cdlemk14-2N  39749  cdlemk15-2N  39750  cdlemk16-2N  39751  cdlemk17-2N  39752  cdlemk18-2N  39757  cdlemk19-2N  39758  cdlemk7u-2N  39759  cdlemk11u-2N  39760  cdlemk12u-2N  39761  cdlemk22  39764  cdlemk30  39765  cdlemk23-3  39773  cdlemk26b-3  39776  cdlemk26-3  39777  cdlemk27-3  39778  cdlemk11ta  39800  cdlemk47  39820  dia2dimlem1  39935