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

Theorem adantl 271
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 270 . 2  |-  ( (
ph  /\  ch )  ->  ps )
32ancoms 264 1  |-  ( ( ch  /\  ph )  ->  ps )
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-ia1 104  ax-ia2 105  ax-ia3 106
This theorem is referenced by:  sylan2  280  anim12ii  335  simplbiim  379  sylan9bb  450  ad2antrl  474  ad2antll  475  im2anan9  563  bi2bian9  573  jaao  672  ordi  763  con1bidc  802  con1bdc  806  dfandc  812  stabtestimpdc  858  dcor  877  annimdc  879  orandc  881  ccase2  908  rnlem  918  simpr1  945  simpr2  946  simpr3  947  3ad2ant3  962  simprl1  984  simprl2  985  simprl3  986  simprr1  987  simprr2  988  simprr3  989  simpr1l  996  simpr1r  997  simpr2l  998  simpr2r  999  simpr3l  1000  simpr3r  1001  simpr11  1023  simpr12  1024  simpr13  1025  simpr21  1026  simpr22  1027  simpr23  1028  simpr31  1029  simpr32  1030  simpr33  1031  falimd  1300  xorbin  1316  xor2dc  1322  biassdc  1327  dfbi3dc  1329  xordidc  1331  ax11v2  1742  ax11b  1748  equs5or  1752  nfsbxyt  1861  sbcomxyyz  1888  2exeu  2034  dimatis  2059  gencbvex  2646  gencbval  2648  rspcdva  2708  elrab3t  2749  euind  2780  reu6  2782  reuind  2796  sbcan  2857  sbcralt  2891  sbcrext  2892  csbcomg  2930  csbiebt  2943  sbcnestgf  2954  sseq1  3021  ddifnel  3104  elin  3156  undif3ss  3232  uneqdifeqim  3335  ifcldadc  3386  ifeq1dadc  3387  ifcldcd  3389  disjpr2  3464  diftpsn3  3535  preqr1g  3566  nfopd  3595  unissel  3638  trel  3890  iinexgm  3937  copsex2t  4008  sowlin  4083  efrirr  4116  ordelon  4146  alxfr  4219  ralxfr  4224  rexxfr  4226  rabxfr  4228  reuhyp  4230  ordelsuc  4257  onsucelsucr  4260  onsucsssucr  4261  onintonm  4269  ordtriexmidlem  4271  ordtri2or2exmidlem  4277  onsucelsucexmidlem  4280  ordsucunielexmid  4282  regexmidlem1  4284  reg2exmidlema  4285  preleq  4306  eunex  4312  ordsuc  4314  nlimsucg  4317  onnmin  4319  wessep  4328  tfi  4331  peano2  4344  posng  4438  sosng  4439  eqrelrdv2  4465  ideqg  4515  opeldmg  4568  relssres  4676  exse2  4729  brcodir  4742  xpidtr  4745  poltletr  4755  ssxpbm  4786  ssxp1  4787  ssxp2  4788  xpexr2m  4792  rnpropg  4830  elxp4  4838  elxp5  4839  dfco2a  4851  iota5  4917  iota2  4923  funssres  4972  funun  4974  fnsng  4977  fununi  4998  funimaexglem  5013  fneu  5034  fco  5087  fco2  5088  funssxp  5091  fssres2  5098  f1orescnv  5173  nffvd  5218  fnsnfv  5264  ssimaex  5266  funfvdm2  5269  dmfco  5273  fvco2  5274  fvmptss2  5279  respreima  5327  rexrn  5336  ralrn  5337  elrnrexdm  5338  ralrnmpt  5341  rexrnmpt  5342  ffvresb  5360  fcompt  5365  xpsng  5370  fprg  5378  fsnunres  5396  resfunexg  5414  funfvima3  5424  rexima  5426  ralima  5427  f1veqaeq  5440  f1ocnvfv1  5448  f1ocnvfv2  5449  fcofo  5455  foeqcnvco  5461  f1eqcocnv  5462  isoresbr  5480  isoini  5488  isoselem  5490  f1oiso  5496  riotabiia  5516  riota2f  5520  riota5f  5523  eloprabga  5622  ovmpt2x  5660  ovmpt2ga  5661  ovg  5670  oprssov  5673  caovcl  5686  caovimo  5725  f1opw2  5737  ofres  5756  resfunexgALT  5768  cofunexg  5769  iunexg  5777  offval3  5792  f2ndres  5818  elxp6  5827  releldm2  5842  oprabco  5869  1stconst  5873  2ndconst  5874  cnvf1o  5877  fo2ndf  5879  f1o2ndf1  5880  poxp  5884  cnvoprab  5886  mpt2xopoveq  5889  sprmpt2  5891  isprmpt2  5892  reldmtpos  5902  dftpos4  5912  tposf2  5917  iunon  5933  iordsmo  5946  tfrlem1  5957  tfrlemisucaccv  5974  tfrlemi1  5981  tfrexlem  5983  tfr1onlemsucaccv  5990  tfri1dALT  6000  tfrcllemsucaccv  6003  tfri3  6016  rdgivallem  6030  rdgon  6035  frecabcl  6048  freccllem  6051  frecfcllem  6053  frecsuclem  6055  oasuc  6108  oawordriexmid  6114  omsuc  6116  nnaass  6129  nndi  6130  nnsucelsuc  6135  nnsucuniel  6139  nntri1  6140  nntri3  6141  nntri2or2  6142  nnsseleq  6145  nndifsnid  6146  nnaordi  6147  nnaword  6150  nnmord  6156  nnm00  6168  swoer  6200  eqer  6204  0er  6206  relelec  6212  ectocl  6239  iinerm  6244  eroveu  6263  ecopovtrn  6269  ecopover  6270  ecopovsymg  6271  ecopovtrng  6272  ecopoverg  6273  th3qlem1  6274  ecovass  6281  ecoviass  6282  ecovdi  6283  ecovidi  6284  ener  6326  fundmen  6353  cnven  6355  1domsn  6363  xpcomco  6370  xpdom2  6375  fopwdom  6380  xpf1o  6385  phplem4  6390  phplem4dom  6397  nndomo  6399  phplem4on  6402  fidceq  6404  fidifsnen  6405  fidifsnid  6406  infiexmid  6412  dif1en  6414  fin0  6419  fin0or  6420  findcard2  6423  findcard2s  6424  diffisn  6427  infnfi  6429  ac6sfi  6431  infm  6432  en2eqpr  6434  onunsnss  6437  unsnfidcex  6440  unsnfidcel  6441  snon0  6445  relcnvfi  6449  eqsupti  6468  supsnti  6477  cnvti  6491  ordiso2  6505  cardcl  6509  isnumi  6510  carden2bex  6517  ltpiord  6571  ltsopi  6572  mulclpi  6580  addasspig  6582  mulasspig  6584  distrpig  6585  addnidpig  6588  ltapig  6590  ltmpig  6591  indpi  6594  nnppipi  6595  enqdc1  6614  addcmpblnq  6619  mulcmpblnq  6620  ordpipqqs  6626  addassnqg  6634  mulcanenq  6637  distrnqg  6639  mulidnq  6641  recmulnqg  6643  ltsonq  6650  ltanqg  6652  ltmnqg  6653  ltaddnq  6659  ltexnqq  6660  halfnqq  6662  ltbtwnnqq  6667  archnqq  6669  prarloclemarch  6670  prarloclemarch2  6671  ltrnqg  6672  enq0tr  6686  enq0er  6687  nqnq0  6693  addcmpblnq0  6695  mulcmpblnq0  6696  mulcanenq0ec  6697  nnnq0lem1  6698  mulnnnq0  6702  nqnq0a  6706  nqnq0m  6707  nq0m0r  6708  nq0a0  6709  distrnq0  6711  addassnq0  6714  nq02m  6717  prcdnql  6736  prcunqu  6737  prubl  6738  prloc  6743  prarloclemlt  6745  prarloclemlo  6746  prarloc  6755  genplt2i  6762  genprndl  6773  genprndu  6774  genpdisj  6775  genpassl  6776  genpassu  6777  addnqprllem  6779  addnqprulem  6780  addnqprl  6781  addnqpru  6782  addlocprlemeqgt  6784  nqprloc  6797  nqprl  6803  nqpru  6804  addnqprlemrl  6809  addnqprlemru  6810  appdivnq  6815  prmuloc  6818  mulnqprl  6820  mulnqpru  6821  mullocprlem  6822  mulnqprlemrl  6825  mulnqprlemru  6826  distrlem4prl  6836  distrlem4pru  6837  1idprl  6842  1idpru  6843  ltpopr  6847  ltsopr  6848  ltaddpr  6849  ltexprlemupu  6856  ltexprlemdisj  6858  ltexprlemloc  6859  ltexprlemfl  6861  ltexprlemrl  6862  ltexprlemfu  6863  ltexprlemru  6864  addcanprleml  6866  ltaprg  6871  prplnqu  6872  addextpr  6873  recexprlemdisj  6882  recexprlemloc  6883  recexprlem1ssl  6885  recexprlem1ssu  6886  aptiprleml  6891  aptiprlemu  6892  caucvgprlemcanl  6896  cauappcvgprlemm  6897  cauappcvgprlemopl  6898  cauappcvgprlemlol  6899  cauappcvgprlemopu  6900  cauappcvgprlemdisj  6903  cauappcvgprlemloc  6904  cauappcvgprlemladdfu  6906  cauappcvgprlemladdfl  6907  cauappcvgprlemladdru  6908  cauappcvgprlemladdrl  6909  cauappcvgprlem1  6911  archrecpr  6916  caucvgprlemnkj  6918  caucvgprlemnbj  6919  caucvgprlemopl  6921  caucvgprlemlol  6922  caucvgprlemopu  6923  caucvgprlemdisj  6926  caucvgprlemloc  6927  caucvgprlemladdfu  6929  caucvgprlemladdrl  6930  caucvgprlemlim  6933  caucvgprprlemval  6940  caucvgprprlemnkltj  6941  caucvgprprlemnkeqj  6942  caucvgprprlemnbj  6945  caucvgprprlemmu  6947  caucvgprprlemopl  6949  caucvgprprlemlol  6950  caucvgprprlemopu  6951  caucvgprprlemdisj  6954  caucvgprprlemloc  6955  caucvgprprlemexbt  6958  caucvgprprlemexb  6959  caucvgprprlemaddq  6960  caucvgprprlemlim  6963  mulcmpblnrlemg  6979  ltsrprg  6986  mulasssrg  6997  distrsrg  6998  lttrsr  7001  ltposr  7002  ltsosr  7003  0idsr  7006  1idsr  7007  ltasrg  7009  recexgt0sr  7012  mulgt0sr  7016  mulextsr1lem  7018  archsr  7020  srpospr  7021  prsradd  7024  prsrlt  7025  caucvgsrlemfv  7029  caucvgsrlemoffval  7034  caucvgsrlemoffcau  7036  caucvgsrlemoffgt1  7037  caucvgsrlemoffres  7038  caucvgsr  7040  ltrennb  7084  axmulass  7101  axdistr  7102  ax0id  7106  axcnre  7109  axcaucvglemval  7125  axcaucvglemcau  7126  axcaucvglemres  7127  ltxrlt  7245  ltso  7256  muladd11  7308  readdcan  7315  cnegexlem1  7350  cnegexlem3  7352  cnegex  7353  addsubeq4  7390  subeq0  7401  renegcl  7436  negf1o  7553  mul2neg  7569  submul2  7570  ltaddneg  7595  ltleadd  7617  ltaddpos  7623  lt2sub  7631  le2sub  7632  lenegcon2  7638  recexre  7745  apirr  7772  apsym  7773  apneg  7778  apti  7789  recextlem1  7808  recexap  7810  mulap0  7811  divvalap  7829  rec11ap  7865  divdivdivap  7868  divmul24ap  7871  divmuleqap  7872  divadddivap  7882  conjmulap  7884  letrp1  7993  ltdivmul  8021  lerec2  8034  ledivdiv  8035  lbinf  8093  suprubex  8096  suprlubex  8097  suprleubex  8099  negiso  8100  cju  8105  nn1suc  8125  nn2ge  8138  nnsub  8144  nndiv  8146  halfaddsub  8332  nn0addcl  8390  nn0mulcl  8391  elnn0nn  8397  nn0ge2m1nn  8415  znegcl  8463  zaddcllempos  8469  zaddcllemneg  8471  zaddcl  8472  ztri3or  8475  zltnle  8478  nzadd  8484  zltp1le  8486  zltlem1  8489  elz2  8500  zdceq  8504  zdclt  8506  zdivadd  8517  gtndiv  8523  suprzclex  8526  prime  8527  zneo  8529  zeo  8533  peano2uz2  8535  uzind  8539  fzind  8543  eluzuzle  8708  uztrn  8716  eluzp1l  8724  peano2uzr  8754  uzaddcl  8755  indstr  8762  infrenegsupex  8763  supinfneg  8764  infsupneg  8765  supminfex  8766  indstr2  8777  ublbneg  8779  divfnzn  8787  qmulz  8789  qaddcl  8801  qnegcl  8802  qapne  8805  qreccl  8808  irradd  8812  irrmul  8813  divlt1lt  8882  divle1le  8883  ledivge1le  8884  nnledivrp  8918  nn0ledivnn  8919  addlelt  8920  xrltnsym  8944  xrlttr  8946  xrltso  8947  xrlttri3  8948  xrre  8963  xrre2  8964  xrre3  8965  xltnegi  8978  ixxss1  9003  ixxss2  9004  ixxss12  9005  ubioog  9013  iccss2  9043  iccssioo2  9045  iccssico2  9046  iccshftr  9092  iccshftl  9094  iccdil  9096  icccntr  9098  divelunit  9100  lincmb01cmp  9101  iccf1o  9102  zltaddlt1le  9104  fztri3or  9134  uzsubsubfz  9142  fzsplit2  9145  fzdisj  9147  fzaddel  9153  fzsubel  9154  fzss1  9157  fzss2  9158  fznatpl1  9169  fzdifsuc  9174  fzrev  9177  fzrev2  9178  fzrev2i  9179  fzrev3  9180  elfzm11  9184  uzsplit  9185  fzm1  9193  fzneuz  9194  elfz2nn0  9205  elfz0fzfz0  9214  fz0fzelfz0  9215  uzsubfz0  9217  fz0fzdiffz0  9218  elfzmlbp  9220  difelfzle  9222  difelfznle  9223  1fv  9226  fzon  9252  fzoss1  9257  fzouzdisj  9266  fzo1fzo0n0  9269  elfzo0z  9270  fzofzim  9274  fzoaddel2  9279  fzosubel2  9281  eluzgtdifelfzo  9283  elfzodifsumelfzo  9287  zpnn0elfzo1  9294  fzosplitsnm1  9295  elfzom1p1elfzo  9300  ssfzo12bi  9311  ubmelm1fzo  9312  fzofzp1b  9314  elfzom1b  9315  elfzomelpfzo  9317  peano2fzor  9318  fzoshftral  9324  exfzdc  9326  fvinim0ffz  9327  subfzo0  9328  qtri3or  9329  qltnle  9332  qdceq  9333  exbtwnzlemshrink  9335  rebtwn2zlemshrink  9340  qbtwnxr  9344  qavgle  9345  flqlt  9365  flqmulnn0  9381  flqeqceilz  9400  intfracq  9402  flqdiv  9403  zmod1congr  9423  zmodcl  9426  zmodfz  9428  zmodfzo  9429  zmodid2  9434  zmodidfzo  9435  mulp1mod1  9447  modqmuladd  9448  modqmuladdnn0  9450  modqm1p1mod0  9457  modifeq2int  9468  modaddmodup  9469  modaddmodlo  9470  modfzo0difsn  9477  modsumfzodifsn  9478  frec2uzuzd  9484  frec2uzltd  9485  frec2uzlt2d  9486  frecuzrdgrrn  9490  frec2uzrdg  9491  frecuzrdgrcl  9492  frecuzrdgtcl  9494  frecuzrdgsuc  9496  frecuzrdgrclt  9497  frecuzrdgg  9498  frecuzrdgfunlem  9501  frecuzrdgsuctlem  9505  fzofig  9514  nn0ennn  9515  iseqvalt  9532  iseqfveq2  9544  iseqfeq2  9545  iseqshft2  9548  iserf  9549  iserfre  9550  monoord2  9552  isermono  9553  iseqsplit  9554  iseqcaopr3  9556  iseqcaopr2  9557  iseradd  9559  isersub  9560  iseqid3s  9562  iseqid2  9564  iser0  9568  iser0f  9569  serige0  9570  serile  9571  expivallem  9574  expival  9575  expinnval  9576  exp1  9579  expp1  9580  expnegap0  9581  expm1t  9601  expap0  9603  expadd  9615  expsubap  9621  leexp1a  9628  subsq  9678  subsq2  9679  binom2sub  9684  bernneq  9690  bernneq3  9692  expnlbnd  9694  facnn  9751  fac0  9752  fac1  9753  facp1  9754  facnn2  9758  faccl  9759  facdiv  9762  facwordi  9764  faclbnd  9765  faclbnd3  9767  faclbnd6  9768  facavg  9770  bcval  9773  bcval4  9776  bccmpl  9778  ibcval5  9787  bcn2  9788  bccl  9791  sizeinfuni  9801  sizeennnuni  9803  sizefiv01gt1  9806  focdmex  9811  sizeeqf1oi  9812  sizef1rn  9813  filtinf  9816  sizenncl  9820  sizeunsng  9831  sizeprg  9832  shftfib  9849  shftfn  9850  shftval3  9853  crre  9882  rereb  9888  mulreap  9889  readd  9894  resub  9895  remullem  9896  imadd  9902  imsub  9903  cjadd  9909  ipcnval  9911  cjsub  9917  caucvgrelemcau  10004  cvg1nlemcau  10008  rexuz3  10014  recvguniq  10019  sqrt0  10028  resqrexlemfp1  10033  resqrexlemover  10034  resqrexlemcalc3  10040  resqrexlemcvg  10043  resqrexlemgt0  10044  resqrexlemga  10047  sqrtmul  10059  sqrtdiv  10066  sqabsadd  10079  sqabssub  10080  absexp  10103  abs2dif2  10131  fzomaxdiflem  10136  cau3lem  10138  qdenre  10226  maxleim  10229  maxabs  10233  maxleast  10237  rexanre  10244  fimaxre2  10247  negfi  10248  minmax  10250  climconst  10267  2clim  10278  climshftlemg  10279  climres  10280  climshft2  10283  addcn2  10287  subcn2  10288  mulcn2  10289  climcn1lem  10295  climadd  10302  climmul  10303  climsub  10304  clim2iser  10313  clim2iser2  10314  iisermulc2  10316  iserile  10318  climserile  10321  climcau  10322  climcvg1nlem  10324  climcaucn  10326  serif0  10327  isumrblem  10337  fisumcvg  10338  dvdsval2  10343  dvdsval3  10344  nndivdvds  10346  nndivides  10347  dvds0lem  10350  negdvdsb  10356  dvdsnegb  10357  dvdsabsb  10359  zdvdsdc  10361  modmulconst  10372  dvds2ln  10373  dvds2add  10374  dvds2sub  10375  dvdstr  10377  dvdsadd2b  10387  dvdsabseq  10392  divconjdvds  10394  dvdsssfz1  10397  alzdvds  10399  fzm1ndvds  10401  fzocongeq  10403  dvdsfac  10405  odd2np1lem  10416  odd2np1  10417  even2n  10418  mod2eq1n2dvds  10423  oddge22np1  10425  evennn02n  10426  evennn2n  10427  2tp1odd  10428  mulsucdiv2z  10429  2teven  10431  ltoddhalfle  10437  halfleoddlt  10438  opeo  10441  omeo  10442  m1expo  10444  nn0o1gt2  10449  nn0ob  10452  divalglemnn  10462  divalg2  10470  divalgmod  10471  modremain  10473  flodddiv4  10478  flodddiv4lt  10480  gcdmndc  10484  zsupcl  10487  zssinfcl  10488  infssuzex  10489  infssuzledc  10490  infssuzcldc  10491  dvdsbnd  10492  gcddvds  10499  dvdslegcd  10500  gcdcl  10502  gcd0id  10514  gcdneg  10517  gcdaddm  10519  modgcd  10526  bezoutlemzz  10535  bezoutlemaz  10536  bezoutlembz  10537  bezoutlemsup  10542  dfgcd3  10543  dfgcd2  10547  dvdsmulgcd  10558  sqgcd  10562  dvdssq  10564  nn0seqcvgd  10567  ialgrlem1st  10568  algcvgblem  10575  ialgcvga  10577  ialgfx  10578  eucalgf  10581  eucalginv  10582  lcmmndc  10588  lcmval  10589  lcmcllem  10593  lcmledvds  10596  lcmneg  10600  lcmgcdlem  10603  lcmgcd  10604  lcmdvds  10605  lcmid  10606  lcmass  10611  coprmgcdb  10614  qredeq  10622  qredeu  10623  divgcdcoprm0  10627  divgcdcoprmex  10628  cncongr1  10629  cncongr2  10630  isprm3  10644  prmind2  10646  nprm  10649  dvdsnprmd  10651  sqnprm  10661  exprmfct  10663  prmdvdsfz  10664  divgcdodd  10666  prmdvdsexp  10671  prmdvdsexpr  10673  prmfac1  10675  rpexp  10676  pw2dvdslemn  10687  oddpwdc  10696  sqne2sq  10699  xpct  10707  znnen  10709  cbvrald  10749  bdsepnft  10836  bj-om  10890  bj-nnen2lp  10907  strcollnft  10937  sscoll2  10941
  Copyright terms: Public domain W3C validator