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  6355  cardval3ex  6363  dfplpq2  6450  addcmpblnq  6463  addpipqqslem  6465  mulpipq2  6467  addcomnqg  6477  addassnqg  6478  distrnqg  6483  nqtri3or  6492  ltsonq  6494  ltanqg  6496  ltexnqq  6504  halfnqq  6506  subhalfnqq  6510  archnqq  6513  prarloclemarch  6514  prarloclemarch2  6515  ltrnqg  6516  enq0tr  6530  nqnq0pi  6534  addcmpblnq0  6539  nnnq0lem1  6542  nqpnq0nq  6549  nqnq0a  6550  nqnq0m  6551  distrnq0  6555  mulcomnq0  6556  addassnq0lemcl  6557  addassnq0  6558  preqlu  6568  prltlu  6583  prarloclemlt  6589  prarloclemlo  6590  prarloclem5  6596  prarloclemcalc  6598  prarloc  6599  genplt2i  6606  genpassg  6622  addnqprllem  6623  addnqprulem  6624  addnqprl  6625  addnqpru  6626  addlocprlemeqgt  6628  addlocprlemgt  6630  addlocprlem  6631  nqprl  6647  nqpru  6648  addnqprlemrl  6653  addnqprlemru  6654  addnqpr  6657  appdivnq  6659  prmuloclemcalc  6661  prmuloc  6662  prmuloc2  6663  mulnqprl  6664  mulnqpru  6665  mullocprlem  6666  mullocpr  6667  mulnqprlemrl  6669  mulnqprlemru  6670  mulnqpr  6673  distrlem4prl  6680  distrlem4pru  6681  distrlem5prl  6682  distrlem5pru  6683  distrprg  6684  ltprordil  6685  1idprl  6686  1idpru  6687  ltnqpri  6690  ltexprlemm  6696  ltexprlemopl  6697  ltexprlemlol  6698  ltexprlemopu  6699  ltexprlemupu  6700  ltexprlemloc  6703  ltexprlemfl  6705  ltexprlemrl  6706  ltexprlemfu  6707  ltexprlemru  6708  ltexpri  6709  addcanprleml  6710  addcanprlemu  6711  ltaprlem  6714  ltaprg  6715  prplnqu  6716  addextpr  6717  recexprlemm  6720  recexprlemdisj  6726  recexprlemloc  6727  recexprlem1ssl  6729  recexprlem1ssu  6730  recexpr  6734  aptiprleml  6735  aptiprlemu  6736  ltmprr  6738  archpr  6739  caucvgprlemcanl  6740  cauappcvgprlemm  6741  cauappcvgprlemopl  6742  cauappcvgprlemopu  6744  cauappcvgprlemdisj  6747  cauappcvgprlemloc  6748  cauappcvgprlemladdfu  6750  cauappcvgprlemladdfl  6751  cauappcvgprlemladdru  6752  cauappcvgprlemladdrl  6753  cauappcvgprlemladd  6754  cauappcvgprlem1  6755  cauappcvgprlem2  6756  cauappcvgpr  6758  archrecpr  6760  caucvgprlemk  6761  caucvgprlemnkj  6762  caucvgprlemnbj  6763  caucvgprlemm  6764  caucvgprlemopl  6765  caucvgprlemopu  6767  caucvgprlemloc  6771  caucvgprlemladdfu  6773  caucvgprlemladdrl  6774  caucvgprlem1  6775  caucvgprlem2  6776  caucvgpr  6778  caucvgprprlemk  6779  caucvgprprlemloccalc  6780  caucvgprprlemnkltj  6785  caucvgprprlemnkeqj  6786  caucvgprprlemnjltk  6787  caucvgprprlemnkj  6788  caucvgprprlemnbj  6789  caucvgprprlemml  6790  caucvgprprlemmu  6791  caucvgprprlemopl  6793  caucvgprprlemopu  6795  caucvgprprlemloc  6799  caucvgprprlemexbt  6802  caucvgprprlemexb  6803  caucvgprprlemaddq  6804  caucvgprprlem1  6805  caucvgprprlem2  6806  caucvgprpr  6808  addcmpblnr  6822  mulcmpblnrlemg  6823  mulcmpblnr  6824  prsrlem1  6825  ltsrprg  6830  mulcomsrg  6840  mulasssrg  6841  distrsrg  6842  lttrsr  6845  ltsosr  6847  ltasrg  6853  pn0sr  6854  negexsr  6855  recexgt0sr  6856  mulgt0sr  6860  aptisr  6861  mulextsr1lem  6862  mulextsr1  6863  archsr  6864  srpospr  6865  prsradd  6868  prsrlt  6869  prsrriota  6870  caucvgsrlemcl  6871  caucvgsrlemfv  6873  caucvgsrlemcau  6875  caucvgsrlemgt1  6877  caucvgsrlemoffval  6878  caucvgsrlemofff  6879  caucvgsrlemoffcau  6880  caucvgsrlemoffgt1  6881  caucvgsrlemoffres  6882  addcnsr  6908  mulcnsr  6909  addcnsrec  6916  mulcnsrec  6917  ltrennb  6928  recidpipr  6930  recidpirqlemcalc  6931  recidpirq  6932  axaddcl  6938  axmulcl  6940  axmulcom  6943  axmulass  6945  axdistr  6946  axrnegex  6951  axcnre  6953  rereceu  6961  recriota  6962  nntopi  6966  axcaucvglemval  6969  axcaucvglemcau  6970  axcaucvglemres  6971  addcld  7044  mulcld  7045  mulcomd  7046  readdcld  7053  remulcld  7054  lelttr  7104  ltletr  7105  gtned  7128  lttri3d  7130  letri3d  7131  lenltd  7132  ltled  7133  readdcan  7151  addcomd  7162  cnegex  7187  negeu  7200  addsubass  7219  subsub2  7237  subsub4  7242  negcon1d  7314  neg11ad  7316  subcld  7320  pncand  7321  pncan2d  7322  pncan3d  7323  npcand  7324  nncand  7325  negsubd  7326  subnegd  7327  subeq0d  7328  subne0d  7329  subeq0ad  7330  negdid  7333  negdi2d  7334  negsubdid  7335  negsubdi2d  7336  neg2subd  7337  resubcld  7377  mulneg1d  7406  mulneg2d  7407  mul2negd  7408  ltadd2  7414  posdif  7448  add20  7467  ltnegd  7512  lenegd  7513  ltnegcon1d  7514  ltnegcon2d  7515  lenegcon1d  7516  lenegcon2d  7517  ltaddposd  7518  ltaddpos2d  7519  ltsubposd  7520  posdifd  7521  addge01d  7522  addge02d  7523  subge0d  7524  suble0d  7525  subge02d  7526  rimul  7574  rereim  7575  apreap  7576  reapmul1lem  7583  reapmul1  7584  reapadd1  7585  reapneg  7586  remulext1  7588  cru  7591  apreim  7592  apsym  7595  addext  7599  apneg  7600  mulext1  7601  mulext  7603  apti  7611  leltap  7613  gt0ap0d  7617  ltap  7620  ltapd  7625  ap0gt0d  7628  recexaplem2  7631  recexap  7632  mulap0bd  7636  mulcanapd  7640  muleqadd  7647  receuap  7648  divmulap  7652  divdivdivap  7687  divcanap6  7693  recclapd  7755  recap0d  7756  recidapd  7757  recidap2d  7758  recrecapd  7759  dividapd  7760  div0apd  7761  rerecclapd  7805  recgt0  7814  prodgt0  7816  lt2msq  7850  lediv12a  7858  lediv2a  7859  recreclt  7864  recgt0d  7898  creui  7910  nnge1  7935  nnaddcld  7959  nnmulcld  7960  nndivred  7961  halfaddsub  8157  lt2halves  8158  addltmul  8159  nn0addcld  8237  nn0mulcld  8238  gtndiv  8333  zaddcld  8362  zsubcld  8363  zmulcld  8364  uzneg  8489  uzm1  8501  uzin  8503  uzind4  8529  qmulcl  8570  qapne  8572  rpaddcld  8636  rpmulcld  8637  rpdivcld  8638  ltrecd  8639  lerecd  8640  ltrec1d  8641  lerec2d  8642  ge0p1rpd  8651  rerpdivcld  8652  ltsubrpd  8653  ltaddrpd  8654  xrlelttr  8720  xrltletr  8721  ixxdisj  8770  ixxss1  8771  ixxss2  8772  iccsupr  8833  icoshft  8856  icoshftf1o  8857  icodisj  8858  elfz1eq  8897  fzen  8905  fzsplit  8913  elfz1end  8917  fznatpl1  8936  fzdifsuc  8941  uzdisj  8953  fseq1p1m1  8954  fzm1  8960  fzneuz  8961  fznuz  8962  uznfz  8963  fznn0sub2  8983  nn0disj  8993  elfzoelz  9002  elfzouz2  9015  fzonnsub  9023  fzospliti  9030  fzosplit  9031  fzodisj  9032  elfzo1  9044  eluzgtdifelfzo  9051  fzocatel  9053  zpnn0elfzo  9061  fzostep1  9091  fvinim0ffz  9094  subfzo0  9095  qtri3or  9096  qbtwnzlemstep  9101  qbtwnz  9104  qbtwnre  9109  flqlelt  9116  flqge  9122  flqlt  9123  flqwordi  9128  flqbi2  9131  fldivnn0  9135  flqaddz  9137  flqmulnn0  9139  flltdivnn0lt  9144  ceilqval  9146  frec2uzsucd  9161  frec2uzltd  9163  frec2uzlt2d  9164  frecuzrdgrrn  9168  frec2uzrdg  9169  frecuzrdgrom  9170  frecuzrdglem  9171  frecuzrdg0  9174  frecuzrdgsuc  9175  frecfzen2  9178  fzfig  9180  fzfigd  9181  iseqeq3  9190  iseqm1  9201  iseqfveq2  9202  iseqfeq2  9203  iseqshft2  9206  monoord  9209  monoord2  9210  iseqsplit  9212  iseqcaopr3  9214  iseqid  9221  iseqhomo  9222  iseqdistr  9223  expivallem  9230  expival  9231  expcl2lemap  9241  expap0  9259  expgt1  9267  mulexp  9268  mulexpzap  9269  expadd  9271  expaddzaplem  9272  expaddzap  9273  expmulzap  9275  ltexp2a  9280  leexp2a  9281  leexp2r  9282  bernneq  9343  expnbnd  9346  expnlbnd  9347  expnlbnd2  9348  expeq0d  9351  expcld  9355  expp1d  9356  sqrecapd  9359  sqmuld  9367  reexpcld  9372  nnexpcld  9376  nn0expcld  9377  rpexpcld  9378  sqgt0apd  9382  shftfvalg  9393  shftfval  9396  shftval2  9401  shftval5  9404  crre  9431  remim  9434  mulreap  9438  recj  9441  reneg  9442  readd  9443  remullem  9445  imcj  9449  imneg  9450  imadd  9451  cjexp  9467  cjap  9480  cjdivap  9483  cnrecnv  9484  cjexpd  9532  readdd  9533  imaddd  9534  resubd  9535  imsubd  9536  remuld  9537  immuld  9538  cjaddd  9539  cjmuld  9540  ipcnd  9541  remul2d  9546  immul2d  9547  crred  9550  crimd  9551  caucvgrelemcau  9553  caucvgre  9554  cvg1nlemcau  9557  cvg1nlemres  9558  recvguniq  9567  resqrexlemover  9582  resqrexlemdecn  9584  resqrexlemcalc1  9586  resqrexlemcalc2  9587  resqrexlemnmsq  9589  resqrexlemnm  9590  resqrexlemcvg  9591  resqrexlemoverl  9593  resqrexlemglsq  9594  resqrexlemga  9595  resqrtcl  9601  rersqrtthlem  9602  sqrtmul  9607  rpsqrtcl  9613  sqrtdiv  9614  abscl  9623  absvalsq  9625  absge0  9632  abs00ap  9634  absreim  9640  absdivap  9642  leabs  9646  absexp  9649  absexpzap  9650  sqabs  9652  ltabs  9657  abslt  9658  absle  9659  abssubap0  9660  abssubne0  9661  absidm  9668  abssubge0  9672  abstri  9674  abs3dif  9675  abs2difabs  9678  fzomaxdiflem  9682  caubnd2  9687  amgm2  9688  absnidd  9730  resqrtcld  9733  sqrtmsqd  9734  sqrtsqd  9735  sqrtge0d  9736  absidd  9737  absltd  9744  absled  9745  absrpclapd  9758  absexpd  9762  abssubd  9763  absmuld  9764  abstrid  9766  abs2difd  9767  abs2dif2d  9768  abs2difabsd  9769  climconst  9785  climuni  9788  climmpt  9795  climshft  9799  climshft2  9801  climcn2  9804  mulcn2  9807  cn1lem  9808  cjcn2  9810  climrecl  9818  climle  9828  iserile  9836  climcau  9840  climcvg1nlem  9842  serif0  9845  nn0seqcvgd  9854  ialgr0  9857  ialgrp1  9859  ialgcvg  9861  algcvgb  9863  spimd  9879  bdssexd  9999
  Copyright terms: Public domain W3C validator