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

Step	Hyp	Ref	Expression
1		adantl.1	. . 3 |- ( ph -> ps )
2	1	adantr 270	. 2 |- ( ( ph /\ ch ) -> ps )
3	2	ancoms 264	1 |- ( ( ch /\ ph ) -> ps )

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  804  con1bdc  808  dfandc  814  stabtestimpdc  860  dcor  879  annimdc  881  orandc  883  ccase2  910  rnlem  920  simpr1  947  simpr2  948  simpr3  949  3ad2ant3  964  simprl1  986  simprl2  987  simprl3  988  simprr1  989  simprr2  990  simprr3  991  simpr1l  998  simpr1r  999  simpr2l  1000  simpr2r  1001  simpr3l  1002  simpr3r  1003  simpr11  1025  simpr12  1026  simpr13  1027  simpr21  1028  simpr22  1029  simpr23  1030  simpr31  1031  simpr32  1032  simpr33  1033  falimd  1302  xorbin  1318  xor2dc  1324  biassdc  1329  dfbi3dc  1331  xordidc  1333  ax11v2  1745  ax11b  1751  equs5or  1755  nfsbxyt  1864  sbcomxyyz  1891  2exeu  2037  dimatis  2062  gencbvex  2659  gencbval  2661  elrab3t  2761  euind  2793  reu6  2795  reuind  2809  sbcan  2870  sbcralt  2904  sbcrext  2905  csbcomg  2943  csbiebt  2956  sbcnestgf  2968  sseq1  3036  ddifnel  3120  elin  3172  undif3ss  3249  uneqdifeqim  3355  ifcldadc  3406  ifeq1dadc  3407  ifbothdadc  3408  ifcldcd  3412  disjpr2  3489  diftpsn3  3561  preqr1g  3593  nfopd  3622  unissel  3665  trel  3918  iinexgm  3965  exmidundif  4009  copsex2t  4046  sowlin  4121  efrirr  4154  ordelon  4184  alxfr  4257  ralxfr  4262  rexxfr  4264  rabxfr  4266  reuhyp  4268  ordelsuc  4295  onsucelsucr  4298  onsucsssucr  4299  onintonm  4307  ordtriexmidlem  4309  ordtri2or2exmidlem  4315  onsucelsucexmidlem  4318  ordsucunielexmid  4320  regexmidlem1  4322  reg2exmidlema  4323  preleq  4344  eunex  4350  ordsuc  4352  nlimsucg  4355  onnmin  4357  wessep  4366  tfi  4370  peano2  4383  posng  4478  sosng  4479  eqrelrdv2  4505  ideqg  4555  opeldmg  4609  relssres  4717  exse2  4773  brcodir  4786  xpidtr  4789  poltletr  4799  ssxpbm  4832  ssxp1  4833  ssxp2  4834  xpexr2m  4838  rnpropg  4876  elxp4  4884  elxp5  4885  dfco2a  4897  iota5  4966  iota2  4972  funssres  5021  funun  5023  fnsng  5026  fununi  5047  funimaexglem  5062  fneu  5083  fco  5140  fco2  5141  funssxp  5144  fssres2  5151  f0rn0  5168  f1orescnv  5232  nffvd  5280  fnsnfv  5326  ssimaex  5328  funfvdm2  5331  dmfco  5335  fvco2  5336  fvmptss2  5342  respreima  5390  rexrn  5399  ralrn  5400  elrnrexdm  5401  ralrnmpt  5404  rexrnmpt  5405  ffvresb  5424  fcompt  5430  xpsng  5435  fprg  5443  fsnunres  5461  resfunexg  5479  funfvima3  5489  rexima  5495  ralima  5496  f1veqaeq  5509  f1ocnvfv1  5517  f1ocnvfv2  5518  fcofo  5524  foeqcnvco  5530  f1eqcocnv  5531  isoresbr  5549  isoini  5558  isoselem  5560  f1oiso  5566  riotabiia  5586  riota2f  5590  riota5f  5593  eloprabga  5692  ovmpt2x  5730  ovmpt2ga  5731  ovg  5740  oprssov  5743  caovcl  5756  caovimo  5795  f1opw2  5807  ofres  5826  resfunexgALT  5838  cofunexg  5839  iunexg  5847  offval3  5862  f2ndres  5888  elxp6  5897  releldm2  5912  oprabco  5939  1stconst  5943  2ndconst  5944  cnvf1o  5947  fo2ndf  5949  f1o2ndf1  5950  poxp  5954  cnvoprab  5956  mpt2xopoveq  5959  sprmpt2  5961  isprmpt2  5962  reldmtpos  5972  dftpos4  5982  tposf2  5987  iunon  6003  iordsmo  6016  tfrlem1  6027  tfrlemisucaccv  6044  tfrlemi1  6051  tfrexlem  6053  tfr1onlemsucaccv  6060  tfri1dALT  6070  tfrcllemsucaccv  6073  tfri3  6086  rdgivallem  6100  rdgon  6105  frecabcl  6118  freccllem  6121  frecfcllem  6123  frecsuclem  6125  oasuc  6179  oawordriexmid  6185  omsuc  6187  nnaass  6200  nndi  6201  nnsucelsuc  6206  nnsucuniel  6210  nntri1  6211  nntri3  6212  nntri2or2  6213  nnsseleq  6216  dcdifsnid  6217  nnaordi  6219  nnaword  6222  nnmord  6228  nnm00  6240  swoer  6272  eqer  6276  0er  6278  relelec  6284  ectocl  6311  iinerm  6316  eroveu  6335  ecopovtrn  6341  ecopover  6342  ecopovsymg  6343  ecopovtrng  6344  ecopoverg  6345  th3qlem1  6346  ecovass  6353  ecoviass  6354  ecovdi  6355  ecovidi  6356  pmss12g  6384  pmresg  6385  mapss  6400  fdiagfn  6401  ener  6448  fundmen  6475  cnven  6477  1domsn  6487  xpcomco  6494  xpdom2  6499  fopwdom  6504  dom0  6506  xpf1o  6512  mapen  6514  mapdom1g  6515  mapxpen  6516  xpmapenlem  6517  phplem4  6523  phplem4dom  6530  nndomo  6532  phplem4on  6535  fidceq  6537  fidifsnen  6538  infiexmid  6545  dif1en  6547  dif1enen  6548  fin0  6553  fin0or  6554  findcard2  6557  findcard2s  6558  diffisn  6561  infnfi  6563  ac6sfi  6566  infm  6572  en2eqpr  6575  onunsnss  6579  unsnfidcex  6582  unsnfidcel  6583  undifdcss  6585  xpfi  6590  fisseneq  6592  ssfirab  6593  snon0  6595  relcnvfi  6600  f1finf1o  6605  en1eqsn  6606  sbthlemi3  6612  sbthlemi6  6615  isbth  6620  eqsupti  6635  supsnti  6644  cnvti  6658  ordiso2  6672  djueq12  6676  djuf1olem  6689  djulclb  6691  djuun  6704  djuss  6705  1stinl  6709  2ndinl  6710  1stinr  6711  2ndinr  6712  updjudhf  6714  updjudhcoinlf  6715  updjudhcoinrg  6716  updjud  6717  enomnilem  6738  finomni  6740  exmidomniim  6741  exmidomni  6742  nnnninf  6750  cardcl  6753  isnumi  6754  carden2bex  6761  exmidfodomrlemim  6771  exmidfodomrlemr  6772  exmidfodomrlemrALT  6773  ltpiord  6822  ltsopi  6823  mulclpi  6831  addasspig  6833  mulasspig  6835  distrpig  6836  addnidpig  6839  ltapig  6841  ltmpig  6842  indpi  6845  nnppipi  6846  enqdc1  6865  addcmpblnq  6870  mulcmpblnq  6871  ordpipqqs  6877  addassnqg  6885  mulcanenq  6888  distrnqg  6890  mulidnq  6892  recmulnqg  6894  ltsonq  6901  ltanqg  6903  ltmnqg  6904  ltaddnq  6910  ltexnqq  6911  halfnqq  6913  ltbtwnnqq  6918  archnqq  6920  prarloclemarch  6921  prarloclemarch2  6922  ltrnqg  6923  enq0tr  6937  enq0er  6938  nqnq0  6944  addcmpblnq0  6946  mulcmpblnq0  6947  mulcanenq0ec  6948  nnnq0lem1  6949  mulnnnq0  6953  nqnq0a  6957  nqnq0m  6958  nq0m0r  6959  nq0a0  6960  distrnq0  6962  addassnq0  6965  nq02m  6968  prcdnql  6987  prcunqu  6988  prubl  6989  prloc  6994  prarloclemlt  6996  prarloclemlo  6997  prarloc  7006  genplt2i  7013  genprndl  7024  genprndu  7025  genpdisj  7026  genpassl  7027  genpassu  7028  addnqprllem  7030  addnqprulem  7031  addnqprl  7032  addnqpru  7033  addlocprlemeqgt  7035  nqprloc  7048  nqprl  7054  nqpru  7055  addnqprlemrl  7060  addnqprlemru  7061  appdivnq  7066  prmuloc  7069  mulnqprl  7071  mulnqpru  7072  mullocprlem  7073  mulnqprlemrl  7076  mulnqprlemru  7077  distrlem4prl  7087  distrlem4pru  7088  1idprl  7093  1idpru  7094  ltpopr  7098  ltsopr  7099  ltaddpr  7100  ltexprlemupu  7107  ltexprlemdisj  7109  ltexprlemloc  7110  ltexprlemfl  7112  ltexprlemrl  7113  ltexprlemfu  7114  ltexprlemru  7115  addcanprleml  7117  ltaprg  7122  prplnqu  7123  addextpr  7124  recexprlemdisj  7133  recexprlemloc  7134  recexprlem1ssl  7136  recexprlem1ssu  7137  aptiprleml  7142  aptiprlemu  7143  caucvgprlemcanl  7147  cauappcvgprlemm  7148  cauappcvgprlemopl  7149  cauappcvgprlemlol  7150  cauappcvgprlemopu  7151  cauappcvgprlemdisj  7154  cauappcvgprlemloc  7155  cauappcvgprlemladdfu  7157  cauappcvgprlemladdfl  7158  cauappcvgprlemladdru  7159  cauappcvgprlemladdrl  7160  cauappcvgprlem1  7162  archrecpr  7167  caucvgprlemnkj  7169  caucvgprlemnbj  7170  caucvgprlemopl  7172  caucvgprlemlol  7173  caucvgprlemopu  7174  caucvgprlemdisj  7177  caucvgprlemloc  7178  caucvgprlemladdfu  7180  caucvgprlemladdrl  7181  caucvgprlemlim  7184  caucvgprprlemval  7191  caucvgprprlemnkltj  7192  caucvgprprlemnkeqj  7193  caucvgprprlemnbj  7196  caucvgprprlemmu  7198  caucvgprprlemopl  7200  caucvgprprlemlol  7201  caucvgprprlemopu  7202  caucvgprprlemdisj  7205  caucvgprprlemloc  7206  caucvgprprlemexbt  7209  caucvgprprlemexb  7210  caucvgprprlemaddq  7211  caucvgprprlemlim  7214  mulcmpblnrlemg  7230  ltsrprg  7237  mulasssrg  7248  distrsrg  7249  lttrsr  7252  ltposr  7253  ltsosr  7254  0idsr  7257  1idsr  7258  ltasrg  7260  recexgt0sr  7263  mulgt0sr  7267  mulextsr1lem  7269  archsr  7271  srpospr  7272  prsradd  7275  prsrlt  7276  caucvgsrlemfv  7280  caucvgsrlemoffval  7285  caucvgsrlemoffcau  7287  caucvgsrlemoffgt1  7288  caucvgsrlemoffres  7289  caucvgsr  7291  ltrennb  7335  axmulass  7352  axdistr  7353  ax0id  7357  axcnre  7360  axcaucvglemval  7376  axcaucvglemcau  7377  axcaucvglemres  7378  ltxrlt  7496  ltso  7507  muladd11  7559  readdcan  7566  cnegexlem1  7601  cnegexlem3  7603  cnegex  7604  addsubeq4  7641  subeq0  7652  renegcl  7687  negf1o  7804  mul2neg  7820  submul2  7821  ltaddneg  7846  ltleadd  7868  ltaddpos  7874  lt2sub  7882  le2sub  7883  lenegcon2  7889  recexre  7996  apirr  8023  apsym  8024  apneg  8029  apti  8040  recextlem1  8059  recexap  8061  mulap0  8062  divvalap  8080  rec11ap  8116  divdivdivap  8119  divmul24ap  8122  divmuleqap  8123  divadddivap  8133  conjmulap  8135  letrp1  8244  ltdivmul  8272  lerec2  8285  ledivdiv  8286  lbinf  8344  suprubex  8347  suprlubex  8348  suprleubex  8350  negiso  8351  cju  8356  nn1suc  8376  nn2ge  8389  nnsub  8395  nndiv  8397  halfaddsub  8583  nn0addcl  8641  nn0mulcl  8642  elnn0nn  8648  nn0ge2m1nn  8666  znegcl  8714  zaddcllempos  8720  zaddcllemneg  8722  zaddcl  8723  ztri3or  8726  zltnle  8729  nzadd  8735  zltp1le  8737  zltlem1  8740  elz2  8751  zdceq  8755  zdclt  8757  zdivadd  8768  gtndiv  8774  suprzclex  8777  prime  8778  zneo  8780  zeo  8784  peano2uz2  8786  uzind  8790  fzind  8794  eluzuzle  8959  uztrn  8967  eluzp1l  8975  peano2uzr  9005  uzaddcl  9006  indstr  9013  infrenegsupex  9014  supinfneg  9015  infsupneg  9016  supminfex  9017  indstr2  9028  ublbneg  9030  divfnzn  9038  qmulz  9040  qaddcl  9052  qnegcl  9053  qapne  9056  qreccl  9059  irradd  9063  irrmul  9064  divlt1lt  9133  divle1le  9134  ledivge1le  9135  nnledivrp  9169  nn0ledivnn  9170  addlelt  9171  xrltnsym  9195  xrlttr  9197  xrltso  9198  xrlttri3  9199  xrre  9214  xrre2  9215  xrre3  9216  xltnegi  9229  ixxss1  9254  ixxss2  9255  ixxss12  9256  ubioog  9264  iccss2  9294  iccssioo2  9296  iccssico2  9297  iccshftr  9343  iccshftl  9345  iccdil  9347  icccntr  9349  divelunit  9351  lincmb01cmp  9352  iccf1o  9353  zltaddlt1le  9355  fztri3or  9385  uzsubsubfz  9393  fzsplit2  9396  fzdisj  9398  fzaddel  9404  fzsubel  9405  fzss1  9408  fzss2  9409  fznatpl1  9420  fzdifsuc  9425  fzrev  9428  fzrev2  9429  fzrev2i  9430  fzrev3  9431  elfzm11  9435  uzsplit  9436  fzm1  9444  fzneuz  9445  elfz2nn0  9456  elfz0fzfz0  9465  fz0fzelfz0  9466  uzsubfz0  9468  fz0fzdiffz0  9469  elfzmlbp  9471  difelfzle  9473  difelfznle  9474  1fv  9478  fzon  9505  fzoss1  9510  fzouzdisj  9519  fzo1fzo0n0  9522  elfzo0z  9523  fzofzim  9527  fzoaddel2  9532  fzosubel2  9534  eluzgtdifelfzo  9536  elfzodifsumelfzo  9540  zpnn0elfzo1  9547  fzosplitsnm1  9548  elfzom1p1elfzo  9553  ssfzo12bi  9564  ubmelm1fzo  9565  fzofzp1b  9567  elfzom1b  9568  elfzomelpfzo  9570  peano2fzor  9571  fzoshftral  9577  exfzdc  9579  fvinim0ffz  9580  subfzo0  9581  qtri3or  9582  qltnle  9585  qdceq  9586  exbtwnzlemshrink  9588  rebtwn2zlemshrink  9593  qbtwnxr  9597  qavgle  9598  flqlt  9618  flqmulnn0  9634  flqeqceilz  9653  intfracq  9655  flqdiv  9656  zmod1congr  9676  zmodcl  9679  zmodfz  9681  zmodfzo  9682  zmodid2  9687  zmodidfzo  9688  mulp1mod1  9700  modqmuladd  9701  modqmuladdnn0  9703  modqm1p1mod0  9710  modifeq2int  9721  modaddmodup  9722  modaddmodlo  9723  modfzo0difsn  9730  modsumfzodifsn  9731  frec2uzuzd  9737  frec2uzltd  9738  frec2uzlt2d  9739  frecuzrdgrrn  9743  frec2uzrdg  9744  frecuzrdgrcl  9745  frecuzrdgtcl  9747  frecuzrdgsuc  9749  frecuzrdgrclt  9750  frecuzrdgg  9751  frecuzrdgfunlem  9754  frecuzrdgsuctlem  9758  fzofig  9767  nn0ennn  9768  iseqvalt  9790  iseqfveq2  9802  iseqfeq2  9803  iseqshft2  9806  iserf  9807  iserfre  9808  monoord2  9810  isermono  9811  iseqsplit  9812  iseqcaopr3  9814  iseqcaopr2  9815  iseqf1olemqk  9827  iseqf1olemqsumkj  9831  iseqf1olemqsumk  9832  iseqf1olemqsum  9833  iseqf1olemstep  9834  iseqf1olemp  9835  iseqf1oleml  9836  iseqf1o  9837  iseradd  9838  isersub  9839  iseqid3s  9841  iseqid2  9843  iser0  9847  iser0f  9848  serige0  9850  serile  9851  expivallem  9854  expival  9855  expinnval  9856  exp1  9859  expp1  9860  expnegap0  9861  expm1t  9881  expap0  9883  expadd  9895  expsubap  9901  leexp1a  9908  subsq  9958  subsq2  9959  binom2sub  9964  bernneq  9970  bernneq3  9972  expnlbnd  9974  facnn  10031  fac0  10032  fac1  10033  facp1  10034  facnn2  10038  faccl  10039  facdiv  10042  facwordi  10044  faclbnd  10045  faclbnd3  10047  faclbnd6  10048  facavg  10050  bcval  10053  bcval4  10056  bccmpl  10058  ibcval5  10067  bcn2  10068  bccl  10071  hashinfuni  10081  hashennnuni  10083  hashfiv01gt1  10086  focdmex  10091  fihasheqf1oi  10092  fihashf1rn  10093  filtinf  10096  hashnncl  10100  hashunsng  10111  hashprg  10112  hashdifsn  10123  hashdifpr  10124  hashfzp1  10128  hashxp  10130  zfz1isolemiso  10140  zfz1isolem1  10141  zfz1iso  10142  iseqcoll  10143  shftfib  10153  shftfn  10154  shftval3  10157  crre  10186  rereb  10192  mulreap  10193  readd  10198  resub  10199  remullem  10200  imadd  10206  imsub  10207  cjadd  10213  ipcnval  10215  cjsub  10221  caucvgrelemcau  10308  cvg1nlemcau  10312  rexuz3  10318  recvguniq  10323  sqrt0  10332  resqrexlemfp1  10337  resqrexlemover  10338  resqrexlemcalc3  10344  resqrexlemcvg  10347  resqrexlemgt0  10348  resqrexlemga  10351  sqrtmul  10363  sqrtdiv  10370  sqabsadd  10383  sqabssub  10384  absexp  10407  abs2dif2  10435  fzomaxdiflem  10440  cau3lem  10442  qdenre  10530  maxleim  10533  maxabs  10537  maxleast  10541  rexanre  10548  fimaxre2  10551  negfi  10552  minmax  10554  climconst  10571  2clim  10582  climshftlemg  10583  climres  10584  climshft2  10587  addcn2  10591  subcn2  10592  mulcn2  10593  climcn1lem  10599  climadd  10606  climmul  10607  climsub  10608  clim2iser  10617  clim2iser2  10618  iisermulc2  10620  iserile  10622  climserile  10625  climcau  10626  climcvg1nlem  10628  climcaucn  10630  serif0  10631  isumrblem  10655  fisumcvg  10656  isummolem3  10659  isummolem2a  10660  zisum  10663  iisum  10664  fisum  10665  sum0  10666  isumz  10667  fisumss  10670  dvdsval2  10674  dvdsval3  10675  nndivdvds  10677  nndivides  10678  dvds0lem  10681  negdvdsb  10687  dvdsnegb  10688  dvdsabsb  10690  zdvdsdc  10692  modmulconst  10703  dvds2ln  10704  dvds2add  10705  dvds2sub  10706  dvdstr  10708  dvdsadd2b  10718  dvdsabseq  10723  divconjdvds  10725  dvdsssfz1  10728  alzdvds  10730  fzm1ndvds  10732  fzocongeq  10734  dvdsfac  10736  odd2np1lem  10747  odd2np1  10748  even2n  10749  mod2eq1n2dvds  10754  oddge22np1  10756  evennn02n  10757  evennn2n  10758  2tp1odd  10759  mulsucdiv2z  10760  2teven  10762  ltoddhalfle  10768  halfleoddlt  10769  opeo  10772  omeo  10773  m1expo  10775  nn0o1gt2  10780  nn0ob  10783  divalglemnn  10793  divalg2  10801  divalgmod  10802  modremain  10804  flodddiv4  10809  flodddiv4lt  10811  gcdmndc  10815  zsupcl  10818  zssinfcl  10819  infssuzex  10820  infssuzledc  10821  infssuzcldc  10822  dvdsbnd  10823  gcddvds  10830  dvdslegcd  10831  gcdcl  10833  gcd0id  10845  gcdneg  10848  gcdaddm  10850  modgcd  10857  bezoutlemzz  10866  bezoutlemaz  10867  bezoutlembz  10868  bezoutlemsup  10873  dfgcd3  10874  dfgcd2  10878  dvdsmulgcd  10889  sqgcd  10893  dvdssq  10895  nn0seqcvgd  10898  ialgrlem1st  10899  algcvgblem  10906  ialgcvga  10908  ialgfx  10909  eucalgf  10912  eucalginv  10913  lcmmndc  10919  lcmval  10920  lcmcllem  10924  lcmledvds  10927  lcmneg  10931  lcmgcdlem  10934  lcmgcd  10935  lcmdvds  10936  lcmid  10937  lcmass  10942  coprmgcdb  10945  qredeq  10953  qredeu  10954  divgcdcoprm0  10958  divgcdcoprmex  10959  cncongr1  10960  cncongr2  10961  isprm3  10975  prmind2  10977  nprm  10980  dvdsnprmd  10982  sqnprm  10992  exprmfct  10994  prmdvdsfz  10995  divgcdodd  10997  prmdvdsexp  11002  prmdvdsexpr  11004  prmfac1  11006  rpexp  11007  pw2dvdslemn  11018  oddpwdc  11027  sqne2sq  11030  divnumden  11049  divdenle  11050  nn0gcdsq  11053  zgcdsq  11054  qden1elz  11058  nn0sqrtelqelz  11059  phivalfi  11063  hashdvds  11072  phiprmpw  11073  crth  11075  phimullem  11076  hashgcdeq  11079  xpct  11084  znnen  11086  cbvrald  11126  bdsepnft  11216  bj-om  11270  bj-nnen2lp  11287  strcollnft  11317  sscoll2  11321  nnpredcl  11328  nnsf  11333  peano4nninf  11334  peano3nninf  11335  nninfalllem1  11337  nninfsellemdc  11340  nninfsellemsuc  11342  nninfsellemqall  11345  nninfsellemeqinf  11346  exmidsbthrlem  11350