Theorem syl333anc 1398

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

Syntax hints:   → wi 4   ∧ w3a 1083

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 209  df-an 399  df-3an 1085

This theorem is referenced by:  eengtrkg  26771  ofscom  33468  cgrextend  33469  segconeq  33471  ifscgr  33505  cgrsub  33506  btwnxfr  33517  fscgr  33541  linecgr  33542  btwnconn1lem4  33551  btwnconn1lem5  33552  btwnconn1lem6  33553  btwnconn1lem8  33555  btwnconn1lem11  33558  seglecgr12  33572  colinbtwnle  33579  lshpkrlem6  36250  ps-2c  36663  pmodlem1  36981  pmodlem2  36982  dalawlem4  37009  dalawlem9  37014  4atexlemc  37204  cdleme11l  37404  cdleme15c  37411  cdleme16  37420  cdleme19e  37442  cdleme20l2  37456  cdleme20l  37457  cdleme20m  37458  cdleme20  37459  cdleme21d  37465  cdleme21e  37466  cdleme26ee  37495  cdleme26eALTN  37496  cdleme27a  37502  cdleme28b  37506  cdleme28c  37507  cdleme36m  37596  cdlemg12  37785  cdlemg16ALTN  37793  cdlemg17iqN  37809  cdlemg18c  37815  cdlemg19  37819  cdlemg21  37821  cdlemg28  37839  cdlemk11  37984  cdlemk12  37985  cdlemk16a  37991  cdlemk16  37992  cdlemk18  38003  cdlemk19  38004  cdlemk11u  38006  cdlemk12u  38007  cdlemk21N  38008  cdlemk20  38009  cdlemkoatnle-2N  38010  cdlemk13-2N  38011  cdlemkole-2N  38012  cdlemk14-2N  38013  cdlemk15-2N  38014  cdlemk16-2N  38015  cdlemk17-2N  38016  cdlemk18-2N  38021  cdlemk19-2N  38022  cdlemk7u-2N  38023  cdlemk11u-2N  38024  cdlemk12u-2N  38025  cdlemk22  38028  cdlemk30  38029  cdlemk23-3  38037  cdlemk26b-3  38040  cdlemk26-3  38041  cdlemk27-3  38042  cdlemk11ta  38064  cdlemk47  38084  dia2dimlem1  38199