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

Theorem syl2anc 403
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 113 . 2 (𝜓 → (𝜒𝜃))
51, 2, 4sylc 61 1 (𝜑𝜃)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 102
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia3 106
This theorem is referenced by:  sylancl  404  sylancr  405  sylancom  411  mpdan  412  mpancom  413  orim12d  733  syl13anc  1172  syl31anc  1173  mp3an2i  1274  nford  1500  eqeq12d  2096  rsp2e  2415  r19.29d2r  2500  elrab3t  2749  eueq2dc  2766  csbiedf  2944  sstrd  3010  uneq12d  3128  unssd  3149  ineq12d  3175  ssind  3197  preq12d  3485  opeq12d  3586  nfopd  3595  breq12d  3806  mpteq12dva  3867  ssexd  3926  exss  3990  opexg  3991  opth  4000  onintexmid  4323  wetriext  4327  tfisi  4336  xpeq12d  4396  poinxp  4435  eqbrrdv  4463  nfimad  4707  cnvexg  4885  funprg  4980  funtpg  4981  funimaexglem  5013  funfni  5030  fnunsn  5037  fnresdm  5039  fn0  5049  fssd  5086  fssxp  5089  fconstg  5114  fconst6g  5116  resdif  5179  nffvd  5218  sefvex  5227  feqresmpt  5259  fvelimab  5261  fvmptd  5285  fvmpt2d  5289  fvmptdf  5290  fvmptt  5294  eqfnfvd  5300  fnreseql  5309  fimacnv  5328  dff3im  5344  foco2  5350  ffvresb  5360  f1oresrab  5361  fmptco  5362  fmptapd  5386  fsnunf  5394  fconst3m  5412  fnex  5415  fcof1  5454  fcofo  5455  cocan1  5458  cocan2  5459  foeqcnvco  5461  f1eqcocnv  5462  fliftrel  5463  fliftel  5464  fliftel1  5465  fliftval  5471  isocnv2  5483  isores2  5484  isotr  5487  f1oiso2  5497  riotass2  5525  riotass  5526  oveq12d  5561  ovexg  5570  ovprc  5571  ovresd  5672  suppssov1  5740  offval  5750  ofrfval  5751  fnofval  5752  ofrval  5753  ofmresval  5754  offval2  5757  ofrfval2  5758  ofco  5760  caofinvl  5764  cofunexg  5769  fnexALT  5771  opabex3d  5779  oprabexd  5785  ofmresex  5795  xpopth  5833  eqop  5834  2nd1st  5837  2ndrn  5840  elopabi  5852  mpt2fvex  5860  oprab2co  5870  1stconst  5873  2ndconst  5874  cnvf1olem  5876  tposexg  5907  tposf2  5917  tposf12  5918  smoiso  5951  tfrlem1  5957  tfrlem5  5963  tfr0dm  5971  tfrlemisucaccv  5974  tfrlemibacc  5975  tfrlemibxssdm  5976  tfrlemibfn  5977  tfrlemi14d  5982  tfrexlem  5983  tfr1onlemsucfn  5989  tfr1onlemsucaccv  5990  tfr1onlembxssdm  5992  tfr1onlembfn  5993  tfr1onlembex  5994  tfr1onlemubacc  5995  tfr1onlemres  5998  tfrcllemsucfn  6002  tfrcllemsucaccv  6003  tfrcllembxssdm  6005  tfrcllembfn  6006  tfrcllembex  6007  tfrcllemubacc  6008  tfrcllemres  6011  tfrcl  6013  rdgivallem  6030  rdgon  6035  frecabcl  6048  frecsuclem  6055  frecrdg  6057  sucinc2  6090  oav2  6107  omv2  6109  omsuc  6116  nnsucsssuc  6136  nndifsnid  6146  nnaordi  6147  nnaword  6150  nnmord  6156  nnmword  6157  nnaordex  6166  ercl  6183  ersym  6184  ertr  6187  swoer  6200  swoord1  6201  swoord2  6202  erth  6216  eroprf  6265  ecopovtrn  6269  ecopovtrng  6272  th3qlem1  6274  ecovicom  6280  ecoviass  6282  ecovidi  6284  f1oen2g  6302  cnvct  6356  fndmeng  6357  xpsnen2g  6373  xpdom1g  6377  xpdom3m  6378  fopwdom  6380  xpf1o  6385  xpen  6386  phplem4dom  6397  phpm  6400  phplem4on  6402  fict  6403  fidceq  6404  fidifsnen  6405  dif1en  6414  fisbth  6417  diffisn  6427  diffifi  6428  infnfi  6429  ac6sfi  6431  en2eqpr  6434  fientri3  6435  nnwetri  6436  unsnfi  6439  unsnfidcex  6440  unsnfidcel  6441  unfidisj  6442  undiffi  6443  fnfi  6446  relcnvfi  6449  funrnfi  6450  f1dmvrnfibi  6452  eqsupti  6468  supsnti  6477  supisolem  6480  supisoex  6481  infglbti  6497  ordiso2  6505  cardval3ex  6513  dfplpq2  6606  addcmpblnq  6619  addpipqqslem  6621  mulpipq2  6623  addcomnqg  6633  addassnqg  6634  distrnqg  6639  nqtri3or  6648  ltsonq  6650  ltanqg  6652  ltexnqq  6660  halfnqq  6662  subhalfnqq  6666  archnqq  6669  prarloclemarch  6670  prarloclemarch2  6671  ltrnqg  6672  enq0tr  6686  nqnq0pi  6690  addcmpblnq0  6695  nnnq0lem1  6698  nqpnq0nq  6705  nqnq0a  6706  nqnq0m  6707  distrnq0  6711  mulcomnq0  6712  addassnq0lemcl  6713  addassnq0  6714  preqlu  6724  prltlu  6739  prarloclemlt  6745  prarloclemlo  6746  prarloclem5  6752  prarloclemcalc  6754  prarloc  6755  genplt2i  6762  genpassg  6778  addnqprllem  6779  addnqprulem  6780  addnqprl  6781  addnqpru  6782  addlocprlemeqgt  6784  addlocprlemgt  6786  addlocprlem  6787  nqprl  6803  nqpru  6804  addnqprlemrl  6809  addnqprlemru  6810  addnqpr  6813  appdivnq  6815  prmuloclemcalc  6817  prmuloc  6818  prmuloc2  6819  mulnqprl  6820  mulnqpru  6821  mullocprlem  6822  mullocpr  6823  mulnqprlemrl  6825  mulnqprlemru  6826  mulnqpr  6829  distrlem4prl  6836  distrlem4pru  6837  distrlem5prl  6838  distrlem5pru  6839  distrprg  6840  ltprordil  6841  1idprl  6842  1idpru  6843  ltnqpri  6846  ltexprlemm  6852  ltexprlemopl  6853  ltexprlemlol  6854  ltexprlemopu  6855  ltexprlemupu  6856  ltexprlemloc  6859  ltexprlemfl  6861  ltexprlemrl  6862  ltexprlemfu  6863  ltexprlemru  6864  ltexpri  6865  addcanprleml  6866  addcanprlemu  6867  ltaprlem  6870  ltaprg  6871  prplnqu  6872  addextpr  6873  recexprlemm  6876  recexprlemdisj  6882  recexprlemloc  6883  recexprlem1ssl  6885  recexprlem1ssu  6886  recexpr  6890  aptiprleml  6891  aptiprlemu  6892  ltmprr  6894  archpr  6895  caucvgprlemcanl  6896  cauappcvgprlemm  6897  cauappcvgprlemopl  6898  cauappcvgprlemopu  6900  cauappcvgprlemdisj  6903  cauappcvgprlemloc  6904  cauappcvgprlemladdfu  6906  cauappcvgprlemladdfl  6907  cauappcvgprlemladdru  6908  cauappcvgprlemladdrl  6909  cauappcvgprlemladd  6910  cauappcvgprlem1  6911  cauappcvgprlem2  6912  cauappcvgpr  6914  archrecpr  6916  caucvgprlemk  6917  caucvgprlemnkj  6918  caucvgprlemnbj  6919  caucvgprlemm  6920  caucvgprlemopl  6921  caucvgprlemopu  6923  caucvgprlemloc  6927  caucvgprlemladdfu  6929  caucvgprlemladdrl  6930  caucvgprlem1  6931  caucvgprlem2  6932  caucvgpr  6934  caucvgprprlemk  6935  caucvgprprlemloccalc  6936  caucvgprprlemnkltj  6941  caucvgprprlemnkeqj  6942  caucvgprprlemnjltk  6943  caucvgprprlemnkj  6944  caucvgprprlemnbj  6945  caucvgprprlemml  6946  caucvgprprlemmu  6947  caucvgprprlemopl  6949  caucvgprprlemopu  6951  caucvgprprlemloc  6955  caucvgprprlemexbt  6958  caucvgprprlemexb  6959  caucvgprprlemaddq  6960  caucvgprprlem1  6961  caucvgprprlem2  6962  caucvgprpr  6964  addcmpblnr  6978  mulcmpblnrlemg  6979  mulcmpblnr  6980  prsrlem1  6981  ltsrprg  6986  mulcomsrg  6996  mulasssrg  6997  distrsrg  6998  lttrsr  7001  ltsosr  7003  ltasrg  7009  pn0sr  7010  negexsr  7011  recexgt0sr  7012  mulgt0sr  7016  aptisr  7017  mulextsr1lem  7018  mulextsr1  7019  archsr  7020  srpospr  7021  prsradd  7024  prsrlt  7025  prsrriota  7026  caucvgsrlemcl  7027  caucvgsrlemfv  7029  caucvgsrlemcau  7031  caucvgsrlemgt1  7033  caucvgsrlemoffval  7034  caucvgsrlemofff  7035  caucvgsrlemoffcau  7036  caucvgsrlemoffgt1  7037  caucvgsrlemoffres  7038  addcnsr  7064  mulcnsr  7065  addcnsrec  7072  mulcnsrec  7073  ltrennb  7084  recidpipr  7086  recidpirqlemcalc  7087  recidpirq  7088  axaddcl  7094  axmulcl  7096  axmulcom  7099  axmulass  7101  axdistr  7102  axrnegex  7107  axcnre  7109  rereceu  7117  recriota  7118  nntopi  7122  axcaucvglemval  7125  axcaucvglemcau  7126  axcaucvglemres  7127  addcld  7200  mulcld  7201  mulcomd  7202  readdcld  7210  remulcld  7211  lelttr  7266  ltletr  7267  gtned  7290  lttri3d  7292  letri3d  7293  lenltd  7294  ltled  7295  readdcan  7315  addcomd  7326  cnegex  7353  negeu  7366  addsubass  7385  subsub2  7403  subsub4  7408  negcon1d  7480  neg11ad  7482  subcld  7486  pncand  7487  pncan2d  7488  pncan3d  7489  npcand  7490  nncand  7491  negsubd  7492  subnegd  7493  subeq0d  7494  subne0d  7495  subeq0ad  7496  negdid  7499  negdi2d  7500  negsubdid  7501  negsubdi2d  7502  neg2subd  7503  resubcld  7552  negf1o  7553  mulneg1d  7582  mulneg2d  7583  mul2negd  7584  ltadd2  7590  posdif  7626  add20  7645  ltnegd  7690  lenegd  7691  ltnegcon1d  7692  ltnegcon2d  7693  lenegcon1d  7694  lenegcon2d  7695  ltaddposd  7696  ltaddpos2d  7697  ltsubposd  7698  posdifd  7699  addge01d  7700  addge02d  7701  subge0d  7702  suble0d  7703  subge02d  7704  rimul  7752  rereim  7753  apreap  7754  reapmul1lem  7761  reapmul1  7762  reapadd1  7763  reapneg  7764  remulext1  7766  cru  7769  apreim  7770  apsym  7773  addext  7777  apneg  7778  mulext1  7779  mulext  7781  apti  7789  leltap  7791  gt0ap0d  7795  ltap  7798  ltapd  7803  ap0gt0d  7806  recexaplem2  7809  recexap  7810  mulap0bd  7814  mulcanapd  7818  muleqadd  7825  receuap  7826  divmulap  7830  divdivdivap  7868  divcanap6  7874  recclapd  7936  recap0d  7937  recidapd  7938  recidap2d  7939  recrecapd  7940  dividapd  7941  div0apd  7942  rerecclapd  7986  recgt0  7995  prodgt0  7997  lt2msq  8031  lediv12a  8039  lediv2a  8040  recreclt  8045  recgt0d  8079  negiso  8100  creui  8104  nnge1  8129  nnaddcld  8153  nnmulcld  8154  nndivred  8155  halfaddsub  8332  lt2halves  8333  addltmul  8334  nn0addcld  8412  nn0mulcld  8413  gtndiv  8523  suprzclex  8526  zaddcld  8554  zsubcld  8555  zmulcld  8556  uzneg  8718  uzm1  8730  uzin  8732  uzind4  8757  supinfneg  8764  infsupneg  8765  supminfex  8766  qmulcl  8803  qapne  8805  rpaddcld  8870  rpmulcld  8871  rpdivcld  8872  ltrecd  8873  lerecd  8874  ltrec1d  8875  lerec2d  8876  ge0p1rpd  8885  rerpdivcld  8886  ltsubrpd  8887  ltaddrpd  8888  xrlelttr  8952  xrltletr  8953  ixxdisj  9002  ixxss1  9003  ixxss2  9004  iccsupr  9065  icoshft  9088  icoshftf1o  9089  icodisj  9090  zltaddlt1le  9104  elfz1eq  9130  fzen  9138  fzsplit  9146  elfz1end  9150  fznatpl1  9169  fzdifsuc  9174  uzdisj  9186  fseq1p1m1  9187  fzm1  9193  fzneuz  9194  fznuz  9195  uznfz  9196  fznn0sub2  9216  nn0disj  9225  elfzoelz  9234  elfzouz2  9247  fzonnsub  9255  fzospliti  9262  fzosplit  9263  fzodisj  9264  elfzo1  9276  eluzgtdifelfzo  9283  fzocatel  9285  zpnn0elfzo  9293  fzostep1  9323  exfzdc  9326  fvinim0ffz  9327  subfzo0  9328  qtri3or  9329  exbtwnz  9337  qbtwnre  9343  qavgle  9345  ico0  9348  apbtwnz  9356  flqlelt  9358  flqge  9364  flqlt  9365  flqwordi  9370  flqbi2  9373  fldivnn0  9377  flqaddz  9379  flqmulnn0  9381  flltdivnn0lt  9386  ceilqval  9388  intfracq  9402  flqdiv  9403  modqcl  9408  mulqmod0  9412  modqmulnn  9424  zmodcld  9427  modqcyc  9441  modqcyc2  9442  modqadd1  9443  mulqaddmodid  9446  mulp1mod1  9447  m1modnnsub1  9452  modqm1p1mod0  9457  modqltm1p1mod  9458  modqmul1  9459  q2submod  9467  modifeq2int  9468  modaddmodlo  9470  modqaddmulmod  9473  modqdi  9474  modqsubdir  9475  modsumfzodifsn  9478  addmodlteq  9480  frec2uzzd  9482  frec2uzltd  9485  frec2uzlt2d  9486  frecuzrdgrrn  9490  frec2uzrdg  9491  frecuzrdgrcl  9492  frecuzrdglem  9493  frecuzrdg0  9495  frecuzrdgsuc  9496  frecuzrdgrclt  9497  frecuzrdgg  9498  frecuzrdgdomlem  9499  frecuzrdg0t  9504  frecuzrdgsuctlem  9505  frecfzen2  9509  frec2uzled  9511  fzfig  9512  fzfigd  9513  uzsinds  9518  iseqeq3  9526  iseqvalt  9532  iseqm1  9543  iseqfveq2  9544  iseqfeq2  9545  iseqshft2  9548  monoord  9551  monoord2  9552  iseqsplit  9554  iseqcaopr3  9556  iseqid  9563  iseqid2  9564  iseqhomo  9565  iseqz  9566  iseqdistr  9567  expivallem  9574  expival  9575  expcl2lemap  9585  expap0  9603  expgt1  9611  mulexp  9612  mulexpzap  9613  expadd  9615  expaddzaplem  9616  expaddzap  9617  expmulzap  9619  ltexp2a  9625  leexp2a  9626  leexp2r  9627  mulbinom2  9686  bernneq  9690  expnbnd  9693  expnlbnd  9694  expnlbnd2  9695  expeq0d  9698  expcld  9702  expp1d  9703  sqrecapd  9706  sqmuld  9714  reexpcld  9719  nnexpcld  9724  nn0expcld  9725  rpexpcld  9726  sqgt0apd  9730  nn0opthlem1d  9744  nn0opthlem2d  9745  nn0opthd  9746  facwordi  9764  faclbnd  9765  faclbnd2  9766  faclbnd3  9767  faclbnd6  9768  facavg  9770  bcval  9773  bcval2  9774  bcrpcl  9777  bccmpl  9778  bcnp1n  9783  bcp1nk  9786  ibcval5  9787  bcp1m1  9789  bcpasc  9790  bccl2  9792  sizeinfuni  9801  sizeinf  9802  sizeennnuni  9803  sizeennn  9804  sizecl  9805  sizefz1  9807  sizeen  9808  sizeeqf1od  9814  sizeneq0  9819  fseq1size  9825  sizedom  9827  sizeunlem  9828  sizeun  9829  shftfvalg  9844  shftfval  9847  shftval2  9852  shftval5  9855  crre  9882  remim  9885  mulreap  9889  recj  9892  reneg  9893  readd  9894  remullem  9896  imcj  9900  imneg  9901  imadd  9902  cjexp  9918  cjap  9931  cjdivap  9934  cnrecnv  9935  cjexpd  9983  readdd  9984  imaddd  9985  resubd  9986  imsubd  9987  remuld  9988  immuld  9989  cjaddd  9990  cjmuld  9991  ipcnd  9992  remul2d  9997  immul2d  9998  crred  10001  crimd  10002  caucvgrelemcau  10004  caucvgre  10005  cvg1nlemcau  10008  cvg1nlemres  10009  recvguniq  10019  resqrexlemover  10034  resqrexlemdecn  10036  resqrexlemcalc1  10038  resqrexlemcalc2  10039  resqrexlemnmsq  10041  resqrexlemnm  10042  resqrexlemcvg  10043  resqrexlemoverl  10045  resqrexlemglsq  10046  resqrexlemga  10047  resqrtcl  10053  rersqrtthlem  10054  sqrtmul  10059  rpsqrtcl  10065  sqrtdiv  10066  abscl  10075  absvalsq  10077  absge0  10084  abs00ap  10086  absreim  10092  absdivap  10094  leabs  10098  absexp  10103  absexpzap  10104  sqabs  10106  ltabs  10111  abslt  10112  absle  10113  abssubap0  10114  abssubne0  10115  absidm  10122  abssubge0  10126  abstri  10128  abs3dif  10129  abs2difabs  10132  fzomaxdiflem  10136  caubnd2  10141  amgm2  10142  absnidd  10184  resqrtcld  10187  sqrtmsqd  10188  sqrtsqd  10189  sqrtge0d  10190  absidd  10191  absltd  10198  absled  10199  absrpclapd  10212  absexpd  10216  abssubd  10217  absmuld  10218  abstrid  10220  abs2difd  10221  abs2dif2d  10222  abs2difabsd  10223  maxabslemlub  10231  maxleastb  10238  maxltsup  10242  fimaxre2  10247  negfi  10248  minmax  10250  lemininf  10253  ltmininf  10254  climconst  10267  climuni  10270  climmpt  10277  climshft  10281  climshft2  10283  climcn2  10286  mulcn2  10289  cn1lem  10290  cjcn2  10292  climrecl  10300  climle  10310  iserile  10318  climcau  10322  climcvg1nlem  10324  serif0  10327  sumdc  10333  sumeq2d  10334  sumeq2  10335  isumrblem  10337  fisumcvg  10338  isumrb  10339  dvdsval2  10343  moddvds  10349  dvds2lem  10352  zdvdsdc  10361  iddvdsexp  10364  summodnegmod  10371  dvds2ln  10373  dvdsadd2b  10387  dvdslelemd  10388  dvdsle  10389  divconjdvds  10394  fzm1ndvds  10401  fzo0dvdseq  10402  fzocongeq  10403  dvdsfac  10405  dvdsexp  10406  dvdsmod  10407  mulmoddvds  10408  odd2np1lem  10416  odd2np1  10417  opeo  10441  omeo  10442  nn0o1gt2  10449  divalglemeunn  10465  divalglemex  10466  divalglemeuneg  10467  divalg  10468  divalgmod  10471  modremain  10473  fldivndvdslt  10479  zsupcl  10487  zssinfcl  10488  infssuzex  10489  dvdsbnd  10492  nndvdslegcd  10501  gcdcld  10504  zeqzmulgcd  10506  divgcdnn  10510  gcdn0gt0  10513  gcdaddm  10519  modgcd  10526  bezoutlemnewy  10529  bezoutlemmain  10531  bezoutlemzz  10535  bezoutlemaz  10536  bezoutlembz  10537  bezoutlemeu  10540  bezoutlemle  10541  dfgcd3  10543  bezout  10544  dvdsgcd  10545  dfgcd2  10547  gcdass  10548  mulgcd  10549  gcddiv  10552  gcdmultiple  10553  gcdmultiplez  10554  gcdzeq  10555  dvdsmulgcd  10558  rplpwr  10560  rppwr  10561  sqgcd  10562  bezoutr1  10566  nn0seqcvgd  10567  ialgr0  10570  ialgrp1  10572  ialgcvg  10574  algcvgb  10576  eucalgval2  10579  eucalgval  10580  eucalgf  10581  eucalginv  10582  eucalglt  10583  lcmval  10589  lcmcllem  10593  lcmledvds  10596  lcmneg  10600  lcmgcdlem  10603  lcmass  10611  ncoprmgcdne1b  10615  coprmdvds2  10619  mulgcddvds  10620  rpmulgcd2  10621  qredeu  10623  rpdvds  10625  congr  10626  divgcdcoprmex  10628  cncongr1  10629  cncongr2  10630  1idssfct  10641  isprm4  10645  prmind2  10646  dvdsnprmd  10651  oddprmge3  10660  sqnprm  10661  exprmfct  10663  coprm  10667  euclemma  10669  isprm6  10670  prmexpb  10674  prmfac1  10675  rpexp  10676  rpexp12i  10678  pw2dvdslemn  10687  pw2dvds  10688  pw2dvdseulemle  10689  oddpwdclemxy  10691  oddpwdc  10696  sqpweven  10697  2sqpwodd  10698  znege1  10700  sqrt2irraplemnn  10701  sqrt2irrap  10702  qnumdenbi  10714  divnumden  10718  numdensq  10724  nn0sqrtelqelz  10728  nonsq  10729  oddennn  10730  xpct  10734  znnen  10736  spimd  10754  bdssexd  10881  qdencn  10970
  Copyright terms: Public domain W3C validator