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

Theorem syl2anc 391
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  392  sylancr  393  sylancom  397  mpdan  398  mpancom  399  orim12d  684  syl13anc  1118  syl31anc  1119  nford  1433  eqeq12d  2028  rsp2e  2342  r19.29d2r  2425  elrab3t  2666  eueq2dc  2683  csbiedf  2856  sstrd  2924  psstrd  3021  sspsstrd  3022  psssstrd  3023  uneq12d  3067  unssd  3088  ineq12d  3108  ssind  3130  preq12d  3419  opeq12d  3521  nfopd  3530  breq12d  3741  mpteq12dva  3802  ssexd  3861  exss  3927  opexg  3928  opth  3938  op1stbg  4149  tfisi  4226  xpeq12d  4286  poinxp  4325  eqbrrdv  4353  nfimad  4593  cnvexg  4771  funprg  4864  funtpg  4865  funimaexglem  4897  funfni  4914  fnunsn  4921  fnresdm  4923  fn0  4933  fssxp  4972  fconstg  4997  fconst6g  4999  resdif  5062  nffvd  5101  sefvex  5110  feqresmpt  5141  fvelimab  5143  fvmptd  5167  fvmpt2d  5171  fvmptdf  5172  fvmptt  5176  eqfnfvd  5182  fnreseql  5191  fimacnv  5210  dff3im  5226  foco2  5232  ffvresb  5242  f1oresrab  5243  fmptco  5244  fmptapd  5268  fsnunf  5276  fconst3m  5294  fnex  5297  fcof1  5337  fcofo  5338  cocan1  5341  cocan2  5342  foeqcnvco  5344  f1eqcocnv  5345  fliftrel  5346  fliftel  5347  fliftel1  5348  fliftval  5354  isocnv2  5366  isores2  5367  isotr  5370  f1oiso2  5380  riotass2  5407  riotass  5408  oveq12d  5443  ovprc  5452  ovresd  5553  suppssov1  5621  offval  5631  ofrfval  5632  fnofval  5633  ofrval  5634  ofmresval  5635  offval2  5638  ofrfval2  5639  ofco  5641  caofinvl  5645  cofunexg  5650  fnexALT  5652  opabex3d  5660  oprabexd  5666  ofmresex  5676  xpopth  5714  eqop  5715  2nd1st  5718  2ndrn  5721  elopabi  5733  mpt2fvex  5741  oprab2co  5751  1stconst  5754  2ndconst  5755  cnvf1olem  5757  tposexg  5784  tposf2  5794  tposf12  5795  smoiso  5828  tfrlem1  5834  tfrlem5  5841  tfrlemisucaccv  5849  tfrlemibacc  5850  tfrlemibxssdm  5851  tfrlemibfn  5852  tfrlemi14d  5857  tfrlemi14  5858  tfrexlem  5859  rdgivallem  5877  frecabex  5888  frecsuclem3  5895  frecrdg  5897  sucinc2  5930  oav2  5947  omv2  5949  omsuc  5955  nnsucsssuc  5975  nnaordi  5981  nnaword  5984  nnmord  5990  nnmword  5991  nnaordex  6000  ercl  6017  ersym  6018  ertr  6021  swoer  6034  swoord1  6035  swoord2  6036  erth  6050  eroprf  6099  ecopovtrn  6103  ecopovtrng  6106  th3qlem1  6108  ecovicom  6114  ecoviass  6116  ecovidi  6118  dfplpq2  6200  addcmpblnq  6213  addpipqqslem  6215  mulpipq2  6217  addcomnqg  6227  addassnqg  6228  distrnqg  6233  nqtri3or  6242  ltsonq  6244  ltanqg  6246  ltexnqq  6253  halfnqq  6254  subhalfnqq  6258  archnqq  6261  prarloclemarch  6262  prarloclemarch2  6263  ltrnqg  6264  enq0tr  6276  nqnq0pi  6280  addcmpblnq0  6285  nnnq0lem1  6288  nqpnq0nq  6295  nqnq0a  6296  nqnq0m  6297  distrnq0  6301  mulcomnq0  6302  addassnq0lemcl  6303  addassnq0  6304  preqlu  6313  prltlu  6328  prarloclemlt  6334  prarloclemlo  6335  prarloclem5  6341  prarloclemcalc  6343  prarloc  6344  genplt2i  6351  genpassg  6368  addnqprllem  6369  addnqprulem  6370  addnqprl  6371  addnqpru  6372  addlocprlemeqgt  6374  addlocprlemgt  6376  addlocprlem  6377  appdivnq  6394  prmuloclemcalc  6396  prmuloc  6397  prmuloc2  6398  mulnqprl  6399  mulnqpru  6400  mullocprlem  6401  mullocpr  6402  distrlem4prl  6410  distrlem4pru  6411  distrlem5prl  6412  distrlem5pru  6413  distrprg  6414  ltprordil  6415  1idprl  6416  1idpru  6417  ltexprlemm  6424  ltexprlemopl  6425  ltexprlemlol  6426  ltexprlemopu  6427  ltexprlemupu  6428  ltexprlemloc  6431  ltexprlemfl  6433  ltexprlemrl  6434  ltexprlemfu  6435  ltexprlemru  6436  ltexpri  6437  addcanprleml  6438  addcanprlemu  6439  ltaprlem  6441  ltaprg  6442  addextpr  6443  recexprlemm  6446  recexprlemdisj  6452  recexprlemloc  6453  recexprlem1ssl  6455  recexprlem1ssu  6456  recexpr  6460  aptiprleml  6461  aptiprlemu  6462  ltmprr  6464  addcmpblnr  6478  mulcmpblnrlemg  6479  mulcmpblnr  6480  prsrlem1  6481  ltsrprg  6486  mulcomsrg  6496  mulasssrg  6497  distrsrg  6498  lttrsr  6501  ltsosr  6503  ltasrg  6509  pn0sr  6510  negexsr  6511  recexgt0sr  6512  mulgt0sr  6515  aptisr  6516  mulextsr1lem  6517  mulextsr1  6518  addcnsr  6541  mulcnsr  6542  addcnsrec  6549  mulcnsrec  6550  axaddcl  6556  axmulcl  6558  axmulcom  6561  axmulass  6563  axdistr  6564  axrnegex  6569  axcnre  6571  addcld  6648  mulcld  6649  mulcomd  6650  readdcld  6656  remulcld  6657  lelttr  6707  ltletr  6708  gtned  6731  lttri3d  6733  letri3d  6734  lenltd  6735  ltled  6736  readdcan  6754  addcomd  6765  cnegex  6790  negeu  6803  addsubass  6822  subsub2  6839  subsub4  6844  negcon1d  6916  neg11ad  6918  subcld  6922  pncand  6923  pncan2d  6924  pncan3d  6925  npcand  6926  nncand  6927  negsubd  6928  subnegd  6929  subeq0d  6930  subne0d  6931  subeq0ad  6932  negdid  6935  negdi2d  6936  negsubdid  6937  negsubdi2d  6938  neg2subd  6939  resubcld  6979  mulneg1d  7008  mulneg2d  7009  mul2negd  7010  ltadd2  7016  posdif  7049  add20  7068  ltnegd  7113  lenegd  7114  ltnegcon1d  7115  ltnegcon2d  7116  lenegcon1d  7117  lenegcon2d  7118  ltaddposd  7119  ltaddpos2d  7120  ltsubposd  7121  posdifd  7122  addge01d  7123  addge02d  7124  subge0d  7125  suble0d  7126  subge02d  7127  rimul  7173  rereim  7174  apreap  7175  reapmul1lem  7182  reapmul1  7183  reapadd1  7184  reapneg  7185  remulext1  7187  cru  7190  apreim  7191  apsym  7194  addext  7198  apneg  7199  mulext1  7200  mulext  7202  apti  7210  gt0ap0d  7215  recexaplem2  7219  recexap  7220  mulap0bd  7224  mulcanapd  7228  muleqadd  7235  receuap  7236  divmulap  7240  divdivdivap  7275  divcanap6  7281  recclapd  7343  recap0d  7344  recidapd  7345  recidap2d  7346  recrecapd  7347  dividapd  7348  div0apd  7349  rerecclapd  7392  recgt0  7400  prodgt0  7402  lt2msq  7436  lediv12a  7444  lediv2a  7445  recreclt  7450  recgt0d  7484  creui  7496  nnge1  7521  nnaddcld  7544  nnmulcld  7545  nndivred  7546  halfaddsub  7738  lt2halves  7739  addltmul  7740  nn0addcld  7814  nn0mulcld  7815  gtndiv  7901  zaddcld  7929  zsubcld  7930  zmulcld  7931  qmulcl  8056  qapne  8058  rpaddcld  8119  rpmulcld  8120  rpdivcld  8121  ltrecd  8122  lerecd  8123  ltrec1d  8124  lerec2d  8125  ge0p1rpd  8130  rerpdivcld  8131  ltsubrpd  8132  ltaddrpd  8133  xrlelttr  8199  xrltletr  8200  spimd  8242  bdssexd  8358
  Copyright terms: Public domain W3C validator