MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  syl133anc Unicode version

Theorem syl133anc 1251
Description: Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.)
Hypotheses
Ref Expression
sylXanc.1
sylXanc.2
sylXanc.3
sylXanc.4
sylXanc.5
sylXanc.6
sylXanc.7
syl133anc.8
Assertion
Ref Expression
syl133anc

Proof of Theorem syl133anc
StepHypRef Expression
1 sylXanc.1 . 2
2 sylXanc.2 . 2
3 sylXanc.3 . 2
4 sylXanc.4 . 2
5 sylXanc.5 . . 3
6 sylXanc.6 . . 3
7 sylXanc.7 . . 3
85, 6, 73jca 1176 . 2
9 syl133anc.8 . 2
101, 2, 3, 4, 8, 9syl131anc 1241 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  /\w3a 973
This theorem is referenced by:  syl233anc  1257  mdetuni0  19123  cgrtr4d  29635  cgrtrand  29643  cgrtr3and  29645  cgrcoml  29646  cgrextendand  29659  segconeu  29661  btwnouttr2  29672  cgr3tr4  29702  cgrxfr  29705  btwnxfr  29706  lineext  29726  brofs2  29727  brifs2  29728  fscgr  29730  btwnconn1lem2  29738  btwnconn1lem4  29740  btwnconn1lem8  29744  btwnconn1lem11  29747  brsegle2  29759  seglecgr12im  29760  segletr  29764  outsidele  29782  dalem13  35400  2llnma1b  35510  cdlemblem  35517  cdlemb  35518  lhpexle3  35736  lhpat  35767  4atex2-0bOLDN  35803  cdlemd4  35926  cdleme14  35998  cdleme19b  36030  cdleme20f  36040  cdleme20j  36044  cdleme20k  36045  cdleme20l2  36047  cdleme20  36050  cdleme22a  36066  cdleme22e  36070  cdleme26e  36085  cdleme28  36099  cdleme38n  36190  cdleme41sn4aw  36201  cdleme41snaw  36202  cdlemg6c  36346  cdlemg6  36349  cdlemg8c  36355  cdlemg9  36360  cdlemg10a  36366  cdlemg12c  36371  cdlemg12d  36372  cdlemg18d  36407  cdlemg18  36408  cdlemg20  36411  cdlemg21  36412  cdlemg22  36413  cdlemg28a  36419  cdlemg33b0  36427  cdlemg28b  36429  cdlemg33a  36432  cdlemg33  36437  cdlemg34  36438  cdlemg36  36440  cdlemg38  36441  cdlemg46  36461  cdlemk6  36563  cdlemki  36567  cdlemksv2  36573  cdlemk11  36575  cdlemk6u  36588  cdleml4N  36705  cdlemn11pre  36937
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 185  df-an 371  df-3an 975
  Copyright terms: Public domain W3C validator