Theorem syl333anc 1403

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

Syntax hints:   → wi 4   ∧ w3a 1088

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 210  df-an 400  df-3an 1090

This theorem is referenced by:  eengtrkg  26932  ofscom  33947  cgrextend  33948  segconeq  33950  ifscgr  33984  cgrsub  33985  btwnxfr  33996  fscgr  34020  linecgr  34021  btwnconn1lem4  34030  btwnconn1lem5  34031  btwnconn1lem6  34032  btwnconn1lem8  34034  btwnconn1lem11  34037  seglecgr12  34051  colinbtwnle  34058  lshpkrlem6  36752  ps-2c  37165  pmodlem1  37483  pmodlem2  37484  dalawlem4  37511  dalawlem9  37516  4atexlemc  37706  cdleme11l  37906  cdleme15c  37913  cdleme16  37922  cdleme19e  37944  cdleme20l2  37958  cdleme20l  37959  cdleme20m  37960  cdleme20  37961  cdleme21d  37967  cdleme21e  37968  cdleme26ee  37997  cdleme26eALTN  37998  cdleme27a  38004  cdleme28b  38008  cdleme28c  38009  cdleme36m  38098  cdlemg12  38287  cdlemg16ALTN  38295  cdlemg17iqN  38311  cdlemg18c  38317  cdlemg19  38321  cdlemg21  38323  cdlemg28  38341  cdlemk11  38486  cdlemk12  38487  cdlemk16a  38493  cdlemk16  38494  cdlemk18  38505  cdlemk19  38506  cdlemk11u  38508  cdlemk12u  38509  cdlemk21N  38510  cdlemk20  38511  cdlemkoatnle-2N  38512  cdlemk13-2N  38513  cdlemkole-2N  38514  cdlemk14-2N  38515  cdlemk15-2N  38516  cdlemk16-2N  38517  cdlemk17-2N  38518  cdlemk18-2N  38523  cdlemk19-2N  38524  cdlemk7u-2N  38525  cdlemk11u-2N  38526  cdlemk12u-2N  38527  cdlemk22  38530  cdlemk30  38531  cdlemk23-3  38539  cdlemk26b-3  38542  cdlemk26-3  38543  cdlemk27-3  38544  cdlemk11ta  38566  cdlemk47  38586  dia2dimlem1  38701