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  onunsnss  6355  snon0  6356  ordiso2  6357  cardcl  6361  isnumi  6362  carden2bex  6369  ltpiord  6417  ltsopi  6418  mulclpi  6426  addasspig  6428  mulasspig  6430  distrpig  6431  addnidpig  6434  ltapig  6436  ltmpig  6437  indpi  6440  nnppipi  6441  enqdc1  6460  addcmpblnq  6465  mulcmpblnq  6466  ordpipqqs  6472  addassnqg  6480  mulcanenq  6483  distrnqg  6485  mulidnq  6487  recmulnqg  6489  ltsonq  6496  ltanqg  6498  ltmnqg  6499  ltaddnq  6505  ltexnqq  6506  halfnqq  6508  ltbtwnnqq  6513  archnqq  6515  prarloclemarch  6516  prarloclemarch2  6517  ltrnqg  6518  enq0tr  6532  enq0er  6533  nqnq0  6539  addcmpblnq0  6541  mulcmpblnq0  6542  mulcanenq0ec  6543  nnnq0lem1  6544  mulnnnq0  6548  nqnq0a  6552  nqnq0m  6553  nq0m0r  6554  nq0a0  6555  distrnq0  6557  addassnq0  6560  nq02m  6563  prcdnql  6582  prcunqu  6583  prubl  6584  prloc  6589  prarloclemlt  6591  prarloclemlo  6592  prarloc  6601  genplt2i  6608  genprndl  6619  genprndu  6620  genpdisj  6621  genpassl  6622  genpassu  6623  addnqprllem  6625  addnqprulem  6626  addnqprl  6627  addnqpru  6628  addlocprlemeqgt  6630  nqprloc  6643  nqprl  6649  nqpru  6650  addnqprlemrl  6655  addnqprlemru  6656  appdivnq  6661  prmuloc  6664  mulnqprl  6666  mulnqpru  6667  mullocprlem  6668  mulnqprlemrl  6671  mulnqprlemru  6672  distrlem4prl  6682  distrlem4pru  6683  1idprl  6688  1idpru  6689  ltpopr  6693  ltsopr  6694  ltaddpr  6695  ltexprlemupu  6702  ltexprlemdisj  6704  ltexprlemloc  6705  ltexprlemfl  6707  ltexprlemrl  6708  ltexprlemfu  6709  ltexprlemru  6710  addcanprleml  6712  ltaprg  6717  prplnqu  6718  addextpr  6719  recexprlemdisj  6728  recexprlemloc  6729  recexprlem1ssl  6731  recexprlem1ssu  6732  aptiprleml  6737  aptiprlemu  6738  caucvgprlemcanl  6742  cauappcvgprlemm  6743  cauappcvgprlemopl  6744  cauappcvgprlemlol  6745  cauappcvgprlemopu  6746  cauappcvgprlemdisj  6749  cauappcvgprlemloc  6750  cauappcvgprlemladdfu  6752  cauappcvgprlemladdfl  6753  cauappcvgprlemladdru  6754  cauappcvgprlemladdrl  6755  cauappcvgprlem1  6757  archrecpr  6762  caucvgprlemnkj  6764  caucvgprlemnbj  6765  caucvgprlemopl  6767  caucvgprlemlol  6768  caucvgprlemopu  6769  caucvgprlemdisj  6772  caucvgprlemloc  6773  caucvgprlemladdfu  6775  caucvgprlemladdrl  6776  caucvgprlemlim  6779  caucvgprprlemval  6786  caucvgprprlemnkltj  6787  caucvgprprlemnkeqj  6788  caucvgprprlemnbj  6791  caucvgprprlemmu  6793  caucvgprprlemopl  6795  caucvgprprlemlol  6796  caucvgprprlemopu  6797  caucvgprprlemdisj  6800  caucvgprprlemloc  6801  caucvgprprlemexbt  6804  caucvgprprlemexb  6805  caucvgprprlemaddq  6806  caucvgprprlemlim  6809  mulcmpblnrlemg  6825  ltsrprg  6832  mulasssrg  6843  distrsrg  6844  lttrsr  6847  ltposr  6848  ltsosr  6849  0idsr  6852  1idsr  6853  ltasrg  6855  recexgt0sr  6858  mulgt0sr  6862  mulextsr1lem  6864  archsr  6866  srpospr  6867  prsradd  6870  prsrlt  6871  caucvgsrlemfv  6875  caucvgsrlemoffval  6880  caucvgsrlemoffcau  6882  caucvgsrlemoffgt1  6883  caucvgsrlemoffres  6884  caucvgsr  6886  ltrennb  6930  axmulass  6947  axdistr  6948  ax0id  6952  axcnre  6955  axcaucvglemval  6971  axcaucvglemcau  6972  axcaucvglemres  6973  ltxrlt  7085  ltso  7096  muladd11  7146  readdcan  7153  cnegexlem1  7186  cnegexlem3  7188  cnegex  7189  addsubeq4  7226  subeq0  7237  renegcl  7272  mul2neg  7395  submul2  7396  ltleadd  7441  ltaddpos  7447  lt2sub  7455  le2sub  7456  lenegcon2  7462  recexre  7569  apirr  7596  apsym  7597  apneg  7602  apti  7613  recextlem1  7632  recexap  7634  mulap0  7635  divvalap  7653  rec11ap  7686  divdivdivap  7689  divmul24ap  7692  divmuleqap  7693  divadddivap  7703  conjmulap  7705  letrp1  7814  ltdivmul  7842  lerec2  7855  ledivdiv  7856  cju  7913  nn1suc  7933  nn2ge  7946  nnsub  7952  nndiv  7954  halfaddsub  8159  nn0addcl  8217  nn0mulcl  8218  elnn0nn  8224  nn0ge2m1nn  8242  znegcl  8276  zaddcllempos  8282  zaddcllemneg  8284  zaddcl  8285  ztri3or  8288  zltnle  8291  zltp1le  8298  zltlem1  8301  elz2  8312  zdceq  8316  zdclt  8318  zdivadd  8329  gtndiv  8335  prime  8337  zneo  8339  zeo  8343  peano2uz2  8345  uzind  8349  fzind  8353  eluzuzle  8481  uztrn  8489  eluzp1l  8497  peano2uzr  8528  uzaddcl  8529  indstr  8536  indstr2  8546  ublbneg  8548  divfnzn  8556  qmulz  8558  qaddcl  8570  qnegcl  8571  qapne  8574  qreccl  8576  irradd  8580  irrmul  8581  divlt1lt  8650  divle1le  8651  ledivge1le  8652  xrltnsym  8714  xrlttr  8716  xrltso  8717  xrlttri3  8718  xrre  8733  xrre2  8734  xrre3  8735  xltnegi  8748  ixxss1  8773  ixxss2  8774  ixxss12  8775  ubioog  8783  iccss2  8813  iccssioo2  8815  iccssico2  8816  iccshftr  8862  iccshftl  8864  iccdil  8866  icccntr  8868  divelunit  8870  lincmb01cmp  8871  iccf1o  8872  fztri3or  8903  uzsubsubfz  8911  fzsplit2  8914  fzdisj  8916  fzaddel  8922  fzsubel  8923  fzss1  8926  fzss2  8927  fznatpl1  8938  fzdifsuc  8943  fzrev  8946  fzrev2  8947  fzrev2i  8948  fzrev3  8949  elfzm11  8953  uzsplit  8954  fzm1  8962  fzneuz  8963  elfz2nn0  8973  elfz0addOLD  8980  elfz0fzfz0  8983  fz0fzelfz0  8984  uzsubfz0  8986  fz0fzdiffz0  8987  elfzmlbmOLD  8989  elfzmlbp  8990  difelfzle  8992  difelfznle  8993  1fv  8996  fzon  9022  fzoss1  9027  fzouzdisj  9036  fzo1fzo0n0  9039  elfzo0z  9040  fzofzim  9044  fzoaddel2  9049  fzosubel2  9051  eluzgtdifelfzo  9053  elfzodifsumelfzo  9057  zpnn0elfzo1  9064  fzosplitsnm1  9065  elfzom1p1elfzo  9070  ssfzo12bi  9081  ubmelm1fzo  9082  fzofzp1b  9084  elfzom1b  9085  elfzomelpfzo  9087  peano2fzor  9088  fzoshftral  9094  fvinim0ffz  9096  subfzo0  9097  qtri3or  9098  qltnle  9101  qdceq  9102  qbtwnzlemshrink  9104  rebtwn2zlemshrink  9108  flqlt  9125  flqmulnn0  9141  flqeqceilz  9160  intfracq  9162  flqdiv  9163  zmod1congr  9183  frec2uzzd  9186  frec2uzuzd  9188  frec2uzltd  9189  frec2uzlt2d  9190  frecuzrdgrrn  9194  frecuzrdgfn  9198  frecuzrdgsuc  9201  fzofig  9208  nn0ennn  9209  iseqfveq2  9228  iseqfeq2  9229  iseqshft2  9232  iserf  9233  iserfre  9234  monoord2  9236  isermono  9237  iseqsplit  9238  iseqcaopr3  9240  iseqcaopr2  9241  iseradd  9243  isersub  9244  iseqid3s  9246  iser0  9250  iser0f  9251  serige0  9252  serile  9253  expivallem  9256  expival  9257  expinnval  9258  exp1  9261  expp1  9262  expnegap0  9263  expm1t  9283  expap0  9285  expadd  9297  expsubap  9302  leexp1a  9309  subsq  9358  subsq2  9359  binom2sub  9364  bernneq  9369  bernneq3  9371  expnlbnd  9373  shftfib  9424  shftfn  9425  shftval3  9428  crre  9457  rereb  9463  mulreap  9464  readd  9469  resub  9470  remullem  9471  imadd  9477  imsub  9478  cjadd  9484  ipcnval  9486  cjsub  9492  caucvgrelemcau  9579  cvg1nlemcau  9583  rexuz3  9588  recvguniq  9593  sqrt0  9602  resqrexlemfp1  9607  resqrexlemover  9608  resqrexlemcalc3  9614  resqrexlemcvg  9617  resqrexlemgt0  9618  resqrexlemga  9621  sqrtmul  9633  sqrtdiv  9640  sqabsadd  9653  sqabssub  9654  absexp  9675  abs2dif2  9703  fzomaxdiflem  9708  cau3lem  9710  qdenre  9798  climconst  9811  2clim  9822  climshftlemg  9823  climres  9824  climshft2  9827  addcn2  9831  subcn2  9832  mulcn2  9833  climcn1lem  9839  climadd  9846  climmul  9847  climsub  9848  clim2iser  9857  clim2iser2  9858  iisermulc2  9860  iserile  9862  climserile  9865  climcau  9866  climcvg1nlem  9868  climcaucn  9870  serif0  9871  nn0seqcvgd  9880  ialgrlem1st  9881  algcvgblem  9888  ialgcvga  9890  ialgfx  9891  cbvrald  9927  bdsepnft  10007  bj-om  10061  bj-nnen2lp  10079  strcollnft  10109  sscoll2  10113
  Copyright terms: Public domain W3C validator