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  22596  frgrwopreg  30408  cgrtr4d  36183  cgrtrand  36191  cgrtr3and  36193  cgrcoml  36194  cgrextendand  36207  segconeu  36209  btwnouttr2  36220  cgr3tr4  36250  cgrxfr  36253  btwnxfr  36254  lineext  36274  brofs2  36275  brifs2  36276  fscgr  36278  btwnconn1lem2  36286  btwnconn1lem4  36288  btwnconn1lem8  36292  btwnconn1lem11  36295  brsegle2  36307  seglecgr12im  36308  segletr  36312  outsidele  36330  dalem13  40136  2llnma1b  40246  cdlemblem  40253  cdlemb  40254  lhpexle3  40472  lhpat  40503  4atex2-0bOLDN  40539  cdlemd4  40661  cdleme14  40733  cdleme19b  40764  cdleme20f  40774  cdleme20j  40778  cdleme20k  40779  cdleme20l2  40781  cdleme20  40784  cdleme22a  40800  cdleme22e  40804  cdleme26e  40819  cdleme28  40833  cdleme38n  40924  cdleme41sn4aw  40935  cdleme41snaw  40936  cdlemg6c  41080  cdlemg6  41083  cdlemg8c  41089  cdlemg9  41094  cdlemg10a  41100  cdlemg12c  41105  cdlemg12d  41106  cdlemg18d  41141  cdlemg18  41142  cdlemg20  41145  cdlemg21  41146  cdlemg22  41147  cdlemg28a  41153  cdlemg33b0  41161  cdlemg28b  41163  cdlemg33a  41166  cdlemg33  41171  cdlemg34  41172  cdlemg36  41174  cdlemg38  41175  cdlemg46  41195  cdlemk6  41297  cdlemki  41301  cdlemksv2  41307  cdlemk11  41309  cdlemk6u  41322  cdleml4N  41439  cdlemn11pre  41670