Theorem syl133anc 1393

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 1128	. 2 ⊢ (𝜑 → (𝜂 ∧ 𝜁 ∧ 𝜎))
9		syl133anc.8	. 2 ⊢ ((𝜓 ∧ (𝜒 ∧ 𝜃 ∧ 𝜏) ∧ (𝜂 ∧ 𝜁 ∧ 𝜎)) → 𝜌)
10	1, 2, 3, 4, 8, 9	syl131anc 1383	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 206  df-an 397  df-3an 1089

This theorem is referenced by:  syl233anc  1399  mdetuni0  22114  frgrwopreg  29565  cgrtr4d  34945  cgrtrand  34953  cgrtr3and  34955  cgrcoml  34956  cgrextendand  34969  segconeu  34971  btwnouttr2  34982  cgr3tr4  35012  cgrxfr  35015  btwnxfr  35016  lineext  35036  brofs2  35037  brifs2  35038  fscgr  35040  btwnconn1lem2  35048  btwnconn1lem4  35050  btwnconn1lem8  35054  btwnconn1lem11  35057  brsegle2  35069  seglecgr12im  35070  segletr  35074  outsidele  35092  dalem13  38535  2llnma1b  38645  cdlemblem  38652  cdlemb  38653  lhpexle3  38871  lhpat  38902  4atex2-0bOLDN  38938  cdlemd4  39060  cdleme14  39132  cdleme19b  39163  cdleme20f  39173  cdleme20j  39177  cdleme20k  39178  cdleme20l2  39180  cdleme20  39183  cdleme22a  39199  cdleme22e  39203  cdleme26e  39218  cdleme28  39232  cdleme38n  39323  cdleme41sn4aw  39334  cdleme41snaw  39335  cdlemg6c  39479  cdlemg6  39482  cdlemg8c  39488  cdlemg9  39493  cdlemg10a  39499  cdlemg12c  39504  cdlemg12d  39505  cdlemg18d  39540  cdlemg18  39541  cdlemg20  39544  cdlemg21  39545  cdlemg22  39546  cdlemg28a  39552  cdlemg33b0  39560  cdlemg28b  39562  cdlemg33a  39565  cdlemg33  39570  cdlemg34  39571  cdlemg36  39573  cdlemg38  39574  cdlemg46  39594  cdlemk6  39696  cdlemki  39700  cdlemksv2  39706  cdlemk11  39708  cdlemk6u  39721  cdleml4N  39838  cdlemn11pre  40069