Theorem syl133anc 1421

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 1411	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  1427  mdetuni0  22969  frgrwopreg  30957  cgrtr4d  36941  cgrtrand  36949  cgrtr3and  36951  cgrcoml  36952  cgrextendand  36965  segconeu  36967  btwnouttr2  36978  cgr3tr4  37008  cgrxfr  37011  btwnxfr  37012  lineext  37032  brofs2  37033  brifs2  37034  fscgr  37036  btwnconn1lem2  37044  btwnconn1lem4  37046  btwnconn1lem8  37050  btwnconn1lem11  37053  brsegle2  37065  seglecgr12im  37066  segletr  37070  outsidele  37088  dalem13  40936  2llnma1b  41046  cdlemblem  41053  cdlemb  41054  lhpexle3  41272  lhpat  41303  4atex2-0bOLDN  41339  cdlemd4  41461  cdleme14  41533  cdleme19b  41564  cdleme20f  41574  cdleme20j  41578  cdleme20k  41579  cdleme20l2  41581  cdleme20  41584  cdleme22a  41600  cdleme22e  41604  cdleme26e  41619  cdleme28  41633  cdleme38n  41724  cdleme41sn4aw  41735  cdleme41snaw  41736  cdlemg6c  41880  cdlemg6  41883  cdlemg8c  41889  cdlemg9  41894  cdlemg10a  41900  cdlemg12c  41905  cdlemg12d  41906  cdlemg18d  41941  cdlemg18  41942  cdlemg20  41945  cdlemg21  41946  cdlemg22  41947  cdlemg28a  41953  cdlemg33b0  41961  cdlemg28b  41963  cdlemg33a  41966  cdlemg33  41971  cdlemg34  41972  cdlemg36  41974  cdlemg38  41975  cdlemg46  41995  cdlemk6  42097  cdlemki  42101  cdlemksv2  42107  cdlemk11  42109  cdlemk6u  42122  cdleml4N  42239  cdlemn11pre  42470