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  29571  ofscom  36866  cgrextend  36867  segconeq  36869  ifscgr  36903  cgrsub  36904  btwnxfr  36915  fscgr  36939  linecgr  36940  btwnconn1lem4  36949  btwnconn1lem5  36950  btwnconn1lem6  36951  btwnconn1lem8  36953  btwnconn1lem11  36956  seglecgr12  36970  colinbtwnle  36977  lshpkrlem6  40279  ps-2c  40692  pmodlem1  41010  pmodlem2  41011  dalawlem4  41038  dalawlem9  41043  4atexlemc  41233  cdleme11l  41433  cdleme15c  41440  cdleme16  41449  cdleme19e  41471  cdleme20l2  41485  cdleme20l  41486  cdleme20m  41487  cdleme20  41488  cdleme21d  41494  cdleme21e  41495  cdleme26ee  41524  cdleme26eALTN  41525  cdleme27a  41531  cdleme28b  41535  cdleme28c  41536  cdleme36m  41625  cdlemg12  41814  cdlemg16ALTN  41822  cdlemg17iqN  41838  cdlemg18c  41844  cdlemg19  41848  cdlemg21  41850  cdlemg28  41868  cdlemk11  42013  cdlemk12  42014  cdlemk16a  42020  cdlemk16  42021  cdlemk18  42032  cdlemk19  42033  cdlemk11u  42035  cdlemk12u  42036  cdlemk21N  42037  cdlemk20  42038  cdlemkoatnle-2N  42039  cdlemk13-2N  42040  cdlemkole-2N  42041  cdlemk14-2N  42042  cdlemk15-2N  42043  cdlemk16-2N  42044  cdlemk17-2N  42045  cdlemk18-2N  42050  cdlemk19-2N  42051  cdlemk7u-2N  42052  cdlemk11u-2N  42053  cdlemk12u-2N  42054  cdlemk22  42057  cdlemk30  42058  cdlemk23-3  42066  cdlemk26b-3  42069  cdlemk26-3  42070  cdlemk27-3  42071  cdlemk11ta  42093  cdlemk47  42113  dia2dimlem1  42228