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  22815  frgrwopreg  30711  cgrtr4d  36498  cgrtrand  36506  cgrtr3and  36508  cgrcoml  36509  cgrextendand  36522  segconeu  36524  btwnouttr2  36535  cgr3tr4  36565  cgrxfr  36568  btwnxfr  36569  lineext  36589  brofs2  36590  brifs2  36591  fscgr  36593  btwnconn1lem2  36601  btwnconn1lem4  36603  btwnconn1lem8  36607  btwnconn1lem11  36610  brsegle2  36622  seglecgr12im  36623  segletr  36627  outsidele  36645  dalem13  40491  2llnma1b  40601  cdlemblem  40608  cdlemb  40609  lhpexle3  40827  lhpat  40858  4atex2-0bOLDN  40894  cdlemd4  41016  cdleme14  41088  cdleme19b  41119  cdleme20f  41129  cdleme20j  41133  cdleme20k  41134  cdleme20l2  41136  cdleme20  41139  cdleme22a  41155  cdleme22e  41159  cdleme26e  41174  cdleme28  41188  cdleme38n  41279  cdleme41sn4aw  41290  cdleme41snaw  41291  cdlemg6c  41435  cdlemg6  41438  cdlemg8c  41444  cdlemg9  41449  cdlemg10a  41455  cdlemg12c  41460  cdlemg12d  41461  cdlemg18d  41496  cdlemg18  41497  cdlemg20  41500  cdlemg21  41501  cdlemg22  41502  cdlemg28a  41508  cdlemg33b0  41516  cdlemg28b  41518  cdlemg33a  41521  cdlemg33  41526  cdlemg34  41527  cdlemg36  41529  cdlemg38  41530  cdlemg46  41550  cdlemk6  41652  cdlemki  41656  cdlemksv2  41662  cdlemk11  41664  cdlemk6u  41677  cdleml4N  41794  cdlemn11pre  42025