Theorem syl333anc 1404

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

Syntax hints:   → wi 4   ∧ w3a 1086

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 1088

This theorem is referenced by:  eengtrkg  28965  ofscom  36047  cgrextend  36048  segconeq  36050  ifscgr  36084  cgrsub  36085  btwnxfr  36096  fscgr  36120  linecgr  36121  btwnconn1lem4  36130  btwnconn1lem5  36131  btwnconn1lem6  36132  btwnconn1lem8  36134  btwnconn1lem11  36137  seglecgr12  36151  colinbtwnle  36158  lshpkrlem6  39160  ps-2c  39573  pmodlem1  39891  pmodlem2  39892  dalawlem4  39919  dalawlem9  39924  4atexlemc  40114  cdleme11l  40314  cdleme15c  40321  cdleme16  40330  cdleme19e  40352  cdleme20l2  40366  cdleme20l  40367  cdleme20m  40368  cdleme20  40369  cdleme21d  40375  cdleme21e  40376  cdleme26ee  40405  cdleme26eALTN  40406  cdleme27a  40412  cdleme28b  40416  cdleme28c  40417  cdleme36m  40506  cdlemg12  40695  cdlemg16ALTN  40703  cdlemg17iqN  40719  cdlemg18c  40725  cdlemg19  40729  cdlemg21  40731  cdlemg28  40749  cdlemk11  40894  cdlemk12  40895  cdlemk16a  40901  cdlemk16  40902  cdlemk18  40913  cdlemk19  40914  cdlemk11u  40916  cdlemk12u  40917  cdlemk21N  40918  cdlemk20  40919  cdlemkoatnle-2N  40920  cdlemk13-2N  40921  cdlemkole-2N  40922  cdlemk14-2N  40923  cdlemk15-2N  40924  cdlemk16-2N  40925  cdlemk17-2N  40926  cdlemk18-2N  40931  cdlemk19-2N  40932  cdlemk7u-2N  40933  cdlemk11u-2N  40934  cdlemk12u-2N  40935  cdlemk22  40938  cdlemk30  40939  cdlemk23-3  40947  cdlemk26b-3  40950  cdlemk26-3  40951  cdlemk27-3  40952  cdlemk11ta  40974  cdlemk47  40994  dia2dimlem1  41109