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  28913  ofscom  35995  cgrextend  35996  segconeq  35998  ifscgr  36032  cgrsub  36033  btwnxfr  36044  fscgr  36068  linecgr  36069  btwnconn1lem4  36078  btwnconn1lem5  36079  btwnconn1lem6  36080  btwnconn1lem8  36082  btwnconn1lem11  36085  seglecgr12  36099  colinbtwnle  36106  lshpkrlem6  39108  ps-2c  39522  pmodlem1  39840  pmodlem2  39841  dalawlem4  39868  dalawlem9  39873  4atexlemc  40063  cdleme11l  40263  cdleme15c  40270  cdleme16  40279  cdleme19e  40301  cdleme20l2  40315  cdleme20l  40316  cdleme20m  40317  cdleme20  40318  cdleme21d  40324  cdleme21e  40325  cdleme26ee  40354  cdleme26eALTN  40355  cdleme27a  40361  cdleme28b  40365  cdleme28c  40366  cdleme36m  40455  cdlemg12  40644  cdlemg16ALTN  40652  cdlemg17iqN  40668  cdlemg18c  40674  cdlemg19  40678  cdlemg21  40680  cdlemg28  40698  cdlemk11  40843  cdlemk12  40844  cdlemk16a  40850  cdlemk16  40851  cdlemk18  40862  cdlemk19  40863  cdlemk11u  40865  cdlemk12u  40866  cdlemk21N  40867  cdlemk20  40868  cdlemkoatnle-2N  40869  cdlemk13-2N  40870  cdlemkole-2N  40871  cdlemk14-2N  40872  cdlemk15-2N  40873  cdlemk16-2N  40874  cdlemk17-2N  40875  cdlemk18-2N  40880  cdlemk19-2N  40881  cdlemk7u-2N  40882  cdlemk11u-2N  40883  cdlemk12u-2N  40884  cdlemk22  40887  cdlemk30  40888  cdlemk23-3  40896  cdlemk26b-3  40899  cdlemk26-3  40900  cdlemk27-3  40901  cdlemk11ta  40923  cdlemk47  40943  dia2dimlem1  41058