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  22586  frgrwopreg  30393  cgrtr4d  36167  cgrtrand  36175  cgrtr3and  36177  cgrcoml  36178  cgrextendand  36191  segconeu  36193  btwnouttr2  36204  cgr3tr4  36234  cgrxfr  36237  btwnxfr  36238  lineext  36258  brofs2  36259  brifs2  36260  fscgr  36262  btwnconn1lem2  36270  btwnconn1lem4  36272  btwnconn1lem8  36276  btwnconn1lem11  36279  brsegle2  36291  seglecgr12im  36292  segletr  36296  outsidele  36314  dalem13  40122  2llnma1b  40232  cdlemblem  40239  cdlemb  40240  lhpexle3  40458  lhpat  40489  4atex2-0bOLDN  40525  cdlemd4  40647  cdleme14  40719  cdleme19b  40750  cdleme20f  40760  cdleme20j  40764  cdleme20k  40765  cdleme20l2  40767  cdleme20  40770  cdleme22a  40786  cdleme22e  40790  cdleme26e  40805  cdleme28  40819  cdleme38n  40910  cdleme41sn4aw  40921  cdleme41snaw  40922  cdlemg6c  41066  cdlemg6  41069  cdlemg8c  41075  cdlemg9  41080  cdlemg10a  41086  cdlemg12c  41091  cdlemg12d  41092  cdlemg18d  41127  cdlemg18  41128  cdlemg20  41131  cdlemg21  41132  cdlemg22  41133  cdlemg28a  41139  cdlemg33b0  41147  cdlemg28b  41149  cdlemg33a  41152  cdlemg33  41157  cdlemg34  41158  cdlemg36  41160  cdlemg38  41161  cdlemg46  41181  cdlemk6  41283  cdlemki  41287  cdlemksv2  41293  cdlemk11  41295  cdlemk6u  41308  cdleml4N  41425  cdlemn11pre  41656