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  29557  ofscom  36752  cgrextend  36753  segconeq  36755  ifscgr  36789  cgrsub  36790  btwnxfr  36801  fscgr  36825  linecgr  36826  btwnconn1lem4  36835  btwnconn1lem5  36836  btwnconn1lem6  36837  btwnconn1lem8  36839  btwnconn1lem11  36842  seglecgr12  36856  colinbtwnle  36863  lshpkrlem6  40152  ps-2c  40565  pmodlem1  40883  pmodlem2  40884  dalawlem4  40911  dalawlem9  40916  4atexlemc  41106  cdleme11l  41306  cdleme15c  41313  cdleme16  41322  cdleme19e  41344  cdleme20l2  41358  cdleme20l  41359  cdleme20m  41360  cdleme20  41361  cdleme21d  41367  cdleme21e  41368  cdleme26ee  41397  cdleme26eALTN  41398  cdleme27a  41404  cdleme28b  41408  cdleme28c  41409  cdleme36m  41498  cdlemg12  41687  cdlemg16ALTN  41695  cdlemg17iqN  41711  cdlemg18c  41717  cdlemg19  41721  cdlemg21  41723  cdlemg28  41741  cdlemk11  41886  cdlemk12  41887  cdlemk16a  41893  cdlemk16  41894  cdlemk18  41905  cdlemk19  41906  cdlemk11u  41908  cdlemk12u  41909  cdlemk21N  41910  cdlemk20  41911  cdlemkoatnle-2N  41912  cdlemk13-2N  41913  cdlemkole-2N  41914  cdlemk14-2N  41915  cdlemk15-2N  41916  cdlemk16-2N  41917  cdlemk17-2N  41918  cdlemk18-2N  41923  cdlemk19-2N  41924  cdlemk7u-2N  41925  cdlemk11u-2N  41926  cdlemk12u-2N  41927  cdlemk22  41930  cdlemk30  41931  cdlemk23-3  41939  cdlemk26b-3  41942  cdlemk26-3  41943  cdlemk27-3  41944  cdlemk11ta  41966  cdlemk47  41986  dia2dimlem1  42101