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  22537  frgrwopreg  30301  cgrtr4d  36025  cgrtrand  36033  cgrtr3and  36035  cgrcoml  36036  cgrextendand  36049  segconeu  36051  btwnouttr2  36062  cgr3tr4  36092  cgrxfr  36095  btwnxfr  36096  lineext  36116  brofs2  36117  brifs2  36118  fscgr  36120  btwnconn1lem2  36128  btwnconn1lem4  36130  btwnconn1lem8  36134  btwnconn1lem11  36137  brsegle2  36149  seglecgr12im  36150  segletr  36154  outsidele  36172  dalem13  39721  2llnma1b  39831  cdlemblem  39838  cdlemb  39839  lhpexle3  40057  lhpat  40088  4atex2-0bOLDN  40124  cdlemd4  40246  cdleme14  40318  cdleme19b  40349  cdleme20f  40359  cdleme20j  40363  cdleme20k  40364  cdleme20l2  40366  cdleme20  40369  cdleme22a  40385  cdleme22e  40389  cdleme26e  40404  cdleme28  40418  cdleme38n  40509  cdleme41sn4aw  40520  cdleme41snaw  40521  cdlemg6c  40665  cdlemg6  40668  cdlemg8c  40674  cdlemg9  40679  cdlemg10a  40685  cdlemg12c  40690  cdlemg12d  40691  cdlemg18d  40726  cdlemg18  40727  cdlemg20  40730  cdlemg21  40731  cdlemg22  40732  cdlemg28a  40738  cdlemg33b0  40746  cdlemg28b  40748  cdlemg33a  40751  cdlemg33  40756  cdlemg34  40757  cdlemg36  40759  cdlemg38  40760  cdlemg46  40780  cdlemk6  40882  cdlemki  40886  cdlemksv2  40892  cdlemk11  40894  cdlemk6u  40907  cdleml4N  41024  cdlemn11pre  41255