Theorem syl333anc 1410

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

Syntax hints:   → wi 4   ∧ w3a 1092

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 208  df-an 397  df-3an 1094

This theorem is referenced by:  eengtrkg  29080  ofscom  36242  cgrextend  36243  segconeq  36245  ifscgr  36279  cgrsub  36280  btwnxfr  36291  fscgr  36315  linecgr  36316  btwnconn1lem4  36325  btwnconn1lem5  36326  btwnconn1lem6  36327  btwnconn1lem8  36329  btwnconn1lem11  36332  seglecgr12  36346  colinbtwnle  36353  lshpkrlem6  39614  ps-2c  40027  pmodlem1  40345  pmodlem2  40346  dalawlem4  40373  dalawlem9  40378  4atexlemc  40568  cdleme11l  40768  cdleme15c  40775  cdleme16  40784  cdleme19e  40806  cdleme20l2  40820  cdleme20l  40821  cdleme20m  40822  cdleme20  40823  cdleme21d  40829  cdleme21e  40830  cdleme26ee  40859  cdleme26eALTN  40860  cdleme27a  40866  cdleme28b  40870  cdleme28c  40871  cdleme36m  40960  cdlemg12  41149  cdlemg16ALTN  41157  cdlemg17iqN  41173  cdlemg18c  41179  cdlemg19  41183  cdlemg21  41185  cdlemg28  41203  cdlemk11  41348  cdlemk12  41349  cdlemk16a  41355  cdlemk16  41356  cdlemk18  41367  cdlemk19  41368  cdlemk11u  41370  cdlemk12u  41371  cdlemk21N  41372  cdlemk20  41373  cdlemkoatnle-2N  41374  cdlemk13-2N  41375  cdlemkole-2N  41376  cdlemk14-2N  41377  cdlemk15-2N  41378  cdlemk16-2N  41379  cdlemk17-2N  41380  cdlemk18-2N  41385  cdlemk19-2N  41386  cdlemk7u-2N  41387  cdlemk11u-2N  41388  cdlemk12u-2N  41389  cdlemk22  41392  cdlemk30  41393  cdlemk23-3  41401  cdlemk26b-3  41404  cdlemk26-3  41405  cdlemk27-3  41406  cdlemk11ta  41428  cdlemk47  41448  dia2dimlem1  41563