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  29055  ofscom  36189  cgrextend  36190  segconeq  36192  ifscgr  36226  cgrsub  36227  btwnxfr  36238  fscgr  36262  linecgr  36263  btwnconn1lem4  36272  btwnconn1lem5  36273  btwnconn1lem6  36274  btwnconn1lem8  36276  btwnconn1lem11  36279  seglecgr12  36293  colinbtwnle  36300  lshpkrlem6  39561  ps-2c  39974  pmodlem1  40292  pmodlem2  40293  dalawlem4  40320  dalawlem9  40325  4atexlemc  40515  cdleme11l  40715  cdleme15c  40722  cdleme16  40731  cdleme19e  40753  cdleme20l2  40767  cdleme20l  40768  cdleme20m  40769  cdleme20  40770  cdleme21d  40776  cdleme21e  40777  cdleme26ee  40806  cdleme26eALTN  40807  cdleme27a  40813  cdleme28b  40817  cdleme28c  40818  cdleme36m  40907  cdlemg12  41096  cdlemg16ALTN  41104  cdlemg17iqN  41120  cdlemg18c  41126  cdlemg19  41130  cdlemg21  41132  cdlemg28  41150  cdlemk11  41295  cdlemk12  41296  cdlemk16a  41302  cdlemk16  41303  cdlemk18  41314  cdlemk19  41315  cdlemk11u  41317  cdlemk12u  41318  cdlemk21N  41319  cdlemk20  41320  cdlemkoatnle-2N  41321  cdlemk13-2N  41322  cdlemkole-2N  41323  cdlemk14-2N  41324  cdlemk15-2N  41325  cdlemk16-2N  41326  cdlemk17-2N  41327  cdlemk18-2N  41332  cdlemk19-2N  41333  cdlemk7u-2N  41334  cdlemk11u-2N  41335  cdlemk12u-2N  41336  cdlemk22  41339  cdlemk30  41340  cdlemk23-3  41348  cdlemk26b-3  41351  cdlemk26-3  41352  cdlemk27-3  41353  cdlemk11ta  41375  cdlemk47  41395  dia2dimlem1  41510