ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  syl2anc Structured version   GIF version

Theorem syl2anc 393
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 108 . 2 (ψ → (χθ))
51, 2, 4sylc 56 1 (φθ)
Colors of variables: wff set class
Syntax hints:  wi 4   wa 97
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia3 101
This theorem is referenced by:  sylancl  394  sylancr  395  sylancom  399  mpdan  400  mpancom  401  orim12d  687  syl13anc  1123  syl31anc  1124  nford  1441  eqeq12d  2036  rsp2e  2350  r19.29d2r  2433  elrab3t  2674  eueq2dc  2691  csbiedf  2864  sstrd  2932  psstrd  3029  sspsstrd  3030  psssstrd  3031  uneq12d  3075  unssd  3096  ineq12d  3116  ssind  3138  preq12d  3429  opeq12d  3531  nfopd  3540  breq12d  3751  mpteq12dva  3812  ssexd  3871  exss  3937  opexg  3938  opth  3948  op1stbg  4160  tfisi  4237  xpeq12d  4297  poinxp  4336  eqbrrdv  4364  nfimad  4604  cnvexg  4782  funprg  4875  funtpg  4876  funimaexglem  4908  funfni  4925  fnunsn  4932  fnresdm  4934  fn0  4944  fssxp  4983  fconstg  5008  fconst6g  5010  resdif  5073  nffvd  5112  sefvex  5121  feqresmpt  5152  fvelimab  5154  fvmptd  5178  fvmpt2d  5182  fvmptdf  5183  fvmptt  5187  eqfnfvd  5193  fnreseql  5202  fimacnv  5221  dff3im  5237  foco2  5243  ffvresb  5253  f1oresrab  5254  fmptco  5255  fmptapd  5279  fsnunf  5287  fconst3m  5305  fnex  5308  fcof1  5348  fcofo  5349  cocan1  5352  cocan2  5353  foeqcnvco  5355  f1eqcocnv  5356  fliftrel  5357  fliftel  5358  fliftel1  5359  fliftval  5365  isocnv2  5377  isores2  5378  isotr  5381  f1oiso2  5391  riotass2  5418  riotass  5419  oveq12d  5454  ovprc  5463  ovresd  5564  suppssov1  5632  offval  5642  ofrfval  5643  fnofval  5644  ofrval  5645  ofmresval  5646  offval2  5649  ofrfval2  5650  ofco  5652  caofinvl  5656  cofunexg  5661  fnexALT  5663  opabex3d  5671  oprabexd  5677  ofmresex  5687  xpopth  5725  eqop  5726  2nd1st  5729  2ndrn  5732  elopabi  5744  mpt2fvex  5752  oprab2co  5762  1stconst  5765  2ndconst  5766  cnvf1olem  5768  tposexg  5795  tposf2  5805  tposf12  5806  smoiso  5839  tfrlem1  5845  tfrlem5  5852  tfrlemisucaccv  5860  tfrlemibacc  5861  tfrlemibxssdm  5862  tfrlemibfn  5863  tfrlemi14d  5868  tfrlemi14  5869  tfrexlem  5870  rdgivallem  5888  frecabex  5899  frecsuclem3  5906  frecrdg  5908  sucinc2  5941  oav2  5958  omv2  5960  omsuc  5966  nnsucsssuc  5986  nnaordi  5992  nnaword  5995  nnmord  6001  nnmword  6002  nnaordex  6011  ercl  6028  ersym  6029  ertr  6032  swoer  6045  swoord1  6046  swoord2  6047  erth  6061  eroprf  6110  ecopovtrn  6114  ecopovtrng  6117  th3qlem1  6119  ecovicom  6125  ecoviass  6127  ecovidi  6129  dfplpq2  6213  addcmpblnq  6226  addpipqqslem  6228  mulpipq2  6230  addcomnqg  6240  addassnqg  6241  distrnqg  6246  nqtri3or  6255  ltsonq  6257  ltanqg  6259  ltexnqq  6266  halfnqq  6267  subhalfnqq  6271  archnqq  6274  prarloclemarch  6275  prarloclemarch2  6276  ltrnqg  6277  enq0tr  6289  nqnq0pi  6293  addcmpblnq0  6298  nnnq0lem1  6301  nqpnq0nq  6308  nqnq0a  6309  nqnq0m  6310  distrnq0  6314  mulcomnq0  6315  addassnq0lemcl  6316  addassnq0  6317  preqlu  6326  prltlu  6341  prarloclemlt  6347  prarloclemlo  6348  prarloclem5  6354  prarloclemcalc  6356  prarloc  6357  genplt2i  6364  genpassg  6381  addnqprllem  6382  addnqprulem  6383  addnqprl  6384  addnqpru  6385  addlocprlemeqgt  6387  addlocprlemgt  6389  addlocprlem  6390  appdivnq  6407  prmuloclemcalc  6409  prmuloc  6410  prmuloc2  6411  mulnqprl  6412  mulnqpru  6413  mullocprlem  6414  mullocpr  6415  distrlem4prl  6423  distrlem4pru  6424  distrlem5prl  6425  distrlem5pru  6426  distrprg  6427  ltprordil  6428  1idprl  6429  1idpru  6430  ltexprlemm  6437  ltexprlemopl  6438  ltexprlemlol  6439  ltexprlemopu  6440  ltexprlemupu  6441  ltexprlemloc  6444  ltexprlemfl  6446  ltexprlemrl  6447  ltexprlemfu  6448  ltexprlemru  6449  ltexpri  6450  addcanprleml  6451  addcanprlemu  6452  ltaprlem  6454  ltaprg  6455  recexprlemm  6458  recexprlemdisj  6464  recexprlemloc  6465  recexprlem1ssl  6467  recexprlem1ssu  6468  recexpr  6472  addcmpblnr  6486  mulcmpblnrlemg  6487  mulcmpblnr  6488  prsrlem1  6489  ltsrprg  6494  mulcomsrg  6504  mulasssrg  6505  distrsrg  6506  lttrsr  6509  ltsosr  6511  ltasrg  6517  pn0sr  6518  negexsr  6519  recexsrlem  6520  mulgt0sr  6522  addcnsr  6545  mulcnsr  6546  addcnsrec  6553  mulcnsrec  6554  axaddcl  6560  axmulcl  6562  axmulcom  6565  axmulass  6567  axdistr  6568  axrnegex  6573  axcnre  6575  addcld  6648  mulcld  6649  mulcomd  6650  readdcld  6656  remulcld  6657  gtned  6721  lenltd  6723  ltled  6724  readdcan  6740  addcomd  6751  cnegex  6776  negeu  6789  addsubass  6808  subsub2  6825  subsub4  6830  negcon1d  6902  neg11ad  6904  subcld  6908  pncand  6909  pncan2d  6910  pncan3d  6911  npcand  6912  nncand  6913  negsubd  6914  subnegd  6915  subeq0d  6916  subne0d  6917  subeq0ad  6918  negdid  6921  negdi2d  6922  negsubdid  6923  negsubdi2d  6924  neg2subd  6925  resubcld  6965  mulneg1d  6994  mulneg2d  6995  mul2negd  6996  spimd  7012  bdssexd  7128
  Copyright terms: Public domain W3C validator