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  29059  ofscom  36201  cgrextend  36202  segconeq  36204  ifscgr  36238  cgrsub  36239  btwnxfr  36250  fscgr  36274  linecgr  36275  btwnconn1lem4  36284  btwnconn1lem5  36285  btwnconn1lem6  36286  btwnconn1lem8  36288  btwnconn1lem11  36291  seglecgr12  36305  colinbtwnle  36312  lshpkrlem6  39375  ps-2c  39788  pmodlem1  40106  pmodlem2  40107  dalawlem4  40134  dalawlem9  40139  4atexlemc  40329  cdleme11l  40529  cdleme15c  40536  cdleme16  40545  cdleme19e  40567  cdleme20l2  40581  cdleme20l  40582  cdleme20m  40583  cdleme20  40584  cdleme21d  40590  cdleme21e  40591  cdleme26ee  40620  cdleme26eALTN  40621  cdleme27a  40627  cdleme28b  40631  cdleme28c  40632  cdleme36m  40721  cdlemg12  40910  cdlemg16ALTN  40918  cdlemg17iqN  40934  cdlemg18c  40940  cdlemg19  40944  cdlemg21  40946  cdlemg28  40964  cdlemk11  41109  cdlemk12  41110  cdlemk16a  41116  cdlemk16  41117  cdlemk18  41128  cdlemk19  41129  cdlemk11u  41131  cdlemk12u  41132  cdlemk21N  41133  cdlemk20  41134  cdlemkoatnle-2N  41135  cdlemk13-2N  41136  cdlemkole-2N  41137  cdlemk14-2N  41138  cdlemk15-2N  41139  cdlemk16-2N  41140  cdlemk17-2N  41141  cdlemk18-2N  41146  cdlemk19-2N  41147  cdlemk7u-2N  41148  cdlemk11u-2N  41149  cdlemk12u-2N  41150  cdlemk22  41153  cdlemk30  41154  cdlemk23-3  41162  cdlemk26b-3  41165  cdlemk26-3  41166  cdlemk27-3  41167  cdlemk11ta  41189  cdlemk47  41209  dia2dimlem1  41324