Theorem syl133anc 1396

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

Syntax hints:   → wi 4   ∧ w3a 1087

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 207  df-an 396  df-3an 1089

This theorem is referenced by:  syl233anc  1402  mdetuni0  22595  frgrwopreg  30413  cgrtr4d  36188  cgrtrand  36196  cgrtr3and  36198  cgrcoml  36199  cgrextendand  36212  segconeu  36214  btwnouttr2  36225  cgr3tr4  36255  cgrxfr  36258  btwnxfr  36259  lineext  36279  brofs2  36280  brifs2  36281  fscgr  36283  btwnconn1lem2  36291  btwnconn1lem4  36293  btwnconn1lem8  36297  btwnconn1lem11  36300  brsegle2  36312  seglecgr12im  36313  segletr  36317  outsidele  36335  dalem13  40133  2llnma1b  40243  cdlemblem  40250  cdlemb  40251  lhpexle3  40469  lhpat  40500  4atex2-0bOLDN  40536  cdlemd4  40658  cdleme14  40730  cdleme19b  40761  cdleme20f  40771  cdleme20j  40775  cdleme20k  40776  cdleme20l2  40778  cdleme20  40781  cdleme22a  40797  cdleme22e  40801  cdleme26e  40816  cdleme28  40830  cdleme38n  40921  cdleme41sn4aw  40932  cdleme41snaw  40933  cdlemg6c  41077  cdlemg6  41080  cdlemg8c  41086  cdlemg9  41091  cdlemg10a  41097  cdlemg12c  41102  cdlemg12d  41103  cdlemg18d  41138  cdlemg18  41139  cdlemg20  41142  cdlemg21  41143  cdlemg22  41144  cdlemg28a  41150  cdlemg33b0  41158  cdlemg28b  41160  cdlemg33a  41163  cdlemg33  41168  cdlemg34  41169  cdlemg36  41171  cdlemg38  41172  cdlemg46  41192  cdlemk6  41294  cdlemki  41298  cdlemksv2  41304  cdlemk11  41306  cdlemk6u  41319  cdleml4N  41436  cdlemn11pre  41667