Theorem syl333anc 1405

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 1398	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  29071  ofscom  36220  cgrextend  36221  segconeq  36223  ifscgr  36257  cgrsub  36258  btwnxfr  36269  fscgr  36293  linecgr  36294  btwnconn1lem4  36303  btwnconn1lem5  36304  btwnconn1lem6  36305  btwnconn1lem8  36307  btwnconn1lem11  36310  seglecgr12  36324  colinbtwnle  36331  lshpkrlem6  39488  ps-2c  39901  pmodlem1  40219  pmodlem2  40220  dalawlem4  40247  dalawlem9  40252  4atexlemc  40442  cdleme11l  40642  cdleme15c  40649  cdleme16  40658  cdleme19e  40680  cdleme20l2  40694  cdleme20l  40695  cdleme20m  40696  cdleme20  40697  cdleme21d  40703  cdleme21e  40704  cdleme26ee  40733  cdleme26eALTN  40734  cdleme27a  40740  cdleme28b  40744  cdleme28c  40745  cdleme36m  40834  cdlemg12  41023  cdlemg16ALTN  41031  cdlemg17iqN  41047  cdlemg18c  41053  cdlemg19  41057  cdlemg21  41059  cdlemg28  41077  cdlemk11  41222  cdlemk12  41223  cdlemk16a  41229  cdlemk16  41230  cdlemk18  41241  cdlemk19  41242  cdlemk11u  41244  cdlemk12u  41245  cdlemk21N  41246  cdlemk20  41247  cdlemkoatnle-2N  41248  cdlemk13-2N  41249  cdlemkole-2N  41250  cdlemk14-2N  41251  cdlemk15-2N  41252  cdlemk16-2N  41253  cdlemk17-2N  41254  cdlemk18-2N  41259  cdlemk19-2N  41260  cdlemk7u-2N  41261  cdlemk11u-2N  41262  cdlemk12u-2N  41263  cdlemk22  41266  cdlemk30  41267  cdlemk23-3  41275  cdlemk26b-3  41278  cdlemk26-3  41279  cdlemk27-3  41280  cdlemk11ta  41302  cdlemk47  41322  dia2dimlem1  41437