Theorem syl133anc 1500

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

Syntax hints:   → wi 4   ∧ w3a 1072

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

This theorem is referenced by:  syl233anc  1506  mdetuni0  20649  frgrwopreg  27498  cgrtr4d  32419  cgrtrand  32427  cgrtr3and  32429  cgrcoml  32430  cgrextendand  32443  segconeu  32445  btwnouttr2  32456  cgr3tr4  32486  cgrxfr  32489  btwnxfr  32490  lineext  32510  brofs2  32511  brifs2  32512  fscgr  32514  btwnconn1lem2  32522  btwnconn1lem4  32524  btwnconn1lem8  32528  btwnconn1lem11  32531  brsegle2  32543  seglecgr12im  32544  segletr  32548  outsidele  32566  dalem13  35483  2llnma1b  35593  cdlemblem  35600  cdlemb  35601  lhpexle3  35819  lhpat  35850  4atex2-0bOLDN  35886  cdlemd4  36009  cdleme14  36081  cdleme19b  36112  cdleme20f  36122  cdleme20j  36126  cdleme20k  36127  cdleme20l2  36129  cdleme20  36132  cdleme22a  36148  cdleme22e  36152  cdleme26e  36167  cdleme28  36181  cdleme38n  36272  cdleme41sn4aw  36283  cdleme41snaw  36284  cdlemg6c  36428  cdlemg6  36431  cdlemg8c  36437  cdlemg9  36442  cdlemg10a  36448  cdlemg12c  36453  cdlemg12d  36454  cdlemg18d  36489  cdlemg18  36490  cdlemg20  36493  cdlemg21  36494  cdlemg22  36495  cdlemg28a  36501  cdlemg33b0  36509  cdlemg28b  36511  cdlemg33a  36514  cdlemg33  36519  cdlemg34  36520  cdlemg36  36522  cdlemg38  36523  cdlemg46  36543  cdlemk6  36645  cdlemki  36649  cdlemksv2  36655  cdlemk11  36657  cdlemk6u  36670  cdleml4N  36787  cdlemn11pre  37019