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 398  df-3an 1089

This theorem is referenced by:  eengtrkg  27399  ofscom  34354  cgrextend  34355  segconeq  34357  ifscgr  34391  cgrsub  34392  btwnxfr  34403  fscgr  34427  linecgr  34428  btwnconn1lem4  34437  btwnconn1lem5  34438  btwnconn1lem6  34439  btwnconn1lem8  34441  btwnconn1lem11  34444  seglecgr12  34458  colinbtwnle  34465  lshpkrlem6  37171  ps-2c  37584  pmodlem1  37902  pmodlem2  37903  dalawlem4  37930  dalawlem9  37935  4atexlemc  38125  cdleme11l  38325  cdleme15c  38332  cdleme16  38341  cdleme19e  38363  cdleme20l2  38377  cdleme20l  38378  cdleme20m  38379  cdleme20  38380  cdleme21d  38386  cdleme21e  38387  cdleme26ee  38416  cdleme26eALTN  38417  cdleme27a  38423  cdleme28b  38427  cdleme28c  38428  cdleme36m  38517  cdlemg12  38706  cdlemg16ALTN  38714  cdlemg17iqN  38730  cdlemg18c  38736  cdlemg19  38740  cdlemg21  38742  cdlemg28  38760  cdlemk11  38905  cdlemk12  38906  cdlemk16a  38912  cdlemk16  38913  cdlemk18  38924  cdlemk19  38925  cdlemk11u  38927  cdlemk12u  38928  cdlemk21N  38929  cdlemk20  38930  cdlemkoatnle-2N  38931  cdlemk13-2N  38932  cdlemkole-2N  38933  cdlemk14-2N  38934  cdlemk15-2N  38935  cdlemk16-2N  38936  cdlemk17-2N  38937  cdlemk18-2N  38942  cdlemk19-2N  38943  cdlemk7u-2N  38944  cdlemk11u-2N  38945  cdlemk12u-2N  38946  cdlemk22  38949  cdlemk30  38950  cdlemk23-3  38958  cdlemk26b-3  38961  cdlemk26-3  38962  cdlemk27-3  38963  cdlemk11ta  38985  cdlemk47  39005  dia2dimlem1  39120