Theorem syl133anc 1396

Description: Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.)

Hypotheses

Ref	Expression
syl3anc.1	⊢ (𝜑 → 𝜓)
syl3anc.2	⊢ (𝜑 → 𝜒)
syl3anc.3	⊢ (𝜑 → 𝜃)
syl3Xanc.4	⊢ (𝜑 → 𝜏)
syl23anc.5	⊢ (𝜑 → 𝜂)
syl33anc.6	⊢ (𝜑 → 𝜁)
syl133anc.7	⊢ (𝜑 → 𝜎)
syl133anc.8	⊢ ((𝜓 ∧ (𝜒 ∧ 𝜃 ∧ 𝜏) ∧ (𝜂 ∧ 𝜁 ∧ 𝜎)) → 𝜌)

Assertion

Ref	Expression
syl133anc	⊢ (𝜑 → 𝜌)

Proof of Theorem syl133anc

Step	Hyp	Ref	Expression
1		syl3anc.1	. 2 ⊢ (𝜑 → 𝜓)
2		syl3anc.2	. 2 ⊢ (𝜑 → 𝜒)
3		syl3anc.3	. 2 ⊢ (𝜑 → 𝜃)
4		syl3Xanc.4	. 2 ⊢ (𝜑 → 𝜏)
5		syl23anc.5	. . 3 ⊢ (𝜑 → 𝜂)
6		syl33anc.6	. . 3 ⊢ (𝜑 → 𝜁)
7		syl133anc.7	. . 3 ⊢ (𝜑 → 𝜎)
8	5, 6, 7	3jca 1129	. 2 ⊢ (𝜑 → (𝜂 ∧ 𝜁 ∧ 𝜎))
9		syl133anc.8	. 2 ⊢ ((𝜓 ∧ (𝜒 ∧ 𝜃 ∧ 𝜏) ∧ (𝜂 ∧ 𝜁 ∧ 𝜎)) → 𝜌)
10	1, 2, 3, 4, 8, 9	syl131anc 1386	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:  syl233anc  1402  mdetuni0  22577  frgrwopreg  30410  cgrtr4d  36198  cgrtrand  36206  cgrtr3and  36208  cgrcoml  36209  cgrextendand  36222  segconeu  36224  btwnouttr2  36235  cgr3tr4  36265  cgrxfr  36268  btwnxfr  36269  lineext  36289  brofs2  36290  brifs2  36291  fscgr  36293  btwnconn1lem2  36301  btwnconn1lem4  36303  btwnconn1lem8  36307  btwnconn1lem11  36310  brsegle2  36322  seglecgr12im  36323  segletr  36327  outsidele  36345  dalem13  40049  2llnma1b  40159  cdlemblem  40166  cdlemb  40167  lhpexle3  40385  lhpat  40416  4atex2-0bOLDN  40452  cdlemd4  40574  cdleme14  40646  cdleme19b  40677  cdleme20f  40687  cdleme20j  40691  cdleme20k  40692  cdleme20l2  40694  cdleme20  40697  cdleme22a  40713  cdleme22e  40717  cdleme26e  40732  cdleme28  40746  cdleme38n  40837  cdleme41sn4aw  40848  cdleme41snaw  40849  cdlemg6c  40993  cdlemg6  40996  cdlemg8c  41002  cdlemg9  41007  cdlemg10a  41013  cdlemg12c  41018  cdlemg12d  41019  cdlemg18d  41054  cdlemg18  41055  cdlemg20  41058  cdlemg21  41059  cdlemg22  41060  cdlemg28a  41066  cdlemg33b0  41074  cdlemg28b  41076  cdlemg33a  41079  cdlemg33  41084  cdlemg34  41085  cdlemg36  41087  cdlemg38  41088  cdlemg46  41108  cdlemk6  41210  cdlemki  41214  cdlemksv2  41220  cdlemk11  41222  cdlemk6u  41235  cdleml4N  41352  cdlemn11pre  41583