Theorem syl333anc 1430

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 1423	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  29621  ofscom  36987  cgrextend  36988  segconeq  36990  ifscgr  37024  cgrsub  37025  btwnxfr  37036  fscgr  37060  linecgr  37061  btwnconn1lem4  37070  btwnconn1lem5  37071  btwnconn1lem6  37072  btwnconn1lem8  37074  btwnconn1lem11  37077  seglecgr12  37091  colinbtwnle  37098  lshpkrlem6  40438  ps-2c  40851  pmodlem1  41169  pmodlem2  41170  dalawlem4  41197  dalawlem9  41202  4atexlemc  41392  cdleme11l  41592  cdleme15c  41599  cdleme16  41608  cdleme19e  41630  cdleme20l2  41644  cdleme20l  41645  cdleme20m  41646  cdleme20  41647  cdleme21d  41653  cdleme21e  41654  cdleme26ee  41683  cdleme26eALTN  41684  cdleme27a  41690  cdleme28b  41694  cdleme28c  41695  cdleme36m  41784  cdlemg12  41973  cdlemg16ALTN  41981  cdlemg17iqN  41997  cdlemg18c  42003  cdlemg19  42007  cdlemg21  42009  cdlemg28  42027  cdlemk11  42172  cdlemk12  42173  cdlemk16a  42179  cdlemk16  42180  cdlemk18  42191  cdlemk19  42192  cdlemk11u  42194  cdlemk12u  42195  cdlemk21N  42196  cdlemk20  42197  cdlemkoatnle-2N  42198  cdlemk13-2N  42199  cdlemkole-2N  42200  cdlemk14-2N  42201  cdlemk15-2N  42202  cdlemk16-2N  42203  cdlemk17-2N  42204  cdlemk18-2N  42209  cdlemk19-2N  42210  cdlemk7u-2N  42211  cdlemk11u-2N  42212  cdlemk12u-2N  42213  cdlemk22  42216  cdlemk30  42217  cdlemk23-3  42225  cdlemk26b-3  42228  cdlemk26-3  42229  cdlemk27-3  42230  cdlemk11ta  42252  cdlemk47  42272  dia2dimlem1  42387