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 207  df-an 396  df-3an 1089

This theorem is referenced by:  syl233anc  1399  mdetuni0  22648  frgrwopreg  30355  cgrtr4d  35949  cgrtrand  35957  cgrtr3and  35959  cgrcoml  35960  cgrextendand  35973  segconeu  35975  btwnouttr2  35986  cgr3tr4  36016  cgrxfr  36019  btwnxfr  36020  lineext  36040  brofs2  36041  brifs2  36042  fscgr  36044  btwnconn1lem2  36052  btwnconn1lem4  36054  btwnconn1lem8  36058  btwnconn1lem11  36061  brsegle2  36073  seglecgr12im  36074  segletr  36078  outsidele  36096  dalem13  39633  2llnma1b  39743  cdlemblem  39750  cdlemb  39751  lhpexle3  39969  lhpat  40000  4atex2-0bOLDN  40036  cdlemd4  40158  cdleme14  40230  cdleme19b  40261  cdleme20f  40271  cdleme20j  40275  cdleme20k  40276  cdleme20l2  40278  cdleme20  40281  cdleme22a  40297  cdleme22e  40301  cdleme26e  40316  cdleme28  40330  cdleme38n  40421  cdleme41sn4aw  40432  cdleme41snaw  40433  cdlemg6c  40577  cdlemg6  40580  cdlemg8c  40586  cdlemg9  40591  cdlemg10a  40597  cdlemg12c  40602  cdlemg12d  40603  cdlemg18d  40638  cdlemg18  40639  cdlemg20  40642  cdlemg21  40643  cdlemg22  40644  cdlemg28a  40650  cdlemg33b0  40658  cdlemg28b  40660  cdlemg33a  40663  cdlemg33  40668  cdlemg34  40669  cdlemg36  40671  cdlemg38  40672  cdlemg46  40692  cdlemk6  40794  cdlemki  40798  cdlemksv2  40804  cdlemk11  40806  cdlemk6u  40819  cdleml4N  40936  cdlemn11pre  41167