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 ⊢ (𝜑 → 𝜆)

Syntax hints:   → wi 4   ∧ w3a 1103

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 401  df-3an 1105

This theorem is referenced by:  eengtrkg  29336  ofscom  36499  cgrextend  36500  segconeq  36502  ifscgr  36536  cgrsub  36537  btwnxfr  36548  fscgr  36572  linecgr  36573  btwnconn1lem4  36582  btwnconn1lem5  36583  btwnconn1lem6  36584  btwnconn1lem8  36586  btwnconn1lem11  36589  seglecgr12  36603  colinbtwnle  36610  lshpkrlem6  39889  ps-2c  40302  pmodlem1  40620  pmodlem2  40621  dalawlem4  40648  dalawlem9  40653  4atexlemc  40843  cdleme11l  41043  cdleme15c  41050  cdleme16  41059  cdleme19e  41081  cdleme20l2  41095  cdleme20l  41096  cdleme20m  41097  cdleme20  41098  cdleme21d  41104  cdleme21e  41105  cdleme26ee  41134  cdleme26eALTN  41135  cdleme27a  41141  cdleme28b  41145  cdleme28c  41146  cdleme36m  41235  cdlemg12  41424  cdlemg16ALTN  41432  cdlemg17iqN  41448  cdlemg18c  41454  cdlemg19  41458  cdlemg21  41460  cdlemg28  41478  cdlemk11  41623  cdlemk12  41624  cdlemk16a  41630  cdlemk16  41631  cdlemk18  41642  cdlemk19  41643  cdlemk11u  41645  cdlemk12u  41646  cdlemk21N  41647  cdlemk20  41648  cdlemkoatnle-2N  41649  cdlemk13-2N  41650  cdlemkole-2N  41651  cdlemk14-2N  41652  cdlemk15-2N  41653  cdlemk16-2N  41654  cdlemk17-2N  41655  cdlemk18-2N  41660  cdlemk19-2N  41661  cdlemk7u-2N  41662  cdlemk11u-2N  41663  cdlemk12u-2N  41664  cdlemk22  41667  cdlemk30  41668  cdlemk23-3  41676  cdlemk26b-3  41679  cdlemk26-3  41680  cdlemk27-3  41681  cdlemk11ta  41703  cdlemk47  41723  dia2dimlem1  41838