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

Syntax hints:   → wi 4   ∧ w3a 1087

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 1089

This theorem is referenced by:  eengtrkg  29001  ofscom  36008  cgrextend  36009  segconeq  36011  ifscgr  36045  cgrsub  36046  btwnxfr  36057  fscgr  36081  linecgr  36082  btwnconn1lem4  36091  btwnconn1lem5  36092  btwnconn1lem6  36093  btwnconn1lem8  36095  btwnconn1lem11  36098  seglecgr12  36112  colinbtwnle  36119  lshpkrlem6  39116  ps-2c  39530  pmodlem1  39848  pmodlem2  39849  dalawlem4  39876  dalawlem9  39881  4atexlemc  40071  cdleme11l  40271  cdleme15c  40278  cdleme16  40287  cdleme19e  40309  cdleme20l2  40323  cdleme20l  40324  cdleme20m  40325  cdleme20  40326  cdleme21d  40332  cdleme21e  40333  cdleme26ee  40362  cdleme26eALTN  40363  cdleme27a  40369  cdleme28b  40373  cdleme28c  40374  cdleme36m  40463  cdlemg12  40652  cdlemg16ALTN  40660  cdlemg17iqN  40676  cdlemg18c  40682  cdlemg19  40686  cdlemg21  40688  cdlemg28  40706  cdlemk11  40851  cdlemk12  40852  cdlemk16a  40858  cdlemk16  40859  cdlemk18  40870  cdlemk19  40871  cdlemk11u  40873  cdlemk12u  40874  cdlemk21N  40875  cdlemk20  40876  cdlemkoatnle-2N  40877  cdlemk13-2N  40878  cdlemkole-2N  40879  cdlemk14-2N  40880  cdlemk15-2N  40881  cdlemk16-2N  40882  cdlemk17-2N  40883  cdlemk18-2N  40888  cdlemk19-2N  40889  cdlemk7u-2N  40890  cdlemk11u-2N  40891  cdlemk12u-2N  40892  cdlemk22  40895  cdlemk30  40896  cdlemk23-3  40904  cdlemk26b-3  40907  cdlemk26-3  40908  cdlemk27-3  40909  cdlemk11ta  40931  cdlemk47  40951  dia2dimlem1  41066