Theorem syl333anc 1399

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

Syntax hints:   → wi 4   ∧ w3a 1084

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

This theorem is referenced by:  eengtrkg  26780  ofscom  33581  cgrextend  33582  segconeq  33584  ifscgr  33618  cgrsub  33619  btwnxfr  33630  fscgr  33654  linecgr  33655  btwnconn1lem4  33664  btwnconn1lem5  33665  btwnconn1lem6  33666  btwnconn1lem8  33668  btwnconn1lem11  33671  seglecgr12  33685  colinbtwnle  33692  lshpkrlem6  36411  ps-2c  36824  pmodlem1  37142  pmodlem2  37143  dalawlem4  37170  dalawlem9  37175  4atexlemc  37365  cdleme11l  37565  cdleme15c  37572  cdleme16  37581  cdleme19e  37603  cdleme20l2  37617  cdleme20l  37618  cdleme20m  37619  cdleme20  37620  cdleme21d  37626  cdleme21e  37627  cdleme26ee  37656  cdleme26eALTN  37657  cdleme27a  37663  cdleme28b  37667  cdleme28c  37668  cdleme36m  37757  cdlemg12  37946  cdlemg16ALTN  37954  cdlemg17iqN  37970  cdlemg18c  37976  cdlemg19  37980  cdlemg21  37982  cdlemg28  38000  cdlemk11  38145  cdlemk12  38146  cdlemk16a  38152  cdlemk16  38153  cdlemk18  38164  cdlemk19  38165  cdlemk11u  38167  cdlemk12u  38168  cdlemk21N  38169  cdlemk20  38170  cdlemkoatnle-2N  38171  cdlemk13-2N  38172  cdlemkole-2N  38173  cdlemk14-2N  38174  cdlemk15-2N  38175  cdlemk16-2N  38176  cdlemk17-2N  38177  cdlemk18-2N  38182  cdlemk19-2N  38183  cdlemk7u-2N  38184  cdlemk11u-2N  38185  cdlemk12u-2N  38186  cdlemk22  38189  cdlemk30  38190  cdlemk23-3  38198  cdlemk26b-3  38201  cdlemk26-3  38202  cdlemk27-3  38203  cdlemk11ta  38225  cdlemk47  38245  dia2dimlem1  38360