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  26774  ofscom  33470  cgrextend  33471  segconeq  33473  ifscgr  33507  cgrsub  33508  btwnxfr  33519  fscgr  33543  linecgr  33544  btwnconn1lem4  33553  btwnconn1lem5  33554  btwnconn1lem6  33555  btwnconn1lem8  33557  btwnconn1lem11  33560  seglecgr12  33574  colinbtwnle  33581  lshpkrlem6  36253  ps-2c  36666  pmodlem1  36984  pmodlem2  36985  dalawlem4  37012  dalawlem9  37017  4atexlemc  37207  cdleme11l  37407  cdleme15c  37414  cdleme16  37423  cdleme19e  37445  cdleme20l2  37459  cdleme20l  37460  cdleme20m  37461  cdleme20  37462  cdleme21d  37468  cdleme21e  37469  cdleme26ee  37498  cdleme26eALTN  37499  cdleme27a  37505  cdleme28b  37509  cdleme28c  37510  cdleme36m  37599  cdlemg12  37788  cdlemg16ALTN  37796  cdlemg17iqN  37812  cdlemg18c  37818  cdlemg19  37822  cdlemg21  37824  cdlemg28  37842  cdlemk11  37987  cdlemk12  37988  cdlemk16a  37994  cdlemk16  37995  cdlemk18  38006  cdlemk19  38007  cdlemk11u  38009  cdlemk12u  38010  cdlemk21N  38011  cdlemk20  38012  cdlemkoatnle-2N  38013  cdlemk13-2N  38014  cdlemkole-2N  38015  cdlemk14-2N  38016  cdlemk15-2N  38017  cdlemk16-2N  38018  cdlemk17-2N  38019  cdlemk18-2N  38024  cdlemk19-2N  38025  cdlemk7u-2N  38026  cdlemk11u-2N  38027  cdlemk12u-2N  38028  cdlemk22  38031  cdlemk30  38032  cdlemk23-3  38040  cdlemk26b-3  38043  cdlemk26-3  38044  cdlemk27-3  38045  cdlemk11ta  38067  cdlemk47  38087  dia2dimlem1  38202