Theorem syl133anc 1411

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

Syntax hints:   → wi 4   ∧ w3a 1097

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 400  df-3an 1099

This theorem is referenced by:  syl233anc  1417  mdetuni0  22668  frgrwopreg  30481  cgrtr4d  36295  cgrtrand  36303  cgrtr3and  36305  cgrcoml  36306  cgrextendand  36319  segconeu  36321  btwnouttr2  36332  cgr3tr4  36362  cgrxfr  36365  btwnxfr  36366  lineext  36386  brofs2  36387  brifs2  36388  fscgr  36390  btwnconn1lem2  36398  btwnconn1lem4  36400  btwnconn1lem8  36404  btwnconn1lem11  36407  brsegle2  36419  seglecgr12im  36420  segletr  36424  outsidele  36442  dalem13  40260  2llnma1b  40370  cdlemblem  40377  cdlemb  40378  lhpexle3  40596  lhpat  40627  4atex2-0bOLDN  40663  cdlemd4  40785  cdleme14  40857  cdleme19b  40888  cdleme20f  40898  cdleme20j  40902  cdleme20k  40903  cdleme20l2  40905  cdleme20  40908  cdleme22a  40924  cdleme22e  40928  cdleme26e  40943  cdleme28  40957  cdleme38n  41048  cdleme41sn4aw  41059  cdleme41snaw  41060  cdlemg6c  41204  cdlemg6  41207  cdlemg8c  41213  cdlemg9  41218  cdlemg10a  41224  cdlemg12c  41229  cdlemg12d  41230  cdlemg18d  41265  cdlemg18  41266  cdlemg20  41269  cdlemg21  41270  cdlemg22  41271  cdlemg28a  41277  cdlemg33b0  41285  cdlemg28b  41287  cdlemg33a  41290  cdlemg33  41295  cdlemg34  41296  cdlemg36  41298  cdlemg38  41299  cdlemg46  41319  cdlemk6  41421  cdlemki  41425  cdlemksv2  41431  cdlemk11  41433  cdlemk6u  41446  cdleml4N  41563  cdlemn11pre  41794