Theorem syl333anc 1429

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

Syntax hints:   → wi 4   ∧ w3a 1103

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 210  df-an 401  df-3an 1105

This theorem is referenced by:  eengtrkg  29317  ofscom  36480  cgrextend  36481  segconeq  36483  ifscgr  36517  cgrsub  36518  btwnxfr  36529  fscgr  36553  linecgr  36554  btwnconn1lem4  36563  btwnconn1lem5  36564  btwnconn1lem6  36565  btwnconn1lem8  36567  btwnconn1lem11  36570  seglecgr12  36584  colinbtwnle  36591  lshpkrlem6  39870  ps-2c  40283  pmodlem1  40601  pmodlem2  40602  dalawlem4  40629  dalawlem9  40634  4atexlemc  40824  cdleme11l  41024  cdleme15c  41031  cdleme16  41040  cdleme19e  41062  cdleme20l2  41076  cdleme20l  41077  cdleme20m  41078  cdleme20  41079  cdleme21d  41085  cdleme21e  41086  cdleme26ee  41115  cdleme26eALTN  41116  cdleme27a  41122  cdleme28b  41126  cdleme28c  41127  cdleme36m  41216  cdlemg12  41405  cdlemg16ALTN  41413  cdlemg17iqN  41429  cdlemg18c  41435  cdlemg19  41439  cdlemg21  41441  cdlemg28  41459  cdlemk11  41604  cdlemk12  41605  cdlemk16a  41611  cdlemk16  41612  cdlemk18  41623  cdlemk19  41624  cdlemk11u  41626  cdlemk12u  41627  cdlemk21N  41628  cdlemk20  41629  cdlemkoatnle-2N  41630  cdlemk13-2N  41631  cdlemkole-2N  41632  cdlemk14-2N  41633  cdlemk15-2N  41634  cdlemk16-2N  41635  cdlemk17-2N  41636  cdlemk18-2N  41641  cdlemk19-2N  41642  cdlemk7u-2N  41643  cdlemk11u-2N  41644  cdlemk12u-2N  41645  cdlemk22  41648  cdlemk30  41649  cdlemk23-3  41657  cdlemk26b-3  41660  cdlemk26-3  41661  cdlemk27-3  41662  cdlemk11ta  41684  cdlemk47  41704  dia2dimlem1  41819