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

Theorem adantl 262
Description: Inference adding a conjunct to the left of an antecedent. (Contributed by NM, 30-Aug-1993.) (Proof shortened by Wolf Lammen, 23-Nov-2012.)
Hypothesis
Ref Expression
adantl.1  |-  ( ph  ->  ps )
Assertion
Ref Expression
adantl  |-  ( ( ch  /\  ph )  ->  ps )

Proof of Theorem adantl
StepHypRef Expression
1 adantl.1 . . 3  |-  ( ph  ->  ps )
21adantr 261 . 2  |-  ( (
ph  /\  ch )  ->  ps )
32ancoms 255 1  |-  ( ( ch  /\  ph )  ->  ps )
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-ia1 99  ax-ia2 100  ax-ia3 101
This theorem is referenced by:  sylan2  270  anim12ii  325  sylan9bb  435  ad2antrl  459  ad2antll  460  im2anan9  530  bi2bian9  540  jaao  639  ordi  729  con1bidc  768  con1bdc  772  dfandc  778  stabtestimpdc  824  dcor  843  annimdc  845  ccase2  873  rnlem  883  simpr1  910  simpr2  911  simpr3  912  3ad2ant3  927  simprl1  949  simprl2  950  simprl3  951  simprr1  952  simprr2  953  simprr3  954  simpr1l  961  simpr1r  962  simpr2l  963  simpr2r  964  simpr3l  965  simpr3r  966  simpr11  988  simpr12  989  simpr13  990  simpr21  991  simpr22  992  simpr23  993  simpr31  994  simpr32  995  simpr33  996  falimd  1258  xorbin  1275  xor2dc  1281  biassdc  1286  dfbi3dc  1288  xordidc  1290  ax11v2  1701  ax11b  1707  equs5or  1711  nfsbxyt  1819  sbcomxyyz  1846  2exeu  1992  dimatis  2017  gencbvex  2600  gencbval  2602  elrab3t  2697  euind  2728  reu6  2730  reuind  2744  sbcan  2805  sbcralt  2834  sbcrext  2835  csbcomg  2873  csbiebt  2886  sbcnestgf  2897  sseq1  2966  ddifnel  3075  elin  3126  undif3ss  3198  uneqdifeqim  3308  ifcldcd  3358  disjpr2  3434  diftpsn3  3505  preqr1g  3537  nfopd  3566  unissel  3609  trel  3861  iinexgm  3908  copsex2t  3982  sowlin  4057  efrirr  4090  ordelon  4120  alxfr  4193  ralxfr  4198  rexxfr  4200  rabxfr  4202  reuhyp  4204  ordelsuc  4231  onsucelsucr  4234  onsucsssucr  4235  onintonm  4243  ordtriexmidlem  4245  ordtri2or2exmidlem  4251  onsucelsucexmidlem  4254  ordsucunielexmid  4256  regexmidlem1  4258  reg2exmidlema  4259  preleq  4279  eunex  4285  ordsuc  4287  nlimsucg  4290  onnmin  4292  wessep  4302  tfi  4305  peano2  4318  opeliunxp  4395  posng  4412  sosng  4413  eqrelrdv2  4439  ideqg  4487  opeldmg  4540  relssres  4648  exse2  4699  brcodir  4712  xpidtr  4715  poltletr  4725  ssxpbm  4756  ssxp1  4757  ssxp2  4758  xpexr2m  4762  rnpropg  4800  elxp4  4808  elxp5  4809  dfco2a  4821  iota5  4887  iota2  4893  funssres  4942  funun  4944  fnsng  4947  fununi  4967  funimaexglem  4982  fneu  5003  fco  5056  fco2  5057  funssxp  5060  fssres2  5067  f1orescnv  5142  nffvd  5187  fnsnfv  5232  ssimaex  5234  funfvdm2  5237  dmfco  5241  fvco2  5242  fvmptss2  5247  respreima  5295  rexrn  5304  ralrn  5305  elrnrexdm  5306  ralrnmpt  5309  rexrnmpt  5310  ffvresb  5328  fcompt  5333  xpsng  5338  fprg  5346  fsnunres  5364  resfunexg  5382  funfvima3  5392  rexima  5394  ralima  5395  f1veqaeq  5408  f1ocnvfv1  5417  f1ocnvfv2  5418  fcofo  5424  foeqcnvco  5430  f1eqcocnv  5431  isoresbr  5449  isoini  5457  isoselem  5459  f1oiso  5465  riotabiia  5485  riota2f  5489  riota5f  5492  eloprabga  5591  ovmpt2x  5629  ovmpt2ga  5630  ovg  5639  oprssov  5642  caovcl  5655  caovimo  5694  f1opw2  5706  ofres  5725  resfunexgALT  5737  cofunexg  5738  iunexg  5746  offval3  5761  f2ndres  5787  elxp6  5796  releldm2  5811  oprabco  5838  1stconst  5842  2ndconst  5843  cnvf1o  5846  fo2ndf  5848  f1o2ndf1  5849  poxp  5853  mpt2xopoveq  5855  sprmpt2  5857  isprmpt2  5858  reldmtpos  5868  dftpos4  5878  tposf2  5883  iunon  5899  iordsmo  5912  tfrlem1  5923  tfrlemisucaccv  5939  tfrlemi1  5946  tfrexlem  5948  tfri3  5953  rdgivallem  5968  rdgon  5973  freccl  5993  oasuc  6044  omsuc  6051  nnaass  6064  nndi  6065  nnsucelsuc  6070  nntri1  6074  nntri3  6075  nntri2or2  6076  nnsseleq  6079  nndifsnid  6080  nnaordi  6081  nnaword  6084  nnmord  6090  nnm00  6102  swoer  6134  eqer  6138  0er  6140  relelec  6146  ectocl  6173  iinerm  6178  eroveu  6197  ecopovtrn  6203  ecopover  6204  ecopovsymg  6205  ecopovtrng  6206  ecopoverg  6207  th3qlem1  6208  ecovass  6215  ecoviass  6216  ecovdi  6217  ecovidi  6218  ener  6259  fundmen  6286  cnven  6288  xpcomco  6300  xpdom2  6305  fopwdom  6310  phplem4  6318  phplem4dom  6324  nndomo  6326  phplem4on  6329  fidceq  6330  fidifsnen  6331  fidifsnid  6332  dif1en  6337  fin0  6342  fin0or  6343  findcard2  6346  findcard2s  6347  diffisn  6350  ac6sfi  6352  ordiso2  6355  cardcl  6359  isnumi  6360  carden2bex  6367  ltpiord  6415  ltsopi  6416  mulclpi  6424  addasspig  6426  mulasspig  6428  distrpig  6429  addnidpig  6432  ltapig  6434  ltmpig  6435  indpi  6438  nnppipi  6439  enqdc1  6458  addcmpblnq  6463  mulcmpblnq  6464  ordpipqqs  6470  addassnqg  6478  mulcanenq  6481  distrnqg  6483  mulidnq  6485  recmulnqg  6487  ltsonq  6494  ltanqg  6496  ltmnqg  6497  ltaddnq  6503  ltexnqq  6504  halfnqq  6506  ltbtwnnqq  6511  archnqq  6513  prarloclemarch  6514  prarloclemarch2  6515  ltrnqg  6516  enq0tr  6530  enq0er  6531  nqnq0  6537  addcmpblnq0  6539  mulcmpblnq0  6540  mulcanenq0ec  6541  nnnq0lem1  6542  mulnnnq0  6546  nqnq0a  6550  nqnq0m  6551  nq0m0r  6552  nq0a0  6553  distrnq0  6555  addassnq0  6558  nq02m  6561  prcdnql  6580  prcunqu  6581  prubl  6582  prloc  6587  prarloclemlt  6589  prarloclemlo  6590  prarloc  6599  genplt2i  6606  genprndl  6617  genprndu  6618  genpdisj  6619  genpassl  6620  genpassu  6621  addnqprllem  6623  addnqprulem  6624  addnqprl  6625  addnqpru  6626  addlocprlemeqgt  6628  nqprloc  6641  nqprl  6647  nqpru  6648  addnqprlemrl  6653  addnqprlemru  6654  appdivnq  6659  prmuloc  6662  mulnqprl  6664  mulnqpru  6665  mullocprlem  6666  mulnqprlemrl  6669  mulnqprlemru  6670  distrlem4prl  6680  distrlem4pru  6681  1idprl  6686  1idpru  6687  ltpopr  6691  ltsopr  6692  ltaddpr  6693  ltexprlemupu  6700  ltexprlemdisj  6702  ltexprlemloc  6703  ltexprlemfl  6705  ltexprlemrl  6706  ltexprlemfu  6707  ltexprlemru  6708  addcanprleml  6710  ltaprg  6715  prplnqu  6716  addextpr  6717  recexprlemdisj  6726  recexprlemloc  6727  recexprlem1ssl  6729  recexprlem1ssu  6730  aptiprleml  6735  aptiprlemu  6736  caucvgprlemcanl  6740  cauappcvgprlemm  6741  cauappcvgprlemopl  6742  cauappcvgprlemlol  6743  cauappcvgprlemopu  6744  cauappcvgprlemdisj  6747  cauappcvgprlemloc  6748  cauappcvgprlemladdfu  6750  cauappcvgprlemladdfl  6751  cauappcvgprlemladdru  6752  cauappcvgprlemladdrl  6753  cauappcvgprlem1  6755  archrecpr  6760  caucvgprlemnkj  6762  caucvgprlemnbj  6763  caucvgprlemopl  6765  caucvgprlemlol  6766  caucvgprlemopu  6767  caucvgprlemdisj  6770  caucvgprlemloc  6771  caucvgprlemladdfu  6773  caucvgprlemladdrl  6774  caucvgprlemlim  6777  caucvgprprlemval  6784  caucvgprprlemnkltj  6785  caucvgprprlemnkeqj  6786  caucvgprprlemnbj  6789  caucvgprprlemmu  6791  caucvgprprlemopl  6793  caucvgprprlemlol  6794  caucvgprprlemopu  6795  caucvgprprlemdisj  6798  caucvgprprlemloc  6799  caucvgprprlemexbt  6802  caucvgprprlemexb  6803  caucvgprprlemaddq  6804  caucvgprprlemlim  6807  mulcmpblnrlemg  6823  ltsrprg  6830  mulasssrg  6841  distrsrg  6842  lttrsr  6845  ltposr  6846  ltsosr  6847  0idsr  6850  1idsr  6851  ltasrg  6853  recexgt0sr  6856  mulgt0sr  6860  mulextsr1lem  6862  archsr  6864  srpospr  6865  prsradd  6868  prsrlt  6869  caucvgsrlemfv  6873  caucvgsrlemoffval  6878  caucvgsrlemoffcau  6880  caucvgsrlemoffgt1  6881  caucvgsrlemoffres  6882  caucvgsr  6884  ltrennb  6928  axmulass  6945  axdistr  6946  ax0id  6950  axcnre  6953  axcaucvglemval  6969  axcaucvglemcau  6970  axcaucvglemres  6971  ltxrlt  7083  ltso  7094  muladd11  7144  readdcan  7151  cnegexlem1  7184  cnegexlem3  7186  cnegex  7187  addsubeq4  7224  subeq0  7235  renegcl  7270  mul2neg  7393  submul2  7394  ltleadd  7439  ltaddpos  7445  lt2sub  7453  le2sub  7454  lenegcon2  7460  recexre  7567  apirr  7594  apsym  7595  apneg  7600  apti  7611  recextlem1  7630  recexap  7632  mulap0  7633  divvalap  7651  rec11ap  7684  divdivdivap  7687  divmul24ap  7690  divmuleqap  7691  divadddivap  7701  conjmulap  7703  letrp1  7812  ltdivmul  7840  lerec2  7853  ledivdiv  7854  cju  7911  nn1suc  7931  nn2ge  7944  nnsub  7950  nndiv  7952  halfaddsub  8157  nn0addcl  8215  nn0mulcl  8216  elnn0nn  8222  nn0ge2m1nn  8240  znegcl  8274  zaddcllempos  8280  zaddcllemneg  8282  zaddcl  8283  ztri3or  8286  zltnle  8289  zltp1le  8296  zltlem1  8299  elz2  8310  zdceq  8314  zdclt  8316  zdivadd  8327  gtndiv  8333  prime  8335  zneo  8337  zeo  8341  peano2uz2  8343  uzind  8347  fzind  8351  eluzuzle  8479  uztrn  8487  eluzp1l  8495  peano2uzr  8526  uzaddcl  8527  indstr  8534  indstr2  8544  ublbneg  8546  divfnzn  8554  qmulz  8556  qaddcl  8568  qnegcl  8569  qapne  8572  qreccl  8574  irradd  8578  irrmul  8579  divlt1lt  8648  divle1le  8649  ledivge1le  8650  xrltnsym  8712  xrlttr  8714  xrltso  8715  xrlttri3  8716  xrre  8731  xrre2  8732  xrre3  8733  xltnegi  8746  ixxss1  8771  ixxss2  8772  ixxss12  8773  ubioog  8781  iccss2  8811  iccssioo2  8813  iccssico2  8814  iccshftr  8860  iccshftl  8862  iccdil  8864  icccntr  8866  divelunit  8868  lincmb01cmp  8869  iccf1o  8870  fztri3or  8901  uzsubsubfz  8909  fzsplit2  8912  fzdisj  8914  fzaddel  8920  fzsubel  8921  fzss1  8924  fzss2  8925  fznatpl1  8936  fzdifsuc  8941  fzrev  8944  fzrev2  8945  fzrev2i  8946  fzrev3  8947  elfzm11  8951  uzsplit  8952  fzm1  8960  fzneuz  8961  elfz2nn0  8971  elfz0addOLD  8978  elfz0fzfz0  8981  fz0fzelfz0  8982  uzsubfz0  8984  fz0fzdiffz0  8985  elfzmlbmOLD  8987  elfzmlbp  8988  difelfzle  8990  difelfznle  8991  1fv  8994  fzon  9020  fzoss1  9025  fzouzdisj  9034  fzo1fzo0n0  9037  elfzo0z  9038  fzofzim  9042  fzoaddel2  9047  fzosubel2  9049  eluzgtdifelfzo  9051  elfzodifsumelfzo  9055  zpnn0elfzo1  9062  fzosplitsnm1  9063  elfzom1p1elfzo  9068  ssfzo12bi  9079  ubmelm1fzo  9080  fzofzp1b  9082  elfzom1b  9083  elfzomelpfzo  9085  peano2fzor  9086  fzoshftral  9092  fvinim0ffz  9094  subfzo0  9095  qtri3or  9096  qltnle  9099  qdceq  9100  qbtwnzlemshrink  9102  rebtwn2zlemshrink  9106  flqlt  9123  flqmulnn0  9139  flqeqceilz  9158  frec2uzzd  9160  frec2uzuzd  9162  frec2uzltd  9163  frec2uzlt2d  9164  frecuzrdgrrn  9168  frecuzrdgfn  9172  frecuzrdgsuc  9175  fzofig  9182  nn0ennn  9183  iseqfveq2  9202  iseqfeq2  9203  iseqshft2  9206  iserf  9207  iserfre  9208  monoord2  9210  isermono  9211  iseqsplit  9212  iseqcaopr3  9214  iseqcaopr2  9215  iseradd  9217  isersub  9218  iseqid3s  9220  iser0  9224  iser0f  9225  serige0  9226  serile  9227  expivallem  9230  expival  9231  expinnval  9232  exp1  9235  expp1  9236  expnegap0  9237  expm1t  9257  expap0  9259  expadd  9271  expsubap  9276  leexp1a  9283  subsq  9332  subsq2  9333  binom2sub  9338  bernneq  9343  bernneq3  9345  expnlbnd  9347  shftfib  9398  shftfn  9399  shftval3  9402  crre  9431  rereb  9437  mulreap  9438  readd  9443  resub  9444  remullem  9445  imadd  9451  imsub  9452  cjadd  9458  ipcnval  9460  cjsub  9466  caucvgrelemcau  9553  cvg1nlemcau  9557  rexuz3  9562  recvguniq  9567  sqrt0  9576  resqrexlemfp1  9581  resqrexlemover  9582  resqrexlemcalc3  9588  resqrexlemcvg  9591  resqrexlemgt0  9592  resqrexlemga  9595  sqrtmul  9607  sqrtdiv  9614  sqabsadd  9627  sqabssub  9628  absexp  9649  abs2dif2  9677  fzomaxdiflem  9682  cau3lem  9684  qdenre  9772  climconst  9785  2clim  9796  climshftlemg  9797  climres  9798  climshft2  9801  addcn2  9805  subcn2  9806  mulcn2  9807  climcn1lem  9813  climadd  9820  climmul  9821  climsub  9822  clim2iser  9831  clim2iser2  9832  iisermulc2  9834  iserile  9836  climserile  9839  climcau  9840  climcvg1nlem  9842  climcaucn  9844  serif0  9845  nn0seqcvgd  9854  ialgrlem1st  9855  algcvgblem  9862  ialgcvga  9864  ialgfx  9865  cbvrald  9901  bdsepnft  9981  bj-om  10035  bj-nnen2lp  10053  strcollnft  10083  sscoll2  10087
  Copyright terms: Public domain W3C validator