Theorem syl333anc 1420

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

Syntax hints:   → wi 4   ∧ w3a 1097

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 400  df-3an 1099

This theorem is referenced by:  eengtrkg  29144  ofscom  36318  cgrextend  36319  segconeq  36321  ifscgr  36355  cgrsub  36356  btwnxfr  36367  fscgr  36391  linecgr  36392  btwnconn1lem4  36401  btwnconn1lem5  36402  btwnconn1lem6  36403  btwnconn1lem8  36405  btwnconn1lem11  36408  seglecgr12  36422  colinbtwnle  36429  lshpkrlem6  39700  ps-2c  40113  pmodlem1  40431  pmodlem2  40432  dalawlem4  40459  dalawlem9  40464  4atexlemc  40654  cdleme11l  40854  cdleme15c  40861  cdleme16  40870  cdleme19e  40892  cdleme20l2  40906  cdleme20l  40907  cdleme20m  40908  cdleme20  40909  cdleme21d  40915  cdleme21e  40916  cdleme26ee  40945  cdleme26eALTN  40946  cdleme27a  40952  cdleme28b  40956  cdleme28c  40957  cdleme36m  41046  cdlemg12  41235  cdlemg16ALTN  41243  cdlemg17iqN  41259  cdlemg18c  41265  cdlemg19  41269  cdlemg21  41271  cdlemg28  41289  cdlemk11  41434  cdlemk12  41435  cdlemk16a  41441  cdlemk16  41442  cdlemk18  41453  cdlemk19  41454  cdlemk11u  41456  cdlemk12u  41457  cdlemk21N  41458  cdlemk20  41459  cdlemkoatnle-2N  41460  cdlemk13-2N  41461  cdlemkole-2N  41462  cdlemk14-2N  41463  cdlemk15-2N  41464  cdlemk16-2N  41465  cdlemk17-2N  41466  cdlemk18-2N  41471  cdlemk19-2N  41472  cdlemk7u-2N  41473  cdlemk11u-2N  41474  cdlemk12u-2N  41475  cdlemk22  41478  cdlemk30  41479  cdlemk23-3  41487  cdlemk26b-3  41490  cdlemk26-3  41491  cdlemk27-3  41492  cdlemk11ta  41514  cdlemk47  41534  dia2dimlem1  41649