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  29069  ofscom  36205  cgrextend  36206  segconeq  36208  ifscgr  36242  cgrsub  36243  btwnxfr  36254  fscgr  36278  linecgr  36279  btwnconn1lem4  36288  btwnconn1lem5  36289  btwnconn1lem6  36290  btwnconn1lem8  36292  btwnconn1lem11  36295  seglecgr12  36309  colinbtwnle  36316  lshpkrlem6  39575  ps-2c  39988  pmodlem1  40306  pmodlem2  40307  dalawlem4  40334  dalawlem9  40339  4atexlemc  40529  cdleme11l  40729  cdleme15c  40736  cdleme16  40745  cdleme19e  40767  cdleme20l2  40781  cdleme20l  40782  cdleme20m  40783  cdleme20  40784  cdleme21d  40790  cdleme21e  40791  cdleme26ee  40820  cdleme26eALTN  40821  cdleme27a  40827  cdleme28b  40831  cdleme28c  40832  cdleme36m  40921  cdlemg12  41110  cdlemg16ALTN  41118  cdlemg17iqN  41134  cdlemg18c  41140  cdlemg19  41144  cdlemg21  41146  cdlemg28  41164  cdlemk11  41309  cdlemk12  41310  cdlemk16a  41316  cdlemk16  41317  cdlemk18  41328  cdlemk19  41329  cdlemk11u  41331  cdlemk12u  41332  cdlemk21N  41333  cdlemk20  41334  cdlemkoatnle-2N  41335  cdlemk13-2N  41336  cdlemkole-2N  41337  cdlemk14-2N  41338  cdlemk15-2N  41339  cdlemk16-2N  41340  cdlemk17-2N  41341  cdlemk18-2N  41346  cdlemk19-2N  41347  cdlemk7u-2N  41348  cdlemk11u-2N  41349  cdlemk12u-2N  41350  cdlemk22  41353  cdlemk30  41354  cdlemk23-3  41362  cdlemk26b-3  41365  cdlemk26-3  41366  cdlemk27-3  41367  cdlemk11ta  41389  cdlemk47  41409  dia2dimlem1  41524