Theorem syl333anc 1400

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

Syntax hints:   → wi 4   ∧ w3a 1085

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 396  df-3an 1087

This theorem is referenced by:  eengtrkg  27335  ofscom  34288  cgrextend  34289  segconeq  34291  ifscgr  34325  cgrsub  34326  btwnxfr  34337  fscgr  34361  linecgr  34362  btwnconn1lem4  34371  btwnconn1lem5  34372  btwnconn1lem6  34373  btwnconn1lem8  34375  btwnconn1lem11  34378  seglecgr12  34392  colinbtwnle  34399  lshpkrlem6  37108  ps-2c  37521  pmodlem1  37839  pmodlem2  37840  dalawlem4  37867  dalawlem9  37872  4atexlemc  38062  cdleme11l  38262  cdleme15c  38269  cdleme16  38278  cdleme19e  38300  cdleme20l2  38314  cdleme20l  38315  cdleme20m  38316  cdleme20  38317  cdleme21d  38323  cdleme21e  38324  cdleme26ee  38353  cdleme26eALTN  38354  cdleme27a  38360  cdleme28b  38364  cdleme28c  38365  cdleme36m  38454  cdlemg12  38643  cdlemg16ALTN  38651  cdlemg17iqN  38667  cdlemg18c  38673  cdlemg19  38677  cdlemg21  38679  cdlemg28  38697  cdlemk11  38842  cdlemk12  38843  cdlemk16a  38849  cdlemk16  38850  cdlemk18  38861  cdlemk19  38862  cdlemk11u  38864  cdlemk12u  38865  cdlemk21N  38866  cdlemk20  38867  cdlemkoatnle-2N  38868  cdlemk13-2N  38869  cdlemkole-2N  38870  cdlemk14-2N  38871  cdlemk15-2N  38872  cdlemk16-2N  38873  cdlemk17-2N  38874  cdlemk18-2N  38879  cdlemk19-2N  38880  cdlemk7u-2N  38881  cdlemk11u-2N  38882  cdlemk12u-2N  38883  cdlemk22  38886  cdlemk30  38887  cdlemk23-3  38895  cdlemk26b-3  38898  cdlemk26-3  38899  cdlemk27-3  38900  cdlemk11ta  38922  cdlemk47  38942  dia2dimlem1  39057