Theorem syl333anc 1405

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

Syntax hints:   → wi 4   ∧ w3a 1087

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 207  df-an 396  df-3an 1089

This theorem is referenced by:  eengtrkg  29043  ofscom  36195  cgrextend  36196  segconeq  36198  ifscgr  36232  cgrsub  36233  btwnxfr  36244  fscgr  36268  linecgr  36269  btwnconn1lem4  36278  btwnconn1lem5  36279  btwnconn1lem6  36280  btwnconn1lem8  36282  btwnconn1lem11  36285  seglecgr12  36299  colinbtwnle  36306  lshpkrlem6  39552  ps-2c  39965  pmodlem1  40283  pmodlem2  40284  dalawlem4  40311  dalawlem9  40316  4atexlemc  40506  cdleme11l  40706  cdleme15c  40713  cdleme16  40722  cdleme19e  40744  cdleme20l2  40758  cdleme20l  40759  cdleme20m  40760  cdleme20  40761  cdleme21d  40767  cdleme21e  40768  cdleme26ee  40797  cdleme26eALTN  40798  cdleme27a  40804  cdleme28b  40808  cdleme28c  40809  cdleme36m  40898  cdlemg12  41087  cdlemg16ALTN  41095  cdlemg17iqN  41111  cdlemg18c  41117  cdlemg19  41121  cdlemg21  41123  cdlemg28  41141  cdlemk11  41286  cdlemk12  41287  cdlemk16a  41293  cdlemk16  41294  cdlemk18  41305  cdlemk19  41306  cdlemk11u  41308  cdlemk12u  41309  cdlemk21N  41310  cdlemk20  41311  cdlemkoatnle-2N  41312  cdlemk13-2N  41313  cdlemkole-2N  41314  cdlemk14-2N  41315  cdlemk15-2N  41316  cdlemk16-2N  41317  cdlemk17-2N  41318  cdlemk18-2N  41323  cdlemk19-2N  41324  cdlemk7u-2N  41325  cdlemk11u-2N  41326  cdlemk12u-2N  41327  cdlemk22  41330  cdlemk30  41331  cdlemk23-3  41339  cdlemk26b-3  41342  cdlemk26-3  41343  cdlemk27-3  41344  cdlemk11ta  41366  cdlemk47  41386  dia2dimlem1  41501