Theorem syl133anc 1420

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 1146	. 2 ⊢ (𝜑 → (𝜂 ∧ 𝜁 ∧ 𝜎))
9		syl133anc.8	. 2 ⊢ ((𝜓 ∧ (𝜒 ∧ 𝜃 ∧ 𝜏) ∧ (𝜂 ∧ 𝜁 ∧ 𝜎)) → 𝜌)
10	1, 2, 3, 4, 8, 9	syl131anc 1410	1 ⊢ (𝜑 → 𝜌)

This proof depends on syntax axioms:   → wi 4   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  syl233anc  1426  mdetuni0  22937  frgrwopreg  30925  cgrtr4d  36825  cgrtrand  36833  cgrtr3and  36835  cgrcoml  36836  cgrextendand  36849  segconeu  36851  btwnouttr2  36862  cgr3tr4  36892  cgrxfr  36895  btwnxfr  36896  lineext  36916  brofs2  36917  brifs2  36918  fscgr  36920  btwnconn1lem2  36928  btwnconn1lem4  36930  btwnconn1lem8  36934  btwnconn1lem11  36937  brsegle2  36949  seglecgr12im  36950  segletr  36954  outsidele  36972  dalem13  40809  2llnma1b  40919  cdlemblem  40926  cdlemb  40927  lhpexle3  41145  lhpat  41176  4atex2-0bOLDN  41212  cdlemd4  41334  cdleme14  41406  cdleme19b  41437  cdleme20f  41447  cdleme20j  41451  cdleme20k  41452  cdleme20l2  41454  cdleme20  41457  cdleme22a  41473  cdleme22e  41477  cdleme26e  41492  cdleme28  41506  cdleme38n  41597  cdleme41sn4aw  41608  cdleme41snaw  41609  cdlemg6c  41753  cdlemg6  41756  cdlemg8c  41762  cdlemg9  41767  cdlemg10a  41773  cdlemg12c  41778  cdlemg12d  41779  cdlemg18d  41814  cdlemg18  41815  cdlemg20  41818  cdlemg21  41819  cdlemg22  41820  cdlemg28a  41826  cdlemg33b0  41834  cdlemg28b  41836  cdlemg33a  41839  cdlemg33  41844  cdlemg34  41845  cdlemg36  41847  cdlemg38  41848  cdlemg46  41868  cdlemk6  41970  cdlemki  41974  cdlemksv2  41980  cdlemk11  41982  cdlemk6u  41995  cdleml4N  42112  cdlemn11pre  42343