Theorem syl133anc 1395

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 1385	1 ⊢ (𝜑 → 𝜌)

Syntax hints:   → wi 4   ∧ w3a 1086

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 1088

This theorem is referenced by:  syl233anc  1401  mdetuni0  22515  frgrwopreg  30259  cgrtr4d  35980  cgrtrand  35988  cgrtr3and  35990  cgrcoml  35991  cgrextendand  36004  segconeu  36006  btwnouttr2  36017  cgr3tr4  36047  cgrxfr  36050  btwnxfr  36051  lineext  36071  brofs2  36072  brifs2  36073  fscgr  36075  btwnconn1lem2  36083  btwnconn1lem4  36085  btwnconn1lem8  36089  btwnconn1lem11  36092  brsegle2  36104  seglecgr12im  36105  segletr  36109  outsidele  36127  dalem13  39677  2llnma1b  39787  cdlemblem  39794  cdlemb  39795  lhpexle3  40013  lhpat  40044  4atex2-0bOLDN  40080  cdlemd4  40202  cdleme14  40274  cdleme19b  40305  cdleme20f  40315  cdleme20j  40319  cdleme20k  40320  cdleme20l2  40322  cdleme20  40325  cdleme22a  40341  cdleme22e  40345  cdleme26e  40360  cdleme28  40374  cdleme38n  40465  cdleme41sn4aw  40476  cdleme41snaw  40477  cdlemg6c  40621  cdlemg6  40624  cdlemg8c  40630  cdlemg9  40635  cdlemg10a  40641  cdlemg12c  40646  cdlemg12d  40647  cdlemg18d  40682  cdlemg18  40683  cdlemg20  40686  cdlemg21  40687  cdlemg22  40688  cdlemg28a  40694  cdlemg33b0  40702  cdlemg28b  40704  cdlemg33a  40707  cdlemg33  40712  cdlemg34  40713  cdlemg36  40715  cdlemg38  40716  cdlemg46  40736  cdlemk6  40838  cdlemki  40842  cdlemksv2  40848  cdlemk11  40850  cdlemk6u  40863  cdleml4N  40980  cdlemn11pre  41211