Theorem syl333anc 1402

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 1395	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 206  df-an 397  df-3an 1089

This theorem is referenced by:  eengtrkg  28282  ofscom  35048  cgrextend  35049  segconeq  35051  ifscgr  35085  cgrsub  35086  btwnxfr  35097  fscgr  35121  linecgr  35122  btwnconn1lem4  35131  btwnconn1lem5  35132  btwnconn1lem6  35133  btwnconn1lem8  35135  btwnconn1lem11  35138  seglecgr12  35152  colinbtwnle  35159  lshpkrlem6  38071  ps-2c  38485  pmodlem1  38803  pmodlem2  38804  dalawlem4  38831  dalawlem9  38836  4atexlemc  39026  cdleme11l  39226  cdleme15c  39233  cdleme16  39242  cdleme19e  39264  cdleme20l2  39278  cdleme20l  39279  cdleme20m  39280  cdleme20  39281  cdleme21d  39287  cdleme21e  39288  cdleme26ee  39317  cdleme26eALTN  39318  cdleme27a  39324  cdleme28b  39328  cdleme28c  39329  cdleme36m  39418  cdlemg12  39607  cdlemg16ALTN  39615  cdlemg17iqN  39631  cdlemg18c  39637  cdlemg19  39641  cdlemg21  39643  cdlemg28  39661  cdlemk11  39806  cdlemk12  39807  cdlemk16a  39813  cdlemk16  39814  cdlemk18  39825  cdlemk19  39826  cdlemk11u  39828  cdlemk12u  39829  cdlemk21N  39830  cdlemk20  39831  cdlemkoatnle-2N  39832  cdlemk13-2N  39833  cdlemkole-2N  39834  cdlemk14-2N  39835  cdlemk15-2N  39836  cdlemk16-2N  39837  cdlemk17-2N  39838  cdlemk18-2N  39843  cdlemk19-2N  39844  cdlemk7u-2N  39845  cdlemk11u-2N  39846  cdlemk12u-2N  39847  cdlemk22  39850  cdlemk30  39851  cdlemk23-3  39859  cdlemk26b-3  39862  cdlemk26-3  39863  cdlemk27-3  39864  cdlemk11ta  39886  cdlemk47  39906  dia2dimlem1  40021