Theorem syl333anc 1350

Description: A syllogism inference combined with contraction. (Contributed by NM, 10-Mar-2012.)

Hypotheses

Ref	Expression
syl12anc.1	⊢ (𝜑 → 𝜓)
syl12anc.2	⊢ (𝜑 → 𝜒)
syl12anc.3	⊢ (𝜑 → 𝜃)
syl22anc.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		syl12anc.1	. 2 ⊢ (𝜑 → 𝜓)
2		syl12anc.2	. 2 ⊢ (𝜑 → 𝜒)
3		syl12anc.3	. 2 ⊢ (𝜑 → 𝜃)
4		syl22anc.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 1235	. 2 ⊢ (𝜑 → (𝜎 ∧ 𝜌 ∧ 𝜇))
11		syl333anc.10	. 2 ⊢ (((𝜓 ∧ 𝜒 ∧ 𝜃) ∧ (𝜏 ∧ 𝜂 ∧ 𝜁) ∧ (𝜎 ∧ 𝜌 ∧ 𝜇)) → 𝜆)
12	1, 2, 3, 4, 5, 6, 10, 11	syl331anc 1343	1 ⊢ (𝜑 → 𝜆)

Syntax hints:   → wi 4   ∧ w3a 1031

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 196  df-an 385  df-3an 1033

This theorem is referenced by:  eengtrkg  25665  ofscom  31284  cgrextend  31285  segconeq  31287  ifscgr  31321  cgrsub  31322  btwnxfr  31333  fscgr  31357  linecgr  31358  btwnconn1lem4  31367  btwnconn1lem5  31368  btwnconn1lem6  31369  btwnconn1lem8  31371  btwnconn1lem11  31374  seglecgr12  31388  colinbtwnle  31395  lshpkrlem6  33420  ps-2c  33832  pmodlem1  34150  pmodlem2  34151  dalawlem4  34178  dalawlem9  34183  4atexlemc  34373  cdleme11l  34574  cdleme15c  34581  cdleme16  34590  cdleme19e  34613  cdleme20l2  34627  cdleme20l  34628  cdleme20m  34629  cdleme20  34630  cdleme21d  34636  cdleme21e  34637  cdleme26ee  34666  cdleme26eALTN  34667  cdleme27a  34673  cdleme28b  34677  cdleme28c  34678  cdleme36m  34767  cdlemg12  34956  cdlemg16ALTN  34964  cdlemg17iqN  34980  cdlemg18c  34986  cdlemg19  34990  cdlemg21  34992  cdlemg28  35010  cdlemk11  35155  cdlemk12  35156  cdlemk16a  35162  cdlemk16  35163  cdlemk18  35174  cdlemk19  35175  cdlemk11u  35177  cdlemk12u  35178  cdlemk21N  35179  cdlemk20  35180  cdlemkoatnle-2N  35181  cdlemk13-2N  35182  cdlemkole-2N  35183  cdlemk14-2N  35184  cdlemk15-2N  35185  cdlemk16-2N  35186  cdlemk17-2N  35187  cdlemk18-2N  35192  cdlemk19-2N  35193  cdlemk7u-2N  35194  cdlemk11u-2N  35195  cdlemk12u-2N  35196  cdlemk22  35199  cdlemk30  35200  cdlemk23-3  35208  cdlemk26b-3  35211  cdlemk26-3  35212  cdlemk27-3  35213  cdlemk11ta  35235  cdlemk47  35255  dia2dimlem1  35371