Theorem syl133anc 1349

Description: Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.)

Hypotheses

Ref	Expression
syl12anc.1	⊢ (𝜑 → 𝜓)
syl12anc.2	⊢ (𝜑 → 𝜒)
syl12anc.3	⊢ (𝜑 → 𝜃)
syl22anc.4	⊢ (𝜑 → 𝜏)
syl23anc.5	⊢ (𝜑 → 𝜂)
syl33anc.6	⊢ (𝜑 → 𝜁)
syl133anc.7	⊢ (𝜑 → 𝜎)
syl133anc.8	⊢ ((𝜓 ∧ (𝜒 ∧ 𝜃 ∧ 𝜏) ∧ (𝜂 ∧ 𝜁 ∧ 𝜎)) → 𝜌)

Assertion

Ref	Expression
syl133anc	⊢ (𝜑 → 𝜌)

Proof of Theorem syl133anc

Step	Hyp	Ref	Expression
1		syl12anc.1	. 2 ⊢ (𝜑 → 𝜓)
2		syl12anc.2	. 2 ⊢ (𝜑 → 𝜒)
3		syl12anc.3	. 2 ⊢ (𝜑 → 𝜃)
4		syl22anc.4	. 2 ⊢ (𝜑 → 𝜏)
5		syl23anc.5	. . 3 ⊢ (𝜑 → 𝜂)
6		syl33anc.6	. . 3 ⊢ (𝜑 → 𝜁)
7		syl133anc.7	. . 3 ⊢ (𝜑 → 𝜎)
8	5, 6, 7	3jca 1242	. 2 ⊢ (𝜑 → (𝜂 ∧ 𝜁 ∧ 𝜎))
9		syl133anc.8	. 2 ⊢ ((𝜓 ∧ (𝜒 ∧ 𝜃 ∧ 𝜏) ∧ (𝜂 ∧ 𝜁 ∧ 𝜎)) → 𝜌)
10	1, 2, 3, 4, 8, 9	syl131anc 1339	1 ⊢ (𝜑 → 𝜌)

Syntax hints:   → wi 4   ∧ w3a 1037

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 197  df-an 386  df-3an 1039

This theorem is referenced by:  syl233anc  1355  mdetuni0  20427  frgrwopreg  27187  cgrtr4d  32092  cgrtrand  32100  cgrtr3and  32102  cgrcoml  32103  cgrextendand  32116  segconeu  32118  btwnouttr2  32129  cgr3tr4  32159  cgrxfr  32162  btwnxfr  32163  lineext  32183  brofs2  32184  brifs2  32185  fscgr  32187  btwnconn1lem2  32195  btwnconn1lem4  32197  btwnconn1lem8  32201  btwnconn1lem11  32204  brsegle2  32216  seglecgr12im  32217  segletr  32221  outsidele  32239  dalem13  34962  2llnma1b  35072  cdlemblem  35079  cdlemb  35080  lhpexle3  35298  lhpat  35329  4atex2-0bOLDN  35365  cdlemd4  35488  cdleme14  35560  cdleme19b  35592  cdleme20f  35602  cdleme20j  35606  cdleme20k  35607  cdleme20l2  35609  cdleme20  35612  cdleme22a  35628  cdleme22e  35632  cdleme26e  35647  cdleme28  35661  cdleme38n  35752  cdleme41sn4aw  35763  cdleme41snaw  35764  cdlemg6c  35908  cdlemg6  35911  cdlemg8c  35917  cdlemg9  35922  cdlemg10a  35928  cdlemg12c  35933  cdlemg12d  35934  cdlemg18d  35969  cdlemg18  35970  cdlemg20  35973  cdlemg21  35974  cdlemg22  35975  cdlemg28a  35981  cdlemg33b0  35989  cdlemg28b  35991  cdlemg33a  35994  cdlemg33  35999  cdlemg34  36000  cdlemg36  36002  cdlemg38  36003  cdlemg46  36023  cdlemk6  36125  cdlemki  36129  cdlemksv2  36135  cdlemk11  36137  cdlemk6u  36150  cdleml4N  36267  cdlemn11pre  36499