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

This proof depends on syntax axioms:   → wi 4   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  eengtrkg  29443  ofscom  36587  cgrextend  36588  segconeq  36590  ifscgr  36624  cgrsub  36625  btwnxfr  36636  fscgr  36660  linecgr  36661  btwnconn1lem4  36670  btwnconn1lem5  36671  btwnconn1lem6  36672  btwnconn1lem8  36674  btwnconn1lem11  36677  seglecgr12  36691  colinbtwnle  36698  lshpkrlem6  39988  ps-2c  40401  pmodlem1  40719  pmodlem2  40720  dalawlem4  40747  dalawlem9  40752  4atexlemc  40942  cdleme11l  41142  cdleme15c  41149  cdleme16  41158  cdleme19e  41180  cdleme20l2  41194  cdleme20l  41195  cdleme20m  41196  cdleme20  41197  cdleme21d  41203  cdleme21e  41204  cdleme26ee  41233  cdleme26eALTN  41234  cdleme27a  41240  cdleme28b  41244  cdleme28c  41245  cdleme36m  41334  cdlemg12  41523  cdlemg16ALTN  41531  cdlemg17iqN  41547  cdlemg18c  41553  cdlemg19  41557  cdlemg21  41559  cdlemg28  41577  cdlemk11  41722  cdlemk12  41723  cdlemk16a  41729  cdlemk16  41730  cdlemk18  41741  cdlemk19  41742  cdlemk11u  41744  cdlemk12u  41745  cdlemk21N  41746  cdlemk20  41747  cdlemkoatnle-2N  41748  cdlemk13-2N  41749  cdlemkole-2N  41750  cdlemk14-2N  41751  cdlemk15-2N  41752  cdlemk16-2N  41753  cdlemk17-2N  41754  cdlemk18-2N  41759  cdlemk19-2N  41760  cdlemk7u-2N  41761  cdlemk11u-2N  41762  cdlemk12u-2N  41763  cdlemk22  41766  cdlemk30  41767  cdlemk23-3  41775  cdlemk26b-3  41778  cdlemk26-3  41779  cdlemk27-3  41780  cdlemk11ta  41802  cdlemk47  41822  dia2dimlem1  41937