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	⊢ (𝜑 → 𝜓)

Assertion

Ref	Expression
adantl	⊢ ((𝜒 ∧ 𝜑) → 𝜓)

Proof of Theorem adantl

Step	Hyp	Ref	Expression
1		adantl.1	. . 3 ⊢ (𝜑 → 𝜓)
2	1	adantr 270	. 2 ⊢ ((𝜑 ∧ 𝜒) → 𝜓)
3	2	ancoms 264	1 ⊢ ((𝜒 ∧ 𝜑) → 𝜓)

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  449  ad2antrl  473  ad2antll  474  im2anan9  562  bi2bian9  572  jaao  671  ordi  762  con1bidc  801  con1bdc  805  dfandc  811  stabtestimpdc  857  dcor  876  annimdc  878  orandc  880  ccase2  907  rnlem  917  simpr1  944  simpr2  945  simpr3  946  3ad2ant3  961  simprl1  983  simprl2  984  simprl3  985  simprr1  986  simprr2  987  simprr3  988  simpr1l  995  simpr1r  996  simpr2l  997  simpr2r  998  simpr3l  999  simpr3r  1000  simpr11  1022  simpr12  1023  simpr13  1024  simpr21  1025  simpr22  1026  simpr23  1027  simpr31  1028  simpr32  1029  simpr33  1030  falimd  1299  xorbin  1315  xor2dc  1321  biassdc  1326  dfbi3dc  1328  xordidc  1330  ax11v2  1741  ax11b  1747  equs5or  1751  nfsbxyt  1860  sbcomxyyz  1887  2exeu  2033  dimatis  2058  gencbvex  2645  gencbval  2647  rspcdva  2707  elrab3t  2748  euind  2779  reu6  2781  reuind  2795  sbcan  2856  sbcralt  2890  sbcrext  2891  csbcomg  2929  csbiebt  2942  sbcnestgf  2953  sseq1  3020  ddifnel  3103  elin  3155  undif3ss  3225  uneqdifeqim  3328  ifcldadc  3378  ifeq1dadc  3379  ifcldcd  3381  disjpr2  3456  diftpsn3  3527  preqr1g  3558  nfopd  3587  unissel  3630  trel  3882  iinexgm  3929  copsex2t  4000  sowlin  4075  efrirr  4108  ordelon  4138  alxfr  4211  ralxfr  4216  rexxfr  4218  rabxfr  4220  reuhyp  4222  ordelsuc  4249  onsucelsucr  4252  onsucsssucr  4253  onintonm  4261  ordtriexmidlem  4263  ordtri2or2exmidlem  4269  onsucelsucexmidlem  4272  ordsucunielexmid  4274  regexmidlem1  4276  reg2exmidlema  4277  preleq  4298  eunex  4304  ordsuc  4306  nlimsucg  4309  onnmin  4311  wessep  4320  tfi  4323  peano2  4336  posng  4430  sosng  4431  eqrelrdv2  4457  ideqg  4505  opeldmg  4558  relssres  4666  exse2  4719  brcodir  4732  xpidtr  4735  poltletr  4745  ssxpbm  4776  ssxp1  4777  ssxp2  4778  xpexr2m  4782  rnpropg  4820  elxp4  4828  elxp5  4829  dfco2a  4841  iota5  4907  iota2  4913  funssres  4962  funun  4964  fnsng  4967  fununi  4987  funimaexglem  5002  fneu  5023  fco  5076  fco2  5077  funssxp  5080  fssres2  5087  f1orescnv  5162  nffvd  5207  fnsnfv  5253  ssimaex  5255  funfvdm2  5258  dmfco  5262  fvco2  5263  fvmptss2  5268  respreima  5316  rexrn  5325  ralrn  5326  elrnrexdm  5327  ralrnmpt  5330  rexrnmpt  5331  ffvresb  5349  fcompt  5354  xpsng  5359  fprg  5367  fsnunres  5385  resfunexg  5403  funfvima3  5413  rexima  5415  ralima  5416  f1veqaeq  5429  f1ocnvfv1  5437  f1ocnvfv2  5438  fcofo  5444  foeqcnvco  5450  f1eqcocnv  5451  isoresbr  5469  isoini  5477  isoselem  5479  f1oiso  5485  riotabiia  5505  riota2f  5509  riota5f  5512  eloprabga  5611  ovmpt2x  5649  ovmpt2ga  5650  ovg  5659  oprssov  5662  caovcl  5675  caovimo  5714  f1opw2  5726  ofres  5745  resfunexgALT  5757  cofunexg  5758  iunexg  5766  offval3  5781  f2ndres  5807  elxp6  5816  releldm2  5831  oprabco  5858  1stconst  5862  2ndconst  5863  cnvf1o  5866  fo2ndf  5868  f1o2ndf1  5869  poxp  5873  cnvoprab  5875  mpt2xopoveq  5878  sprmpt2  5880  isprmpt2  5881  reldmtpos  5891  dftpos4  5901  tposf2  5906  iunon  5922  iordsmo  5935  tfrlem1  5946  tfrlemisucaccv  5962  tfrlemi1  5969  tfrexlem  5971  tfri3  5976  rdgivallem  5991  rdgon  5996  freccl  6016  oasuc  6067  omsuc  6074  nnaass  6087  nndi  6088  nnsucelsuc  6093  nntri1  6097  nntri3  6098  nntri2or2  6099  nnsseleq  6102  nndifsnid  6103  nnaordi  6104  nnaword  6107  nnmord  6113  nnm00  6125  swoer  6157  eqer  6161  0er  6163  relelec  6169  ectocl  6196  iinerm  6201  eroveu  6220  ecopovtrn  6226  ecopover  6227  ecopovsymg  6228  ecopovtrng  6229  ecopoverg  6230  th3qlem1  6231  ecovass  6238  ecoviass  6239  ecovdi  6240  ecovidi  6241  ener  6282  fundmen  6309  cnven  6311  xpcomco  6323  xpdom2  6328  fopwdom  6333  phplem4  6341  phplem4dom  6348  nndomo  6350  phplem4on  6353  fidceq  6354  fidifsnen  6355  fidifsnid  6356  infiexmid  6362  dif1en  6364  fin0  6369  fin0or  6370  findcard2  6373  findcard2s  6374  diffisn  6377  ac6sfi  6379  en2eqpr  6380  onunsnss  6383  unsnfidcex  6385  unsnfidcel  6386  snon0  6387  relcnvfi  6391  eqsupti  6409  supsnti  6418  cnvti  6432  ordiso2  6446  cardcl  6450  isnumi  6451  carden2bex  6458  ltpiord  6509  ltsopi  6510  mulclpi  6518  addasspig  6520  mulasspig  6522  distrpig  6523  addnidpig  6526  ltapig  6528  ltmpig  6529  indpi  6532  nnppipi  6533  enqdc1  6552  addcmpblnq  6557  mulcmpblnq  6558  ordpipqqs  6564  addassnqg  6572  mulcanenq  6575  distrnqg  6577  mulidnq  6579  recmulnqg  6581  ltsonq  6588  ltanqg  6590  ltmnqg  6591  ltaddnq  6597  ltexnqq  6598  halfnqq  6600  ltbtwnnqq  6605  archnqq  6607  prarloclemarch  6608  prarloclemarch2  6609  ltrnqg  6610  enq0tr  6624  enq0er  6625  nqnq0  6631  addcmpblnq0  6633  mulcmpblnq0  6634  mulcanenq0ec  6635  nnnq0lem1  6636  mulnnnq0  6640  nqnq0a  6644  nqnq0m  6645  nq0m0r  6646  nq0a0  6647  distrnq0  6649  addassnq0  6652  nq02m  6655  prcdnql  6674  prcunqu  6675  prubl  6676  prloc  6681  prarloclemlt  6683  prarloclemlo  6684  prarloc  6693  genplt2i  6700  genprndl  6711  genprndu  6712  genpdisj  6713  genpassl  6714  genpassu  6715  addnqprllem  6717  addnqprulem  6718  addnqprl  6719  addnqpru  6720  addlocprlemeqgt  6722  nqprloc  6735  nqprl  6741  nqpru  6742  addnqprlemrl  6747  addnqprlemru  6748  appdivnq  6753  prmuloc  6756  mulnqprl  6758  mulnqpru  6759  mullocprlem  6760  mulnqprlemrl  6763  mulnqprlemru  6764  distrlem4prl  6774  distrlem4pru  6775  1idprl  6780  1idpru  6781  ltpopr  6785  ltsopr  6786  ltaddpr  6787  ltexprlemupu  6794  ltexprlemdisj  6796  ltexprlemloc  6797  ltexprlemfl  6799  ltexprlemrl  6800  ltexprlemfu  6801  ltexprlemru  6802  addcanprleml  6804  ltaprg  6809  prplnqu  6810  addextpr  6811  recexprlemdisj  6820  recexprlemloc  6821  recexprlem1ssl  6823  recexprlem1ssu  6824  aptiprleml  6829  aptiprlemu  6830  caucvgprlemcanl  6834  cauappcvgprlemm  6835  cauappcvgprlemopl  6836  cauappcvgprlemlol  6837  cauappcvgprlemopu  6838  cauappcvgprlemdisj  6841  cauappcvgprlemloc  6842  cauappcvgprlemladdfu  6844  cauappcvgprlemladdfl  6845  cauappcvgprlemladdru  6846  cauappcvgprlemladdrl  6847  cauappcvgprlem1  6849  archrecpr  6854  caucvgprlemnkj  6856  caucvgprlemnbj  6857  caucvgprlemopl  6859  caucvgprlemlol  6860  caucvgprlemopu  6861  caucvgprlemdisj  6864  caucvgprlemloc  6865  caucvgprlemladdfu  6867  caucvgprlemladdrl  6868  caucvgprlemlim  6871  caucvgprprlemval  6878  caucvgprprlemnkltj  6879  caucvgprprlemnkeqj  6880  caucvgprprlemnbj  6883  caucvgprprlemmu  6885  caucvgprprlemopl  6887  caucvgprprlemlol  6888  caucvgprprlemopu  6889  caucvgprprlemdisj  6892  caucvgprprlemloc  6893  caucvgprprlemexbt  6896  caucvgprprlemexb  6897  caucvgprprlemaddq  6898  caucvgprprlemlim  6901  mulcmpblnrlemg  6917  ltsrprg  6924  mulasssrg  6935  distrsrg  6936  lttrsr  6939  ltposr  6940  ltsosr  6941  0idsr  6944  1idsr  6945  ltasrg  6947  recexgt0sr  6950  mulgt0sr  6954  mulextsr1lem  6956  archsr  6958  srpospr  6959  prsradd  6962  prsrlt  6963  caucvgsrlemfv  6967  caucvgsrlemoffval  6972  caucvgsrlemoffcau  6974  caucvgsrlemoffgt1  6975  caucvgsrlemoffres  6976  caucvgsr  6978  ltrennb  7022  axmulass  7039  axdistr  7040  ax0id  7044  axcnre  7047  axcaucvglemval  7063  axcaucvglemcau  7064  axcaucvglemres  7065  ltxrlt  7178  ltso  7189  muladd11  7241  readdcan  7248  cnegexlem1  7283  cnegexlem3  7285  cnegex  7286  addsubeq4  7323  subeq0  7334  renegcl  7369  negf1o  7486  mul2neg  7502  submul2  7503  ltaddneg  7528  ltleadd  7550  ltaddpos  7556  lt2sub  7564  le2sub  7565  lenegcon2  7571  recexre  7678  apirr  7705  apsym  7706  apneg  7711  apti  7722  recextlem1  7741  recexap  7743  mulap0  7744  divvalap  7762  rec11ap  7798  divdivdivap  7801  divmul24ap  7804  divmuleqap  7805  divadddivap  7815  conjmulap  7817  letrp1  7926  ltdivmul  7954  lerec2  7967  ledivdiv  7968  lbinf  8026  suprubex  8029  suprlubex  8030  suprleubex  8032  negiso  8033  cju  8038  nn1suc  8058  nn2ge  8071  nnsub  8077  nndiv  8079  halfaddsub  8265  nn0addcl  8323  nn0mulcl  8324  elnn0nn  8330  nn0ge2m1nn  8348  znegcl  8382  zaddcllempos  8388  zaddcllemneg  8390  zaddcl  8391  ztri3or  8394  zltnle  8397  nzadd  8403  zltp1le  8405  zltlem1  8408  elz2  8419  zdceq  8423  zdclt  8425  zdivadd  8436  gtndiv  8442  suprzclex  8445  prime  8446  zneo  8448  zeo  8452  peano2uz2  8454  uzind  8458  fzind  8462  eluzuzle  8627  uztrn  8635  eluzp1l  8643  peano2uzr  8673  uzaddcl  8674  indstr  8681  infrenegsupex  8682  supinfneg  8683  infsupneg  8684  supminfex  8685  indstr2  8696  ublbneg  8698  divfnzn  8706  qmulz  8708  qaddcl  8720  qnegcl  8721  qapne  8724  qreccl  8727  irradd  8731  irrmul  8732  divlt1lt  8801  divle1le  8802  ledivge1le  8803  nnledivrp  8837  nn0ledivnn  8838  addlelt  8839  xrltnsym  8868  xrlttr  8870  xrltso  8871  xrlttri3  8872  xrre  8887  xrre2  8888  xrre3  8889  xltnegi  8902  ixxss1  8927  ixxss2  8928  ixxss12  8929  ubioog  8937  iccss2  8967  iccssioo2  8969  iccssico2  8970  iccshftr  9016  iccshftl  9018  iccdil  9020  icccntr  9022  divelunit  9024  lincmb01cmp  9025  iccf1o  9026  zltaddlt1le  9028  fztri3or  9058  uzsubsubfz  9066  fzsplit2  9069  fzdisj  9071  fzaddel  9077  fzsubel  9078  fzss1  9081  fzss2  9082  fznatpl1  9093  fzdifsuc  9098  fzrev  9101  fzrev2  9102  fzrev2i  9103  fzrev3  9104  elfzm11  9108  uzsplit  9109  fzm1  9117  fzneuz  9118  elfz2nn0  9128  elfz0fzfz0  9137  fz0fzelfz0  9138  uzsubfz0  9140  fz0fzdiffz0  9141  elfzmlbp  9143  difelfzle  9145  difelfznle  9146  1fv  9149  fzon  9175  fzoss1  9180  fzouzdisj  9189  fzo1fzo0n0  9192  elfzo0z  9193  fzofzim  9197  fzoaddel2  9202  fzosubel2  9204  eluzgtdifelfzo  9206  elfzodifsumelfzo  9210  zpnn0elfzo1  9217  fzosplitsnm1  9218  elfzom1p1elfzo  9223  ssfzo12bi  9234  ubmelm1fzo  9235  fzofzp1b  9237  elfzom1b  9238  elfzomelpfzo  9240  peano2fzor  9241  fzoshftral  9247  exfzdc  9249  fvinim0ffz  9250  subfzo0  9251  qtri3or  9252  qltnle  9255  qdceq  9256  qbtwnzlemshrink  9258  rebtwn2zlemshrink  9262  qbtwnxr  9266  qavgle  9267  flqlt  9285  flqmulnn0  9301  flqeqceilz  9320  intfracq  9322  flqdiv  9323  zmod1congr  9343  zmodcl  9346  zmodfz  9348  zmodfzo  9349  zmodid2  9354  zmodidfzo  9355  mulp1mod1  9367  modqmuladd  9368  modqmuladdnn0  9370  modqm1p1mod0  9377  modifeq2int  9388  modaddmodup  9389  modaddmodlo  9390  modfzo0difsn  9397  modsumfzodifsn  9398  frec2uzzd  9402  frec2uzuzd  9404  frec2uzltd  9405  frec2uzlt2d  9406  frecuzrdgrrn  9410  frecuzrdgfn  9414  frecuzrdgsuc  9417  fzofig  9424  nn0ennn  9425  iseqfveq2  9448  iseqfeq2  9449  iseqshft2  9452  iserf  9453  iserfre  9454  monoord2  9456  isermono  9457  iseqsplit  9458  iseqcaopr3  9460  iseqcaopr2  9461  iseradd  9463  isersub  9464  iseqid3s  9466  iser0  9471  iser0f  9472  serige0  9473  serile  9474  expivallem  9477  expival  9478  expinnval  9479  exp1  9482  expp1  9483  expnegap0  9484  expm1t  9504  expap0  9506  expadd  9518  expsubap  9524  leexp1a  9531  subsq  9581  subsq2  9582  binom2sub  9587  bernneq  9593  bernneq3  9595  expnlbnd  9597  facnn  9654  fac0  9655  fac1  9656  facp1  9657  facnn2  9661  faccl  9662  facdiv  9665  facwordi  9667  faclbnd  9668  faclbnd3  9670  faclbnd6  9671  facavg  9673  bcval  9676  bcval4  9679  bccmpl  9681  ibcval5  9690  bcn2  9691  bccl  9694  shftfib  9711  shftfn  9712  shftval3  9715  crre  9744  rereb  9750  mulreap  9751  readd  9756  resub  9757  remullem  9758  imadd  9764  imsub  9765  cjadd  9771  ipcnval  9773  cjsub  9779  caucvgrelemcau  9866  cvg1nlemcau  9870  rexuz3  9876  recvguniq  9881  sqrt0  9890  resqrexlemfp1  9895  resqrexlemover  9896  resqrexlemcalc3  9902  resqrexlemcvg  9905  resqrexlemgt0  9906  resqrexlemga  9909  sqrtmul  9921  sqrtdiv  9928  sqabsadd  9941  sqabssub  9942  absexp  9965  abs2dif2  9993  fzomaxdiflem  9998  cau3lem  10000  qdenre  10088  maxleim  10091  maxabs  10095  maxleast  10099  rexanre  10106  fimaxre2  10109  negfi  10110  minmax  10112  climconst  10129  2clim  10140  climshftlemg  10141  climres  10142  climshft2  10145  addcn2  10149  subcn2  10150  mulcn2  10151  climcn1lem  10157  climadd  10164  climmul  10165  climsub  10166  clim2iser  10175  clim2iser2  10176  iisermulc2  10178  iserile  10180  climserile  10183  climcau  10184  climcvg1nlem  10186  climcaucn  10188  serif0  10189  dvdsval2  10198  dvdsval3  10199  nndivdvds  10201  nndivides  10202  dvds0lem  10205  negdvdsb  10211  dvdsnegb  10212  dvdsabsb  10214  zdvdsdc  10216  modmulconst  10227  dvds2ln  10228  dvds2add  10229  dvds2sub  10230  dvdstr  10232  dvdsadd2b  10242  dvdsabseq  10247  divconjdvds  10249  dvdsssfz1  10252  alzdvds  10254  fzm1ndvds  10256  fzocongeq  10258  dvdsfac  10260  odd2np1lem  10271  odd2np1  10272  even2n  10273  mod2eq1n2dvds  10279  oddge22np1  10281  evennn02n  10282  evennn2n  10283  2tp1odd  10284  mulsucdiv2z  10285  2teven  10287  ltoddhalfle  10293  halfleoddlt  10294  opeo  10297  omeo  10298  m1expo  10300  nn0o1gt2  10305  nn0ob  10308  divalglemnn  10318  divalg2  10326  divalgmod  10327  modremain  10329  flodddiv4  10334  flodddiv4lt  10336  gcdmndc  10340  zsupcl  10343  zssinfcl  10344  infssuzex  10345  infssuzledc  10346  infssuzcldc  10347  dvdsbnd  10348  gcddvds  10355  dvdslegcd  10356  gcdcl  10358  gcd0id  10370  gcdneg  10373  gcdaddm  10375  modgcd  10382  bezoutlemzz  10391  bezoutlemaz  10392  bezoutlembz  10393  bezoutlemsup  10398  dfgcd3  10399  dfgcd2  10403  dvdsmulgcd  10414  sqgcd  10418  dvdssq  10420  nn0seqcvgd  10423  ialgrlem1st  10424  algcvgblem  10431  ialgcvga  10433  ialgfx  10434  eucalgf  10437  eucalginv  10438  lcmmndc  10444  lcmval  10445  lcmcllem  10449  lcmledvds  10452  lcmneg  10456  lcmgcdlem  10459  lcmgcd  10460  lcmdvds  10461  lcmid  10462  lcmass  10467  coprmgcdb  10470  qredeq  10478  qredeu  10479  divgcdcoprm0  10483  divgcdcoprmex  10484  cncongr1  10485  cncongr2  10486  isprm3  10500  prmind2  10502  nprm  10505  dvdsnprmd  10507  sqnprm  10517  exprmfct  10519  prmdvdsfz  10520  divgcdodd  10522  prmdvdsexp  10527  prmdvdsexpr  10529  prmfac1  10531  rpexp  10532  pw2dvdslemn  10543  oddpwdc  10552  sqne2sq  10555  cbvrald  10598  bdsepnft  10678  bj-om  10732  bj-nnen2lp  10749  strcollnft  10779  sscoll2  10783