Theorem syl333anc 1427

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

Syntax hints:   → wi 4   ∧ w3a 1101

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 210  df-an 401  df-3an 1103

This theorem is referenced by:  eengtrkg  29273  ofscom  36394  cgrextend  36395  segconeq  36397  ifscgr  36431  cgrsub  36432  btwnxfr  36443  fscgr  36467  linecgr  36468  btwnconn1lem4  36477  btwnconn1lem5  36478  btwnconn1lem6  36479  btwnconn1lem8  36481  btwnconn1lem11  36484  seglecgr12  36498  colinbtwnle  36505  lshpkrlem6  39774  ps-2c  40187  pmodlem1  40505  pmodlem2  40506  dalawlem4  40533  dalawlem9  40538  4atexlemc  40728  cdleme11l  40928  cdleme15c  40935  cdleme16  40944  cdleme19e  40966  cdleme20l2  40980  cdleme20l  40981  cdleme20m  40982  cdleme20  40983  cdleme21d  40989  cdleme21e  40990  cdleme26ee  41019  cdleme26eALTN  41020  cdleme27a  41026  cdleme28b  41030  cdleme28c  41031  cdleme36m  41120  cdlemg12  41309  cdlemg16ALTN  41317  cdlemg17iqN  41333  cdlemg18c  41339  cdlemg19  41343  cdlemg21  41345  cdlemg28  41363  cdlemk11  41508  cdlemk12  41509  cdlemk16a  41515  cdlemk16  41516  cdlemk18  41527  cdlemk19  41528  cdlemk11u  41530  cdlemk12u  41531  cdlemk21N  41532  cdlemk20  41533  cdlemkoatnle-2N  41534  cdlemk13-2N  41535  cdlemkole-2N  41536  cdlemk14-2N  41537  cdlemk15-2N  41538  cdlemk16-2N  41539  cdlemk17-2N  41540  cdlemk18-2N  41545  cdlemk19-2N  41546  cdlemk7u-2N  41547  cdlemk11u-2N  41548  cdlemk12u-2N  41549  cdlemk22  41552  cdlemk30  41553  cdlemk23-3  41561  cdlemk26b-3  41564  cdlemk26-3  41565  cdlemk27-3  41566  cdlemk11ta  41588  cdlemk47  41608  dia2dimlem1  41723