Theorem syl333anc 1403

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 1396	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  28932  ofscom  35983  cgrextend  35984  segconeq  35986  ifscgr  36020  cgrsub  36021  btwnxfr  36032  fscgr  36056  linecgr  36057  btwnconn1lem4  36066  btwnconn1lem5  36067  btwnconn1lem6  36068  btwnconn1lem8  36070  btwnconn1lem11  36073  seglecgr12  36087  colinbtwnle  36094  lshpkrlem6  39091  ps-2c  39505  pmodlem1  39823  pmodlem2  39824  dalawlem4  39851  dalawlem9  39856  4atexlemc  40046  cdleme11l  40246  cdleme15c  40253  cdleme16  40262  cdleme19e  40284  cdleme20l2  40298  cdleme20l  40299  cdleme20m  40300  cdleme20  40301  cdleme21d  40307  cdleme21e  40308  cdleme26ee  40337  cdleme26eALTN  40338  cdleme27a  40344  cdleme28b  40348  cdleme28c  40349  cdleme36m  40438  cdlemg12  40627  cdlemg16ALTN  40635  cdlemg17iqN  40651  cdlemg18c  40657  cdlemg19  40661  cdlemg21  40663  cdlemg28  40681  cdlemk11  40826  cdlemk12  40827  cdlemk16a  40833  cdlemk16  40834  cdlemk18  40845  cdlemk19  40846  cdlemk11u  40848  cdlemk12u  40849  cdlemk21N  40850  cdlemk20  40851  cdlemkoatnle-2N  40852  cdlemk13-2N  40853  cdlemkole-2N  40854  cdlemk14-2N  40855  cdlemk15-2N  40856  cdlemk16-2N  40857  cdlemk17-2N  40858  cdlemk18-2N  40863  cdlemk19-2N  40864  cdlemk7u-2N  40865  cdlemk11u-2N  40866  cdlemk12u-2N  40867  cdlemk22  40870  cdlemk30  40871  cdlemk23-3  40879  cdlemk26b-3  40882  cdlemk26-3  40883  cdlemk27-3  40884  cdlemk11ta  40906  cdlemk47  40926  dia2dimlem1  41041