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  28920  ofscom  36002  cgrextend  36003  segconeq  36005  ifscgr  36039  cgrsub  36040  btwnxfr  36051  fscgr  36075  linecgr  36076  btwnconn1lem4  36085  btwnconn1lem5  36086  btwnconn1lem6  36087  btwnconn1lem8  36089  btwnconn1lem11  36092  seglecgr12  36106  colinbtwnle  36113  lshpkrlem6  39115  ps-2c  39529  pmodlem1  39847  pmodlem2  39848  dalawlem4  39875  dalawlem9  39880  4atexlemc  40070  cdleme11l  40270  cdleme15c  40277  cdleme16  40286  cdleme19e  40308  cdleme20l2  40322  cdleme20l  40323  cdleme20m  40324  cdleme20  40325  cdleme21d  40331  cdleme21e  40332  cdleme26ee  40361  cdleme26eALTN  40362  cdleme27a  40368  cdleme28b  40372  cdleme28c  40373  cdleme36m  40462  cdlemg12  40651  cdlemg16ALTN  40659  cdlemg17iqN  40675  cdlemg18c  40681  cdlemg19  40685  cdlemg21  40687  cdlemg28  40705  cdlemk11  40850  cdlemk12  40851  cdlemk16a  40857  cdlemk16  40858  cdlemk18  40869  cdlemk19  40870  cdlemk11u  40872  cdlemk12u  40873  cdlemk21N  40874  cdlemk20  40875  cdlemkoatnle-2N  40876  cdlemk13-2N  40877  cdlemkole-2N  40878  cdlemk14-2N  40879  cdlemk15-2N  40880  cdlemk16-2N  40881  cdlemk17-2N  40882  cdlemk18-2N  40887  cdlemk19-2N  40888  cdlemk7u-2N  40889  cdlemk11u-2N  40890  cdlemk12u-2N  40891  cdlemk22  40894  cdlemk30  40895  cdlemk23-3  40903  cdlemk26b-3  40906  cdlemk26-3  40907  cdlemk27-3  40908  cdlemk11ta  40930  cdlemk47  40950  dia2dimlem1  41065