ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  syl2anc 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  700  syl13anc  1137  syl31anc  1138  nford  1459  eqeq12d  2054  rsp2e  2369  r19.29d2r  2452  elrab3t  2694  eueq2dc  2711  csbiedf  2884  sstrd  2952  psstrd  3049  sspsstrd  3050  psssstrd  3051  uneq12d  3095  unssd  3116  ineq12d  3136  ssind  3158  preq12d  3452  opeq12d  3554  nfopd  3563  breq12d  3774  mpteq12dva  3835  ssexd  3894  exss  3960  opexg  3961  opth  3971  op1stbg  4197  onintexmid  4282  tfisi  4288  xpeq12d  4348  poinxp  4387  eqbrrdv  4415  nfimad  4655  cnvexg  4833  funprg  4927  funtpg  4928  funimaexglem  4960  funfni  4977  fnunsn  4984  fnresdm  4986  fn0  4996  fssd  5033  fssxp  5036  fconstg  5061  fconst6g  5063  resdif  5126  nffvd  5165  sefvex  5174  feqresmpt  5205  fvelimab  5207  fvmptd  5231  fvmpt2d  5235  fvmptdf  5236  fvmptt  5240  eqfnfvd  5246  fnreseql  5255  fimacnv  5274  dff3im  5290  foco2  5296  ffvresb  5306  f1oresrab  5307  fmptco  5308  fmptapd  5332  fsnunf  5340  fconst3m  5358  fnex  5361  fcof1  5401  fcofo  5402  cocan1  5405  cocan2  5406  foeqcnvco  5408  f1eqcocnv  5409  fliftrel  5410  fliftel  5411  fliftel1  5412  fliftval  5418  isocnv2  5430  isores2  5431  isotr  5434  f1oiso2  5444  riotass2  5472  riotass  5473  oveq12d  5508  ovexg  5517  ovprc  5518  ovresd  5619  suppssov1  5687  offval  5697  ofrfval  5698  fnofval  5699  ofrval  5700  ofmresval  5701  offval2  5704  ofrfval2  5705  ofco  5707  caofinvl  5711  cofunexg  5716  fnexALT  5718  opabex3d  5726  oprabexd  5732  ofmresex  5742  xpopth  5780  eqop  5781  2nd1st  5784  2ndrn  5787  elopabi  5799  mpt2fvex  5807  oprab2co  5817  1stconst  5820  2ndconst  5821  cnvf1olem  5823  tposexg  5851  tposf2  5861  tposf12  5862  smoiso  5895  tfrlem1  5901  tfrlem5  5908  tfr0  5915  tfrlemisucaccv  5917  tfrlemibacc  5918  tfrlemibxssdm  5919  tfrlemibfn  5920  tfrlemi14d  5925  tfrexlem  5926  rdgivallem  5946  frecsuclem3  5968  frecrdg  5970  freccl  5971  sucinc2  6004  oav2  6021  omv2  6023  omsuc  6029  nnsucsssuc  6049  nndifsnid  6058  nnaordi  6059  nnaword  6062  nnmord  6068  nnmword  6069  nnaordex  6078  ercl  6095  ersym  6096  ertr  6099  swoer  6112  swoord1  6113  swoord2  6114  erth  6128  eroprf  6177  ecopovtrn  6181  ecopovtrng  6184  th3qlem1  6186  ecovicom  6192  ecoviass  6194  ecovidi  6196  f1oen2g  6213  fndmeng  6267  xpsnen2g  6281  xpdom1g  6285  xpdom3m  6286  fopwdom  6288  phplem4dom  6302  phpm  6305  phplem4on  6307  fidceq  6308  fidifsnen  6309  dif1en  6315  fisbth  6318  diffisn  6327  diffifi  6328  ac6sfi  6329  fientri3  6330  cardval3ex  6337  dfplpq2  6424  addcmpblnq  6437  addpipqqslem  6439  mulpipq2  6441  addcomnqg  6451  addassnqg  6452  distrnqg  6457  nqtri3or  6466  ltsonq  6468  ltanqg  6470  ltexnqq  6478  halfnqq  6480  subhalfnqq  6484  archnqq  6487  prarloclemarch  6488  prarloclemarch2  6489  ltrnqg  6490  enq0tr  6504  nqnq0pi  6508  addcmpblnq0  6513  nnnq0lem1  6516  nqpnq0nq  6523  nqnq0a  6524  nqnq0m  6525  distrnq0  6529  mulcomnq0  6530  addassnq0lemcl  6531  addassnq0  6532  preqlu  6542  prltlu  6557  prarloclemlt  6563  prarloclemlo  6564  prarloclem5  6570  prarloclemcalc  6572  prarloc  6573  genplt2i  6580  genpassg  6596  addnqprllem  6597  addnqprulem  6598  addnqprl  6599  addnqpru  6600  addlocprlemeqgt  6602  addlocprlemgt  6604  addlocprlem  6605  nqprl  6621  nqpru  6622  addnqprlemrl  6627  addnqprlemru  6628  addnqpr  6631  appdivnq  6633  prmuloclemcalc  6635  prmuloc  6636  prmuloc2  6637  mulnqprl  6638  mulnqpru  6639  mullocprlem  6640  mullocpr  6641  mulnqprlemrl  6643  mulnqprlemru  6644  mulnqpr  6647  distrlem4prl  6654  distrlem4pru  6655  distrlem5prl  6656  distrlem5pru  6657  distrprg  6658  ltprordil  6659  1idprl  6660  1idpru  6661  ltnqpri  6664  ltexprlemm  6670  ltexprlemopl  6671  ltexprlemlol  6672  ltexprlemopu  6673  ltexprlemupu  6674  ltexprlemloc  6677  ltexprlemfl  6679  ltexprlemrl  6680  ltexprlemfu  6681  ltexprlemru  6682  ltexpri  6683  addcanprleml  6684  addcanprlemu  6685  ltaprlem  6688  ltaprg  6689  prplnqu  6690  addextpr  6691  recexprlemm  6694  recexprlemdisj  6700  recexprlemloc  6701  recexprlem1ssl  6703  recexprlem1ssu  6704  recexpr  6708  aptiprleml  6709  aptiprlemu  6710  ltmprr  6712  archpr  6713  caucvgprlemcanl  6714  cauappcvgprlemm  6715  cauappcvgprlemopl  6716  cauappcvgprlemopu  6718  cauappcvgprlemdisj  6721  cauappcvgprlemloc  6722  cauappcvgprlemladdfu  6724  cauappcvgprlemladdfl  6725  cauappcvgprlemladdru  6726  cauappcvgprlemladdrl  6727  cauappcvgprlemladd  6728  cauappcvgprlem1  6729  cauappcvgprlem2  6730  cauappcvgpr  6732  archrecpr  6734  caucvgprlemk  6735  caucvgprlemnkj  6736  caucvgprlemnbj  6737  caucvgprlemm  6738  caucvgprlemopl  6739  caucvgprlemopu  6741  caucvgprlemloc  6745  caucvgprlemladdfu  6747  caucvgprlemladdrl  6748  caucvgprlem1  6749  caucvgprlem2  6750  caucvgpr  6752  caucvgprprlemk  6753  caucvgprprlemloccalc  6754  caucvgprprlemnkltj  6759  caucvgprprlemnkeqj  6760  caucvgprprlemnjltk  6761  caucvgprprlemnkj  6762  caucvgprprlemnbj  6763  caucvgprprlemml  6764  caucvgprprlemmu  6765  caucvgprprlemopl  6767  caucvgprprlemopu  6769  caucvgprprlemloc  6773  caucvgprprlemexbt  6776  caucvgprprlemexb  6777  caucvgprprlemaddq  6778  caucvgprprlem1  6779  caucvgprprlem2  6780  caucvgprpr  6782  addcmpblnr  6796  mulcmpblnrlemg  6797  mulcmpblnr  6798  prsrlem1  6799  ltsrprg  6804  mulcomsrg  6814  mulasssrg  6815  distrsrg  6816  lttrsr  6819  ltsosr  6821  ltasrg  6827  pn0sr  6828  negexsr  6829  recexgt0sr  6830  mulgt0sr  6834  aptisr  6835  mulextsr1lem  6836  mulextsr1  6837  archsr  6838  srpospr  6839  prsradd  6842  prsrlt  6843  prsrriota  6844  caucvgsrlemcl  6845  caucvgsrlemfv  6847  caucvgsrlemcau  6849  caucvgsrlemgt1  6851  caucvgsrlemoffval  6852  caucvgsrlemofff  6853  caucvgsrlemoffcau  6854  caucvgsrlemoffgt1  6855  caucvgsrlemoffres  6856  addcnsr  6882  mulcnsr  6883  addcnsrec  6890  mulcnsrec  6891  ltrennb  6902  recidpipr  6904  recidpirqlemcalc  6905  recidpirq  6906  axaddcl  6912  axmulcl  6914  axmulcom  6917  axmulass  6919  axdistr  6920  axrnegex  6925  axcnre  6927  rereceu  6935  recriota  6936  nntopi  6940  axcaucvglemval  6943  axcaucvglemcau  6944  axcaucvglemres  6945  addcld  7018  mulcld  7019  mulcomd  7020  readdcld  7026  remulcld  7027  lelttr  7077  ltletr  7078  gtned  7101  lttri3d  7103  letri3d  7104  lenltd  7105  ltled  7106  readdcan  7124  addcomd  7135  cnegex  7160  negeu  7173  addsubass  7192  subsub2  7209  subsub4  7214  negcon1d  7286  neg11ad  7288  subcld  7292  pncand  7293  pncan2d  7294  pncan3d  7295  npcand  7296  nncand  7297  negsubd  7298  subnegd  7299  subeq0d  7300  subne0d  7301  subeq0ad  7302  negdid  7305  negdi2d  7306  negsubdid  7307  negsubdi2d  7308  neg2subd  7309  resubcld  7349  mulneg1d  7378  mulneg2d  7379  mul2negd  7380  ltadd2  7386  posdif  7419  add20  7438  ltnegd  7483  lenegd  7484  ltnegcon1d  7485  ltnegcon2d  7486  lenegcon1d  7487  lenegcon2d  7488  ltaddposd  7489  ltaddpos2d  7490  ltsubposd  7491  posdifd  7492  addge01d  7493  addge02d  7494  subge0d  7495  suble0d  7496  subge02d  7497  rimul  7543  rereim  7544  apreap  7545  reapmul1lem  7552  reapmul1  7553  reapadd1  7554  reapneg  7555  remulext1  7557  cru  7560  apreim  7561  apsym  7564  addext  7568  apneg  7569  mulext1  7570  mulext  7572  apti  7580  leltap  7582  gt0ap0d  7586  ltap  7589  ltapd  7594  ap0gt0d  7597  recexaplem2  7600  recexap  7601  mulap0bd  7605  mulcanapd  7609  muleqadd  7616  receuap  7617  divmulap  7621  divdivdivap  7656  divcanap6  7662  recclapd  7724  recap0d  7725  recidapd  7726  recidap2d  7727  recrecapd  7728  dividapd  7729  div0apd  7730  rerecclapd  7774  recgt0  7783  prodgt0  7785  lt2msq  7819  lediv12a  7827  lediv2a  7828  recreclt  7833  recgt0d  7867  creui  7879  nnge1  7904  nnaddcld  7928  nnmulcld  7929  nndivred  7930  halfaddsub  8123  lt2halves  8124  addltmul  8125  nn0addcld  8202  nn0mulcld  8203  gtndiv  8298  zaddcld  8327  zsubcld  8328  zmulcld  8329  uzneg  8454  uzm1  8466  uzin  8468  uzind4  8494  qmulcl  8535  qapne  8537  rpaddcld  8600  rpmulcld  8601  rpdivcld  8602  ltrecd  8603  lerecd  8604  ltrec1d  8605  lerec2d  8606  ge0p1rpd  8611  rerpdivcld  8612  ltsubrpd  8613  ltaddrpd  8614  xrlelttr  8680  xrltletr  8681  ixxdisj  8730  ixxss1  8731  ixxss2  8732  iccsupr  8793  icoshft  8816  icoshftf1o  8817  icodisj  8818  elfz1eq  8857  fzen  8865  fzsplit  8873  elfz1end  8877  fznatpl1  8896  fzdifsuc  8901  uzdisj  8913  fseq1p1m1  8914  fzm1  8920  fzneuz  8921  fznuz  8922  uznfz  8923  fznn0sub2  8943  nn0disj  8953  elfzoelz  8962  elfzouz2  8975  fzonnsub  8983  fzospliti  8990  fzosplit  8991  fzodisj  8992  elfzo1  9004  eluzgtdifelfzo  9011  fzocatel  9013  zpnn0elfzo  9021  fzostep1  9051  frec2uzsucd  9056  frec2uzltd  9058  frec2uzlt2d  9059  frecuzrdgrrn  9063  frec2uzrdg  9064  frecuzrdgrom  9065  frecuzrdglem  9066  frecuzrdg0  9069  frecuzrdgsuc  9070  frecfzen2  9073  fzfig  9075  fzfigd  9076  iseqeq3  9085  iseqm1  9096  iseqfveq2  9097  iseqfeq2  9098  iseqshft2  9101  monoord  9104  monoord2  9105  iseqsplit  9107  iseqcaopr3  9109  iseqid  9116  iseqhomo  9117  iseqdistr  9118  expivallem  9125  expival  9126  expcl2lemap  9136  expap0  9154  expgt1  9162  mulexp  9163  mulexpzap  9164  expadd  9166  expaddzaplem  9167  expaddzap  9168  expmulzap  9170  ltexp2a  9175  leexp2a  9176  leexp2r  9177  bernneq  9238  expnbnd  9241  expnlbnd  9242  expnlbnd2  9243  expeq0d  9246  expcld  9250  expp1d  9251  sqrecapd  9254  sqmuld  9262  reexpcld  9267  nnexpcld  9271  nn0expcld  9272  rpexpcld  9273  sqgt0apd  9277  shftfvalg  9288  shftfval  9291  shftval2  9296  shftval5  9299  crre  9326  remim  9329  mulreap  9333  recj  9336  reneg  9337  readd  9338  remullem  9340  imcj  9344  imneg  9345  imadd  9346  cjexp  9362  cjap  9375  cjdivap  9378  cnrecnv  9379  cjexpd  9427  readdd  9428  imaddd  9429  resubd  9430  imsubd  9431  remuld  9432  immuld  9433  cjaddd  9434  cjmuld  9435  ipcnd  9436  remul2d  9441  immul2d  9442  crred  9445  crimd  9446  caucvgrelemcau  9448  caucvgre  9449  cvg1nlemcau  9452  cvg1nlemres  9453  recvguniq  9462  resqrexlemover  9477  resqrexlemdecn  9479  resqrexlemcalc1  9481  resqrexlemcalc2  9482  resqrexlemnmsq  9484  resqrexlemnm  9485  resqrexlemcvg  9486  resqrexlemoverl  9488  resqrexlemglsq  9489  resqrexlemga  9490  resqrtcl  9496  rersqrtthlem  9497  sqrtmul  9502  rpsqrtcl  9508  sqrtdiv  9509  abscl  9518  absvalsq  9520  absge0  9527  abs00ap  9529  absreim  9535  absdivap  9537  leabs  9541  absexp  9544  absexpzap  9545  sqabs  9547  ltabs  9552  abslt  9553  absle  9554  abssubap0  9555  abssubne0  9556  absidm  9563  abssubge0  9567  abstri  9569  abs3dif  9570  abs2difabs  9573  fzomaxdiflem  9577  caubnd2  9582  amgm2  9583  absnidd  9625  resqrtcld  9628  sqrtmsqd  9629  sqrtsqd  9630  sqrtge0d  9631  absidd  9632  absltd  9639  absled  9640  absrpclapd  9653  absexpd  9657  abssubd  9658  absmuld  9659  abstrid  9661  abs2difd  9662  abs2dif2d  9663  abs2difabsd  9664  climconst  9679  climuni  9682  climmpt  9689  climshft  9693  climshft2  9695  climcn2  9698  mulcn2  9701  cn1lem  9702  cjcn2  9704  climrecl  9712  climle  9722  iserile  9730  climcau  9734  climcvg1nlem  9736  serif0  9739  nn0seqcvgd  9748  ialgr0  9751  ialgrp1  9753  ialgcvg  9755  algcvgb  9757  spimd  9769  bdssexd  9889
  Copyright terms: Public domain W3C validator