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

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

Proof of Theorem syl212anc
StepHypRef Expression
1 sylXanc.1 . 2
2 sylXanc.2 . 2
3 sylXanc.3 . 2
4 sylXanc.4 . . 3
5 sylXanc.5 . . 3
64, 5jca 518 . 2
7 syl212anc.6 . 2
81, 2, 3, 6, 7syl211anc 1188 1
 Colors of variables: wff set class Syntax hints:   wi 4   wa 358   w3a 934 This theorem is referenced by:  rmob  3079  pntrmax  20713  limptlimpr2lem1  25574  paddasslem4  30012  4atexlemu  30253  4atexlemv  30254  cdleme20aN  30498  cdleme20g  30504  cdlemg9a  30821  cdlemg12a  30832  cdlemg17dALTN  30853  cdlemg18b  30868  cdlemg18c  30869 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8 This theorem depends on definitions:  df-bi 177  df-an 360  df-3an 936
 Copyright terms: Public domain W3C validator