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  699  syl13anc  1136  syl31anc  1137  nford  1456  eqeq12d  2051  rsp2e  2366  r19.29d2r  2449  elrab3t  2691  eueq2dc  2708  csbiedf  2881  sstrd  2949  psstrd  3046  sspsstrd  3047  psssstrd  3048  uneq12d  3092  unssd  3113  ineq12d  3133  ssind  3155  preq12d  3446  opeq12d  3548  nfopd  3557  breq12d  3768  mpteq12dva  3829  ssexd  3888  exss  3954  opexg  3955  opth  3965  op1stbg  4176  tfisi  4253  xpeq12d  4313  poinxp  4352  eqbrrdv  4380  nfimad  4620  cnvexg  4798  funprg  4892  funtpg  4893  funimaexglem  4925  funfni  4942  fnunsn  4949  fnresdm  4951  fn0  4961  fssd  4998  fssxp  5001  fconstg  5026  fconst6g  5028  resdif  5091  nffvd  5130  sefvex  5139  feqresmpt  5170  fvelimab  5172  fvmptd  5196  fvmpt2d  5200  fvmptdf  5201  fvmptt  5205  eqfnfvd  5211  fnreseql  5220  fimacnv  5239  dff3im  5255  foco2  5261  ffvresb  5271  f1oresrab  5272  fmptco  5273  fmptapd  5297  fsnunf  5305  fconst3m  5323  fnex  5326  fcof1  5366  fcofo  5367  cocan1  5370  cocan2  5371  foeqcnvco  5373  f1eqcocnv  5374  fliftrel  5375  fliftel  5376  fliftel1  5377  fliftval  5383  isocnv2  5395  isores2  5396  isotr  5399  f1oiso2  5409  riotass2  5437  riotass  5438  oveq12d  5473  ovprc  5482  ovresd  5583  suppssov1  5651  offval  5661  ofrfval  5662  fnofval  5663  ofrval  5664  ofmresval  5665  offval2  5668  ofrfval2  5669  ofco  5671  caofinvl  5675  cofunexg  5680  fnexALT  5682  opabex3d  5690  oprabexd  5696  ofmresex  5706  xpopth  5744  eqop  5745  2nd1st  5748  2ndrn  5751  elopabi  5763  mpt2fvex  5771  oprab2co  5781  1stconst  5784  2ndconst  5785  cnvf1olem  5787  tposexg  5814  tposf2  5824  tposf12  5825  smoiso  5858  tfrlem1  5864  tfrlem5  5871  tfr0  5878  tfrlemisucaccv  5880  tfrlemibacc  5881  tfrlemibxssdm  5882  tfrlemibfn  5883  tfrlemi14d  5888  tfrexlem  5889  rdgivallem  5908  frecsuclem3  5929  frecrdg  5931  freccl  5932  sucinc2  5965  oav2  5982  omv2  5984  omsuc  5990  nnsucsssuc  6010  nnaordi  6017  nnaword  6020  nnmord  6026  nnmword  6027  nnaordex  6036  ercl  6053  ersym  6054  ertr  6057  swoer  6070  swoord1  6071  swoord2  6072  erth  6086  eroprf  6135  ecopovtrn  6139  ecopovtrng  6142  th3qlem1  6144  ecovicom  6150  ecoviass  6152  ecovidi  6154  f1oen2g  6171  fndmeng  6225  xpsnen2g  6239  xpdom1g  6243  xpdom3m  6244  fopwdom  6246  dfplpq2  6338  addcmpblnq  6351  addpipqqslem  6353  mulpipq2  6355  addcomnqg  6365  addassnqg  6366  distrnqg  6371  nqtri3or  6380  ltsonq  6382  ltanqg  6384  ltexnqq  6391  halfnqq  6393  subhalfnqq  6397  archnqq  6400  prarloclemarch  6401  prarloclemarch2  6402  ltrnqg  6403  enq0tr  6417  nqnq0pi  6421  addcmpblnq0  6426  nnnq0lem1  6429  nqpnq0nq  6436  nqnq0a  6437  nqnq0m  6438  distrnq0  6442  mulcomnq0  6443  addassnq0lemcl  6444  addassnq0  6445  preqlu  6455  prltlu  6470  prarloclemlt  6476  prarloclemlo  6477  prarloclem5  6483  prarloclemcalc  6485  prarloc  6486  genplt2i  6493  genpassg  6509  addnqprllem  6510  addnqprulem  6511  addnqprl  6512  addnqpru  6513  addlocprlemeqgt  6515  addlocprlemgt  6517  addlocprlem  6518  nqprl  6533  addnqprlemrl  6538  addnqprlemru  6539  addnqpr  6542  appdivnq  6544  prmuloclemcalc  6546  prmuloc  6547  prmuloc2  6548  mulnqprl  6549  mulnqpru  6550  mullocprlem  6551  mullocpr  6552  distrlem4prl  6560  distrlem4pru  6561  distrlem5prl  6562  distrlem5pru  6563  distrprg  6564  ltprordil  6565  1idprl  6566  1idpru  6567  ltexprlemm  6574  ltexprlemopl  6575  ltexprlemlol  6576  ltexprlemopu  6577  ltexprlemupu  6578  ltexprlemloc  6581  ltexprlemfl  6583  ltexprlemrl  6584  ltexprlemfu  6585  ltexprlemru  6586  ltexpri  6587  addcanprleml  6588  addcanprlemu  6589  ltaprlem  6591  ltaprg  6592  addextpr  6593  recexprlemm  6596  recexprlemdisj  6602  recexprlemloc  6603  recexprlem1ssl  6605  recexprlem1ssu  6606  recexpr  6610  aptiprleml  6611  aptiprlemu  6612  ltmprr  6614  archpr  6615  cauappcvgprlemcan  6616  cauappcvgprlemm  6617  cauappcvgprlemopl  6618  cauappcvgprlemopu  6620  cauappcvgprlemdisj  6623  cauappcvgprlemloc  6624  cauappcvgprlemladdfu  6626  cauappcvgprlemladdfl  6627  cauappcvgprlemladdru  6628  cauappcvgprlemladdrl  6629  cauappcvgprlemladd  6630  cauappcvgprlem1  6631  cauappcvgprlem2  6632  cauappcvgpr  6634  caucvgprlemk  6636  caucvgprlemnkj  6637  caucvgprlemnbj  6638  caucvgprlemm  6639  caucvgprlemopl  6640  caucvgprlemopu  6642  caucvgprlemloc  6646  caucvgprlemladdfu  6648  caucvgprlemladdrl  6649  caucvgprlem1  6650  caucvgprlem2  6651  caucvgpr  6653  addcmpblnr  6667  mulcmpblnrlemg  6668  mulcmpblnr  6669  prsrlem1  6670  ltsrprg  6675  mulcomsrg  6685  mulasssrg  6686  distrsrg  6687  lttrsr  6690  ltsosr  6692  ltasrg  6698  pn0sr  6699  negexsr  6700  recexgt0sr  6701  mulgt0sr  6704  aptisr  6705  mulextsr1lem  6706  mulextsr1  6707  archsr  6708  addcnsr  6731  mulcnsr  6732  addcnsrec  6739  mulcnsrec  6740  axaddcl  6750  axmulcl  6752  axmulcom  6755  axmulass  6757  axdistr  6758  axrnegex  6763  axcnre  6765  addcld  6844  mulcld  6845  mulcomd  6846  readdcld  6852  remulcld  6853  lelttr  6903  ltletr  6904  gtned  6927  lttri3d  6929  letri3d  6930  lenltd  6931  ltled  6932  readdcan  6950  addcomd  6961  cnegex  6986  negeu  6999  addsubass  7018  subsub2  7035  subsub4  7040  negcon1d  7112  neg11ad  7114  subcld  7118  pncand  7119  pncan2d  7120  pncan3d  7121  npcand  7122  nncand  7123  negsubd  7124  subnegd  7125  subeq0d  7126  subne0d  7127  subeq0ad  7128  negdid  7131  negdi2d  7132  negsubdid  7133  negsubdi2d  7134  neg2subd  7135  resubcld  7175  mulneg1d  7204  mulneg2d  7205  mul2negd  7206  ltadd2  7212  posdif  7245  add20  7264  ltnegd  7309  lenegd  7310  ltnegcon1d  7311  ltnegcon2d  7312  lenegcon1d  7313  lenegcon2d  7314  ltaddposd  7315  ltaddpos2d  7316  ltsubposd  7317  posdifd  7318  addge01d  7319  addge02d  7320  subge0d  7321  suble0d  7322  subge02d  7323  rimul  7369  rereim  7370  apreap  7371  reapmul1lem  7378  reapmul1  7379  reapadd1  7380  reapneg  7381  remulext1  7383  cru  7386  apreim  7387  apsym  7390  addext  7394  apneg  7395  mulext1  7396  mulext  7398  apti  7406  gt0ap0d  7411  recexaplem2  7415  recexap  7416  mulap0bd  7420  mulcanapd  7424  muleqadd  7431  receuap  7432  divmulap  7436  divdivdivap  7471  divcanap6  7477  recclapd  7539  recap0d  7540  recidapd  7541  recidap2d  7542  recrecapd  7543  dividapd  7544  div0apd  7545  rerecclapd  7588  recgt0  7597  prodgt0  7599  lt2msq  7633  lediv12a  7641  lediv2a  7642  recreclt  7647  recgt0d  7681  creui  7693  nnge1  7718  nnaddcld  7741  nnmulcld  7742  nndivred  7743  halfaddsub  7936  lt2halves  7937  addltmul  7938  nn0addcld  8015  nn0mulcld  8016  gtndiv  8111  zaddcld  8140  zsubcld  8141  zmulcld  8142  uzneg  8267  uzm1  8279  uzin  8281  uzind4  8307  qmulcl  8348  qapne  8350  rpaddcld  8412  rpmulcld  8413  rpdivcld  8414  ltrecd  8415  lerecd  8416  ltrec1d  8417  lerec2d  8418  ge0p1rpd  8423  rerpdivcld  8424  ltsubrpd  8425  ltaddrpd  8426  xrlelttr  8492  xrltletr  8493  ixxdisj  8542  ixxss1  8543  ixxss2  8544  iccsupr  8605  icoshft  8628  icoshftf1o  8629  icodisj  8630  elfz1eq  8669  fzen  8677  fzsplit  8685  elfz1end  8689  fznatpl1  8708  fzdifsuc  8713  uzdisj  8725  fseq1p1m1  8726  fzm1  8732  fzneuz  8733  fznuz  8734  uznfz  8735  fznn0sub2  8755  nn0disj  8765  elfzoelz  8774  elfzouz2  8787  fzonnsub  8795  fzospliti  8802  fzosplit  8803  fzodisj  8804  elfzo1  8816  eluzgtdifelfzo  8823  fzocatel  8825  zpnn0elfzo  8833  fzostep1  8863  frec2uzsucd  8868  frec2uzltd  8870  frec2uzlt2d  8871  frecuzrdgrrn  8875  frec2uzrdg  8876  frecuzrdgrom  8877  frecuzrdglem  8878  frecuzrdg0  8881  frecuzrdgsuc  8882  frecfzen2  8885  fzfig  8887  fzfigd  8888  iseqeq3  8896  iseqfveq2  8905  iseqfeq2  8906  expivallem  8910  expival  8911  expcl2lemap  8921  expap0  8939  expgt1  8947  mulexp  8948  mulexpzap  8949  expadd  8951  expaddzaplem  8952  expaddzap  8953  expmulzap  8955  ltexp2a  8960  leexp2a  8961  leexp2r  8962  bernneq  9022  expnbnd  9025  expnlbnd  9026  expnlbnd2  9027  expeq0d  9030  expcld  9034  expp1d  9035  sqrecapd  9038  sqmuld  9046  reexpcld  9051  nnexpcld  9055  nn0expcld  9056  rpexpcld  9057  sqgt0apd  9061  crre  9085  remim  9088  mulreap  9092  recj  9095  reneg  9096  readd  9097  remullem  9099  imcj  9103  imneg  9104  imadd  9105  cjexp  9121  cjap  9134  cjdivap  9137  cnrecnv  9138  cjexpd  9185  readdd  9186  imaddd  9187  resubd  9188  imsubd  9189  remuld  9190  immuld  9191  cjaddd  9192  cjmuld  9193  ipcnd  9194  remul2d  9199  immul2d  9200  crred  9203  crimd  9204  spimd  9240  bdssexd  9360
  Copyright terms: Public domain W3C validator