NFE Home New Foundations Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  NFE Home  >  Th. List  >  syl2anc Unicode version

Theorem syl2anc 642
Description: Syllogism inference combined with contraction. (Contributed by NM, 16-Mar-2012.)
Hypotheses
Ref Expression
syl2anc.1
syl2anc.2
syl2anc.3
Assertion
Ref Expression
syl2anc

Proof of Theorem syl2anc
StepHypRef Expression
1 syl2anc.1 . 2
2 syl2anc.2 . 2
3 syl2anc.3 . . 3
43ex 423 . 2
51, 2, 4sylc 56 1
Colors of variables: wff setvar class
Syntax hints:   wi 4   wa 358
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 177  df-an 360
This theorem is referenced by:  sylancl  643  sylancr  644  sylancom  648  mpdan  649  mpancom  650  orim12d  811  syl13anc  1184  syl31anc  1185  nanbi12d  1303  nfimdOLD  1809  ax11indalem  2197  ax11inda2ALT  2198  eqeq12d  2367  rsp2e  2677  eueq2  3010  csbiedf  3173  nineq12d  3242  symdifeq12d  3256  sstrd  3282  psstrd  3376  sspsstrd  3377  psssstrd  3378  uneq12d  3419  unssd  3439  ineq12d  3458  ssind  3479  preq12d  3807  opkeq12d  4067  symdifexg  4103  pwadjoin  4119  xpkeq12d  4206  sspw1  4335  addceq12d  4391  preaddccan2  4455  leltfintr  4458  ltfintri  4466  ncfinprop  4474  ncfindi  4475  ncfinraise  4481  ncfinlower  4483  tfindi  4496  tfinsuc  4498  tfinltfinlem1  4500  tfinltfin  4501  eventfin  4517  oddtfin  4518  nnadjoin  4520  sfindbl  4530  sfintfin  4532  tfinnn  4534  sfinltfin  4535  1cvsfin  4542  vfintle  4546  vfinspsslem1  4550  vfinspclt  4552  vinf  4555  nfopd  4605  breq12d  4652  xpeq12d  4809  nfimad  4954  funprgOLD  5150  funfni  5183  fnunsn  5190  feq23d  5220  fssxp  5232  fconstg  5251  f1ores  5300  resdif  5306  nffvd  5335  fvelimab  5370  eqfnfvd  5395  fimacnv  5411  foco2  5426  ffvresb  5431  fconst3  5457  isores2  5493  f1oiso2  5500  oveq12d  5540  mpteq12dv  5656  fmpt2d  5695  fvmptd  5702  fullfunexg  5859  trrd  5925  refrd  5926  antird  5928  antid  5929  connexrd  5930  connexd  5931  iserd  5942  xpsnen2g  6054  nenpw1pwlem2  6085  nntccl  6170  ltcpw1pwg  6202  sbthlem1  6203  sbthlem3  6205  sbth  6206  dflec3  6221  nclenc  6222  lenc  6223  tcncg  6224  tlecg  6230  nclenn  6249  addcdir  6251  lemuc1  6253  lemuc2  6254  nnltp1c  6262  addccan2nc  6265  lecadd2  6266  ncslesuc  6267  nmembers1lem3  6270  spaccl  6286  nchoicelem1  6289  nchoicelem2  6290  nchoicelem9  6297  nchoicelem12  6300  nchoicelem13  6301  nchoicelem17  6305  nchoicelem19  6307  nchoice  6308  fnfreclem1  6317  fnfreclem3  6319  frecsuc  6322
  Copyright terms: Public domain W3C validator