Theorem syl133anc 1341

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

Syntax hints:   → wi 4   ∧ w3a 1031

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 196  df-an 385  df-3an 1033

This theorem is referenced by:  syl233anc  1347  mdetuni0  20246  cgrtr4d  31262  cgrtrand  31270  cgrtr3and  31272  cgrcoml  31273  cgrextendand  31286  segconeu  31288  btwnouttr2  31299  cgr3tr4  31329  cgrxfr  31332  btwnxfr  31333  lineext  31353  brofs2  31354  brifs2  31355  fscgr  31357  btwnconn1lem2  31365  btwnconn1lem4  31367  btwnconn1lem8  31371  btwnconn1lem11  31374  brsegle2  31386  seglecgr12im  31387  segletr  31391  outsidele  31409  dalem13  33980  2llnma1b  34090  cdlemblem  34097  cdlemb  34098  lhpexle3  34316  lhpat  34347  4atex2-0bOLDN  34383  cdlemd4  34506  cdleme14  34578  cdleme19b  34610  cdleme20f  34620  cdleme20j  34624  cdleme20k  34625  cdleme20l2  34627  cdleme20  34630  cdleme22a  34646  cdleme22e  34650  cdleme26e  34665  cdleme28  34679  cdleme38n  34770  cdleme41sn4aw  34781  cdleme41snaw  34782  cdlemg6c  34926  cdlemg6  34929  cdlemg8c  34935  cdlemg9  34940  cdlemg10a  34946  cdlemg12c  34951  cdlemg12d  34952  cdlemg18d  34987  cdlemg18  34988  cdlemg20  34991  cdlemg21  34992  cdlemg22  34993  cdlemg28a  34999  cdlemg33b0  35007  cdlemg28b  35009  cdlemg33a  35012  cdlemg33  35017  cdlemg34  35018  cdlemg36  35020  cdlemg38  35021  cdlemg46  35041  cdlemk6  35143  cdlemki  35147  cdlemksv2  35153  cdlemk11  35155  cdlemk6u  35168  cdleml4N  35285  cdlemn11pre  35517