Theorem syl133anc 1389

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

Syntax hints:   → wi 4   ∧ w3a 1083

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 209  df-an 399  df-3an 1085

This theorem is referenced by:  syl233anc  1395  mdetuni0  21232  frgrwopreg  28104  cgrtr4d  33448  cgrtrand  33456  cgrtr3and  33458  cgrcoml  33459  cgrextendand  33472  segconeu  33474  btwnouttr2  33485  cgr3tr4  33515  cgrxfr  33518  btwnxfr  33519  lineext  33539  brofs2  33540  brifs2  33541  fscgr  33543  btwnconn1lem2  33551  btwnconn1lem4  33553  btwnconn1lem8  33557  btwnconn1lem11  33560  brsegle2  33572  seglecgr12im  33573  segletr  33577  outsidele  33595  dalem13  36814  2llnma1b  36924  cdlemblem  36931  cdlemb  36932  lhpexle3  37150  lhpat  37181  4atex2-0bOLDN  37217  cdlemd4  37339  cdleme14  37411  cdleme19b  37442  cdleme20f  37452  cdleme20j  37456  cdleme20k  37457  cdleme20l2  37459  cdleme20  37462  cdleme22a  37478  cdleme22e  37482  cdleme26e  37497  cdleme28  37511  cdleme38n  37602  cdleme41sn4aw  37613  cdleme41snaw  37614  cdlemg6c  37758  cdlemg6  37761  cdlemg8c  37767  cdlemg9  37772  cdlemg10a  37778  cdlemg12c  37783  cdlemg12d  37784  cdlemg18d  37819  cdlemg18  37820  cdlemg20  37823  cdlemg21  37824  cdlemg22  37825  cdlemg28a  37831  cdlemg33b0  37839  cdlemg28b  37841  cdlemg33a  37844  cdlemg33  37849  cdlemg34  37850  cdlemg36  37852  cdlemg38  37853  cdlemg46  37873  cdlemk6  37975  cdlemki  37979  cdlemksv2  37985  cdlemk11  37987  cdlemk6u  38000  cdleml4N  38117  cdlemn11pre  38348