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

Theorem syl2anc 391
Description: Syllogism inference combined with contraction. (Contributed by NM, 16-Mar-2012.)
Hypotheses
Ref Expression
syl2anc.1  |-  ( ph  ->  ps )
syl2anc.2  |-  ( ph  ->  ch )
syl2anc.3  |-  ( ( ps  /\  ch )  ->  th )
Assertion
Ref Expression
syl2anc  |-  ( ph  ->  th )

Proof of Theorem syl2anc
StepHypRef Expression
1 syl2anc.1 . 2  |-  ( ph  ->  ps )
2 syl2anc.2 . 2  |-  ( ph  ->  ch )
3 syl2anc.3 . . 3  |-  ( ( ps  /\  ch )  ->  th )
43ex 108 . 2  |-  ( ps 
->  ( ch  ->  th )
)
51, 2, 4sylc 56 1  |-  ( ph  ->  th )
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  2372  r19.29d2r  2455  elrab3t  2697  eueq2dc  2714  csbiedf  2887  sstrd  2955  psstrd  3052  sspsstrd  3053  psssstrd  3054  uneq12d  3098  unssd  3119  ineq12d  3139  ssind  3161  preq12d  3455  opeq12d  3557  nfopd  3566  breq12d  3777  mpteq12dva  3838  ssexd  3897  exss  3963  opexg  3964  opth  3974  op1stbg  4210  onintexmid  4297  wetriext  4301  tfisi  4310  xpeq12d  4370  poinxp  4409  eqbrrdv  4437  nfimad  4677  cnvexg  4855  funprg  4949  funtpg  4950  funimaexglem  4982  funfni  4999  fnunsn  5006  fnresdm  5008  fn0  5018  fssd  5055  fssxp  5058  fconstg  5083  fconst6g  5085  resdif  5148  nffvd  5187  sefvex  5196  feqresmpt  5227  fvelimab  5229  fvmptd  5253  fvmpt2d  5257  fvmptdf  5258  fvmptt  5262  eqfnfvd  5268  fnreseql  5277  fimacnv  5296  dff3im  5312  foco2  5318  ffvresb  5328  f1oresrab  5329  fmptco  5330  fmptapd  5354  fsnunf  5362  fconst3m  5380  fnex  5383  fcof1  5423  fcofo  5424  cocan1  5427  cocan2  5428  foeqcnvco  5430  f1eqcocnv  5431  fliftrel  5432  fliftel  5433  fliftel1  5434  fliftval  5440  isocnv2  5452  isores2  5453  isotr  5456  f1oiso2  5466  riotass2  5494  riotass  5495  oveq12d  5530  ovexg  5539  ovprc  5540  ovresd  5641  suppssov1  5709  offval  5719  ofrfval  5720  fnofval  5721  ofrval  5722  ofmresval  5723  offval2  5726  ofrfval2  5727  ofco  5729  caofinvl  5733  cofunexg  5738  fnexALT  5740  opabex3d  5748  oprabexd  5754  ofmresex  5764  xpopth  5802  eqop  5803  2nd1st  5806  2ndrn  5809  elopabi  5821  mpt2fvex  5829  oprab2co  5839  1stconst  5842  2ndconst  5843  cnvf1olem  5845  tposexg  5873  tposf2  5883  tposf12  5884  smoiso  5917  tfrlem1  5923  tfrlem5  5930  tfr0  5937  tfrlemisucaccv  5939  tfrlemibacc  5940  tfrlemibxssdm  5941  tfrlemibfn  5942  tfrlemi14d  5947  tfrexlem  5948  rdgivallem  5968  frecsuclem3  5990  frecrdg  5992  freccl  5993  sucinc2  6026  oav2  6043  omv2  6045  omsuc  6051  nnsucsssuc  6071  nndifsnid  6080  nnaordi  6081  nnaword  6084  nnmord  6090  nnmword  6091  nnaordex  6100  ercl  6117  ersym  6118  ertr  6121  swoer  6134  swoord1  6135  swoord2  6136  erth  6150  eroprf  6199  ecopovtrn  6203  ecopovtrng  6206  th3qlem1  6208  ecovicom  6214  ecoviass  6216  ecovidi  6218  f1oen2g  6235  fndmeng  6289  xpsnen2g  6303  xpdom1g  6307  xpdom3m  6308  fopwdom  6310  phplem4dom  6324  phpm  6327  phplem4on  6329  fidceq  6330  fidifsnen  6331  dif1en  6337  fisbth  6340  diffisn  6350  diffifi  6351  ac6sfi  6352  fientri3  6353  nnwetri  6354  ordiso2  6357  cardval3ex  6365  dfplpq2  6452  addcmpblnq  6465  addpipqqslem  6467  mulpipq2  6469  addcomnqg  6479  addassnqg  6480  distrnqg  6485  nqtri3or  6494  ltsonq  6496  ltanqg  6498  ltexnqq  6506  halfnqq  6508  subhalfnqq  6512  archnqq  6515  prarloclemarch  6516  prarloclemarch2  6517  ltrnqg  6518  enq0tr  6532  nqnq0pi  6536  addcmpblnq0  6541  nnnq0lem1  6544  nqpnq0nq  6551  nqnq0a  6552  nqnq0m  6553  distrnq0  6557  mulcomnq0  6558  addassnq0lemcl  6559  addassnq0  6560  preqlu  6570  prltlu  6585  prarloclemlt  6591  prarloclemlo  6592  prarloclem5  6598  prarloclemcalc  6600  prarloc  6601  genplt2i  6608  genpassg  6624  addnqprllem  6625  addnqprulem  6626  addnqprl  6627  addnqpru  6628  addlocprlemeqgt  6630  addlocprlemgt  6632  addlocprlem  6633  nqprl  6649  nqpru  6650  addnqprlemrl  6655  addnqprlemru  6656  addnqpr  6659  appdivnq  6661  prmuloclemcalc  6663  prmuloc  6664  prmuloc2  6665  mulnqprl  6666  mulnqpru  6667  mullocprlem  6668  mullocpr  6669  mulnqprlemrl  6671  mulnqprlemru  6672  mulnqpr  6675  distrlem4prl  6682  distrlem4pru  6683  distrlem5prl  6684  distrlem5pru  6685  distrprg  6686  ltprordil  6687  1idprl  6688  1idpru  6689  ltnqpri  6692  ltexprlemm  6698  ltexprlemopl  6699  ltexprlemlol  6700  ltexprlemopu  6701  ltexprlemupu  6702  ltexprlemloc  6705  ltexprlemfl  6707  ltexprlemrl  6708  ltexprlemfu  6709  ltexprlemru  6710  ltexpri  6711  addcanprleml  6712  addcanprlemu  6713  ltaprlem  6716  ltaprg  6717  prplnqu  6718  addextpr  6719  recexprlemm  6722  recexprlemdisj  6728  recexprlemloc  6729  recexprlem1ssl  6731  recexprlem1ssu  6732  recexpr  6736  aptiprleml  6737  aptiprlemu  6738  ltmprr  6740  archpr  6741  caucvgprlemcanl  6742  cauappcvgprlemm  6743  cauappcvgprlemopl  6744  cauappcvgprlemopu  6746  cauappcvgprlemdisj  6749  cauappcvgprlemloc  6750  cauappcvgprlemladdfu  6752  cauappcvgprlemladdfl  6753  cauappcvgprlemladdru  6754  cauappcvgprlemladdrl  6755  cauappcvgprlemladd  6756  cauappcvgprlem1  6757  cauappcvgprlem2  6758  cauappcvgpr  6760  archrecpr  6762  caucvgprlemk  6763  caucvgprlemnkj  6764  caucvgprlemnbj  6765  caucvgprlemm  6766  caucvgprlemopl  6767  caucvgprlemopu  6769  caucvgprlemloc  6773  caucvgprlemladdfu  6775  caucvgprlemladdrl  6776  caucvgprlem1  6777  caucvgprlem2  6778  caucvgpr  6780  caucvgprprlemk  6781  caucvgprprlemloccalc  6782  caucvgprprlemnkltj  6787  caucvgprprlemnkeqj  6788  caucvgprprlemnjltk  6789  caucvgprprlemnkj  6790  caucvgprprlemnbj  6791  caucvgprprlemml  6792  caucvgprprlemmu  6793  caucvgprprlemopl  6795  caucvgprprlemopu  6797  caucvgprprlemloc  6801  caucvgprprlemexbt  6804  caucvgprprlemexb  6805  caucvgprprlemaddq  6806  caucvgprprlem1  6807  caucvgprprlem2  6808  caucvgprpr  6810  addcmpblnr  6824  mulcmpblnrlemg  6825  mulcmpblnr  6826  prsrlem1  6827  ltsrprg  6832  mulcomsrg  6842  mulasssrg  6843  distrsrg  6844  lttrsr  6847  ltsosr  6849  ltasrg  6855  pn0sr  6856  negexsr  6857  recexgt0sr  6858  mulgt0sr  6862  aptisr  6863  mulextsr1lem  6864  mulextsr1  6865  archsr  6866  srpospr  6867  prsradd  6870  prsrlt  6871  prsrriota  6872  caucvgsrlemcl  6873  caucvgsrlemfv  6875  caucvgsrlemcau  6877  caucvgsrlemgt1  6879  caucvgsrlemoffval  6880  caucvgsrlemofff  6881  caucvgsrlemoffcau  6882  caucvgsrlemoffgt1  6883  caucvgsrlemoffres  6884  addcnsr  6910  mulcnsr  6911  addcnsrec  6918  mulcnsrec  6919  ltrennb  6930  recidpipr  6932  recidpirqlemcalc  6933  recidpirq  6934  axaddcl  6940  axmulcl  6942  axmulcom  6945  axmulass  6947  axdistr  6948  axrnegex  6953  axcnre  6955  rereceu  6963  recriota  6964  nntopi  6968  axcaucvglemval  6971  axcaucvglemcau  6972  axcaucvglemres  6973  addcld  7046  mulcld  7047  mulcomd  7048  readdcld  7055  remulcld  7056  lelttr  7106  ltletr  7107  gtned  7130  lttri3d  7132  letri3d  7133  lenltd  7134  ltled  7135  readdcan  7153  addcomd  7164  cnegex  7189  negeu  7202  addsubass  7221  subsub2  7239  subsub4  7244  negcon1d  7316  neg11ad  7318  subcld  7322  pncand  7323  pncan2d  7324  pncan3d  7325  npcand  7326  nncand  7327  negsubd  7328  subnegd  7329  subeq0d  7330  subne0d  7331  subeq0ad  7332  negdid  7335  negdi2d  7336  negsubdid  7337  negsubdi2d  7338  neg2subd  7339  resubcld  7379  mulneg1d  7408  mulneg2d  7409  mul2negd  7410  ltadd2  7416  posdif  7450  add20  7469  ltnegd  7514  lenegd  7515  ltnegcon1d  7516  ltnegcon2d  7517  lenegcon1d  7518  lenegcon2d  7519  ltaddposd  7520  ltaddpos2d  7521  ltsubposd  7522  posdifd  7523  addge01d  7524  addge02d  7525  subge0d  7526  suble0d  7527  subge02d  7528  rimul  7576  rereim  7577  apreap  7578  reapmul1lem  7585  reapmul1  7586  reapadd1  7587  reapneg  7588  remulext1  7590  cru  7593  apreim  7594  apsym  7597  addext  7601  apneg  7602  mulext1  7603  mulext  7605  apti  7613  leltap  7615  gt0ap0d  7619  ltap  7622  ltapd  7627  ap0gt0d  7630  recexaplem2  7633  recexap  7634  mulap0bd  7638  mulcanapd  7642  muleqadd  7649  receuap  7650  divmulap  7654  divdivdivap  7689  divcanap6  7695  recclapd  7757  recap0d  7758  recidapd  7759  recidap2d  7760  recrecapd  7761  dividapd  7762  div0apd  7763  rerecclapd  7807  recgt0  7816  prodgt0  7818  lt2msq  7852  lediv12a  7860  lediv2a  7861  recreclt  7866  recgt0d  7900  creui  7912  nnge1  7937  nnaddcld  7961  nnmulcld  7962  nndivred  7963  halfaddsub  8159  lt2halves  8160  addltmul  8161  nn0addcld  8239  nn0mulcld  8240  gtndiv  8335  zaddcld  8364  zsubcld  8365  zmulcld  8366  uzneg  8491  uzm1  8503  uzin  8505  uzind4  8531  qmulcl  8572  qapne  8574  rpaddcld  8638  rpmulcld  8639  rpdivcld  8640  ltrecd  8641  lerecd  8642  ltrec1d  8643  lerec2d  8644  ge0p1rpd  8653  rerpdivcld  8654  ltsubrpd  8655  ltaddrpd  8656  xrlelttr  8722  xrltletr  8723  ixxdisj  8772  ixxss1  8773  ixxss2  8774  iccsupr  8835  icoshft  8858  icoshftf1o  8859  icodisj  8860  elfz1eq  8899  fzen  8907  fzsplit  8915  elfz1end  8919  fznatpl1  8938  fzdifsuc  8943  uzdisj  8955  fseq1p1m1  8956  fzm1  8962  fzneuz  8963  fznuz  8964  uznfz  8965  fznn0sub2  8985  nn0disj  8995  elfzoelz  9004  elfzouz2  9017  fzonnsub  9025  fzospliti  9032  fzosplit  9033  fzodisj  9034  elfzo1  9046  eluzgtdifelfzo  9053  fzocatel  9055  zpnn0elfzo  9063  fzostep1  9093  fvinim0ffz  9096  subfzo0  9097  qtri3or  9098  qbtwnzlemstep  9103  qbtwnz  9106  qbtwnre  9111  flqlelt  9118  flqge  9124  flqlt  9125  flqwordi  9130  flqbi2  9133  fldivnn0  9137  flqaddz  9139  flqmulnn0  9141  flltdivnn0lt  9146  ceilqval  9148  intfracq  9162  flqdiv  9163  modqcl  9168  mulqmod0  9172  modqmulnn  9184  frec2uzsucd  9187  frec2uzltd  9189  frec2uzlt2d  9190  frecuzrdgrrn  9194  frec2uzrdg  9195  frecuzrdgrom  9196  frecuzrdglem  9197  frecuzrdg0  9200  frecuzrdgsuc  9201  frecfzen2  9204  fzfig  9206  fzfigd  9207  iseqeq3  9216  iseqm1  9227  iseqfveq2  9228  iseqfeq2  9229  iseqshft2  9232  monoord  9235  monoord2  9236  iseqsplit  9238  iseqcaopr3  9240  iseqid  9247  iseqhomo  9248  iseqdistr  9249  expivallem  9256  expival  9257  expcl2lemap  9267  expap0  9285  expgt1  9293  mulexp  9294  mulexpzap  9295  expadd  9297  expaddzaplem  9298  expaddzap  9299  expmulzap  9301  ltexp2a  9306  leexp2a  9307  leexp2r  9308  bernneq  9369  expnbnd  9372  expnlbnd  9373  expnlbnd2  9374  expeq0d  9377  expcld  9381  expp1d  9382  sqrecapd  9385  sqmuld  9393  reexpcld  9398  nnexpcld  9402  nn0expcld  9403  rpexpcld  9404  sqgt0apd  9408  shftfvalg  9419  shftfval  9422  shftval2  9427  shftval5  9430  crre  9457  remim  9460  mulreap  9464  recj  9467  reneg  9468  readd  9469  remullem  9471  imcj  9475  imneg  9476  imadd  9477  cjexp  9493  cjap  9506  cjdivap  9509  cnrecnv  9510  cjexpd  9558  readdd  9559  imaddd  9560  resubd  9561  imsubd  9562  remuld  9563  immuld  9564  cjaddd  9565  cjmuld  9566  ipcnd  9567  remul2d  9572  immul2d  9573  crred  9576  crimd  9577  caucvgrelemcau  9579  caucvgre  9580  cvg1nlemcau  9583  cvg1nlemres  9584  recvguniq  9593  resqrexlemover  9608  resqrexlemdecn  9610  resqrexlemcalc1  9612  resqrexlemcalc2  9613  resqrexlemnmsq  9615  resqrexlemnm  9616  resqrexlemcvg  9617  resqrexlemoverl  9619  resqrexlemglsq  9620  resqrexlemga  9621  resqrtcl  9627  rersqrtthlem  9628  sqrtmul  9633  rpsqrtcl  9639  sqrtdiv  9640  abscl  9649  absvalsq  9651  absge0  9658  abs00ap  9660  absreim  9666  absdivap  9668  leabs  9672  absexp  9675  absexpzap  9676  sqabs  9678  ltabs  9683  abslt  9684  absle  9685  abssubap0  9686  abssubne0  9687  absidm  9694  abssubge0  9698  abstri  9700  abs3dif  9701  abs2difabs  9704  fzomaxdiflem  9708  caubnd2  9713  amgm2  9714  absnidd  9756  resqrtcld  9759  sqrtmsqd  9760  sqrtsqd  9761  sqrtge0d  9762  absidd  9763  absltd  9770  absled  9771  absrpclapd  9784  absexpd  9788  abssubd  9789  absmuld  9790  abstrid  9792  abs2difd  9793  abs2dif2d  9794  abs2difabsd  9795  climconst  9811  climuni  9814  climmpt  9821  climshft  9825  climshft2  9827  climcn2  9830  mulcn2  9833  cn1lem  9834  cjcn2  9836  climrecl  9844  climle  9854  iserile  9862  climcau  9866  climcvg1nlem  9868  serif0  9871  nn0seqcvgd  9880  ialgr0  9883  ialgrp1  9885  ialgcvg  9887  algcvgb  9889  spimd  9905  bdssexd  10025  qdencn  10124
  Copyright terms: Public domain W3C validator