Theorem syl333anc 1429

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

This proof depends on syntax axioms:   → wi 4   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  eengtrkg  29367  ofscom  36512  cgrextend  36513  segconeq  36515  ifscgr  36549  cgrsub  36550  btwnxfr  36561  fscgr  36585  linecgr  36586  btwnconn1lem4  36595  btwnconn1lem5  36596  btwnconn1lem6  36597  btwnconn1lem8  36599  btwnconn1lem11  36602  seglecgr12  36616  colinbtwnle  36623  lshpkrlem6  39922  ps-2c  40335  pmodlem1  40653  pmodlem2  40654  dalawlem4  40681  dalawlem9  40686  4atexlemc  40876  cdleme11l  41076  cdleme15c  41083  cdleme16  41092  cdleme19e  41114  cdleme20l2  41128  cdleme20l  41129  cdleme20m  41130  cdleme20  41131  cdleme21d  41137  cdleme21e  41138  cdleme26ee  41167  cdleme26eALTN  41168  cdleme27a  41174  cdleme28b  41178  cdleme28c  41179  cdleme36m  41268  cdlemg12  41457  cdlemg16ALTN  41465  cdlemg17iqN  41481  cdlemg18c  41487  cdlemg19  41491  cdlemg21  41493  cdlemg28  41511  cdlemk11  41656  cdlemk12  41657  cdlemk16a  41663  cdlemk16  41664  cdlemk18  41675  cdlemk19  41676  cdlemk11u  41678  cdlemk12u  41679  cdlemk21N  41680  cdlemk20  41681  cdlemkoatnle-2N  41682  cdlemk13-2N  41683  cdlemkole-2N  41684  cdlemk14-2N  41685  cdlemk15-2N  41686  cdlemk16-2N  41687  cdlemk17-2N  41688  cdlemk18-2N  41693  cdlemk19-2N  41694  cdlemk7u-2N  41695  cdlemk11u-2N  41696  cdlemk12u-2N  41697  cdlemk22  41700  cdlemk30  41701  cdlemk23-3  41709  cdlemk26b-3  41712  cdlemk26-3  41713  cdlemk27-3  41714  cdlemk11ta  41736  cdlemk47  41756  dia2dimlem1  41871