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  28968  ofscom  36074  cgrextend  36075  segconeq  36077  ifscgr  36111  cgrsub  36112  btwnxfr  36123  fscgr  36147  linecgr  36148  btwnconn1lem4  36157  btwnconn1lem5  36158  btwnconn1lem6  36159  btwnconn1lem8  36161  btwnconn1lem11  36164  seglecgr12  36178  colinbtwnle  36185  lshpkrlem6  39237  ps-2c  39650  pmodlem1  39968  pmodlem2  39969  dalawlem4  39996  dalawlem9  40001  4atexlemc  40191  cdleme11l  40391  cdleme15c  40398  cdleme16  40407  cdleme19e  40429  cdleme20l2  40443  cdleme20l  40444  cdleme20m  40445  cdleme20  40446  cdleme21d  40452  cdleme21e  40453  cdleme26ee  40482  cdleme26eALTN  40483  cdleme27a  40489  cdleme28b  40493  cdleme28c  40494  cdleme36m  40583  cdlemg12  40772  cdlemg16ALTN  40780  cdlemg17iqN  40796  cdlemg18c  40802  cdlemg19  40806  cdlemg21  40808  cdlemg28  40826  cdlemk11  40971  cdlemk12  40972  cdlemk16a  40978  cdlemk16  40979  cdlemk18  40990  cdlemk19  40991  cdlemk11u  40993  cdlemk12u  40994  cdlemk21N  40995  cdlemk20  40996  cdlemkoatnle-2N  40997  cdlemk13-2N  40998  cdlemkole-2N  40999  cdlemk14-2N  41000  cdlemk15-2N  41001  cdlemk16-2N  41002  cdlemk17-2N  41003  cdlemk18-2N  41008  cdlemk19-2N  41009  cdlemk7u-2N  41010  cdlemk11u-2N  41011  cdlemk12u-2N  41012  cdlemk22  41015  cdlemk30  41016  cdlemk23-3  41024  cdlemk26b-3  41027  cdlemk26-3  41028  cdlemk27-3  41029  cdlemk11ta  41051  cdlemk47  41071  dia2dimlem1  41186