Theorem ad2antlr 489

Description: Deduction adding two conjuncts to antecedent. (Contributed by NM, 19-Oct-1999.) (Proof shortened by Wolf Lammen, 20-Nov-2012.)

Hypothesis

Ref	Expression
ad2ant.1	|- ( ph -> ps )

Assertion

Ref	Expression
ad2antlr	|- ( ( ( ch /\ ph ) /\ th ) -> ps )

Proof of Theorem ad2antlr

Step	Hyp	Ref	Expression
1		ad2ant.1	. . 3 |- ( ph -> ps )
2	1	adantr 276	. 2 |- ( ( ph /\ th ) -> ps )
3	2	adantll 476	1 |- ( ( ( ch /\ ph ) /\ th ) -> ps )

Syntax hints:   -> wi 4   /\ wa 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem is referenced by:  ad3antlr  493  simplr  528  simplrl  535  simplrr  536  ordtri2or2exmidlem  4622  en2lp  4650  foun  5599  f1oprg  5625  fcof1o  5925  foeqcnvco  5926  f1eqcocnv  5927  caovord3  6191  f1o2ndf1  6388  smores2  6455  frecrdg  6569  nnaordex  6691  xpdom2  7010  xpen  7026  mapen  7027  xpmapenlem  7030  nndomo  7045  phpm  7047  fidifsnen  7052  isinfinf  7079  fidcen  7081  finexdc  7085  elssdc  7087  fientri3  7100  fiintim  7116  xpfi  7117  f1dmvrnfibi  7134  sbthlemi8  7154  djudom  7283  omp1eomlem  7284  difinfsn  7290  ctmlemr  7298  ctssdccl  7301  nnnninfeq  7318  enomnilem  7328  finomni  7330  ismkvnex  7345  enmkvlem  7351  nninfwlpoimlemginf  7366  exmidfodomrlemrALT  7404  exmidontriim  7430  netap  7463  exmidapne  7469  acnccim  7481  dfplpq2  7564  recclnq  7602  subhalfnqq  7624  distrnq0  7669  prarloclem3step  7706  genpml  7727  genpmu  7728  addnqprl  7739  addnqpru  7740  appdivnq  7773  mulnqprl  7778  mulnqpru  7779  mullocpr  7781  ltexprlemfl  7819  ltexprlemfu  7821  ltmprr  7852  archpr  7853  cauappcvgprlemm  7855  caucvgprlemladdrl  7888  caucvgprprlemopl  7907  caucvgprprlemopu  7909  recexgt0sr  7983  mulgt0sr  7988  elrealeu  8039  axcaucvglemcau  8108  axcaucvglemres  8109  cnegex  8347  apirr  8775  mulge0  8789  lemul12a  9032  lediv2a  9065  creur  9129  nndiv  9174  zaddcllemneg  9508  peano5uzti  9578  supinfneg  9819  infsupneg  9820  divfnzn  9845  xrltso  10021  xpncan  10096  xltadd1  10101  xleaddadd  10112  elioc2  10161  elico2  10162  elicc2  10163  exfzdc  10476  zsupcllemstep  10479  infssuzex  10483  suprzubdc  10486  exbtwnzlemex  10499  rebtwn2z  10504  modqid  10601  modqcyc  10611  mulqaddmodid  10616  modqadd2mod  10626  addmodlteq  10650  frecuzrdgg  10668  nninfinf  10695  seq3val  10712  seqvalcd  10713  seq3clss  10723  iseqf1olemqcl  10751  iseqf1olemnab  10753  seq3f1olemp  10767  seq3f1o  10769  seqf1oglem1  10771  seqfeq4g  10783  fser0const  10787  ser3ge0  10788  exp3vallem  10792  qsqeqor  10902  facndiv  10991  faclbnd  10993  bcval5  11015  hashen  11036  fihashdom  11056  hashunlem  11057  hashfacen  11090  zfz1isolemiso  11093  seq3coll  11096  ccatsymb  11169  ccatrn  11176  ccatw2s1p2  11213  swrdccatin1  11296  swrdccatin2  11300  swrdccat3b  11311  caucvgre  11532  resqrexlemlo  11564  cau3lem  11665  qdenre  11753  rexico  11772  fimaxre2  11778  2zinfmin  11794  xrmaxiflemcl  11796  xrmaxifle  11797  xrmaxiflemcom  11800  2clim  11852  cn1lem  11865  climsqz  11886  climsqz2  11887  climcau  11898  sumrbdclem  11928  summodclem2a  11932  fsum3  11938  fsumcl2lem  11949  fsumadd  11957  sumsnf  11960  fsum2dlemstep  11985  fisum0diag2  11998  fsummulc2  11999  mertenslemub  12085  mertenslemi1  12086  mertensabs  12088  ntrivcvgap  12099  prodrbdclem  12122  prodmodclem3  12126  prodmodclem2a  12127  prodmodc  12129  prod1dc  12137  prodsnf  12143  fprod2dlemstep  12173  efaddlem  12225  tanaddaplem  12289  zdvdsdc  12363  dvdseq  12399  dvdsext  12406  odd2np1  12424  sqoddm1div8z  12437  nno  12457  dfgcd3  12571  nninfctlemfo  12601  dvdslcm  12631  lcmneg  12636  lcmgcdlem  12639  ncoprmgcdne1b  12651  qredeq  12658  qredeu  12659  divgcdcoprm0  12663  exprmfct  12700  prmdvdsfz  12701  isprm5  12704  rpexp1i  12716  sqrt2irr  12724  nonsq  12769  eulerthlemrprm  12791  eulerthlema  12792  phisum  12803  modprmn0modprm0  12819  pclemdc  12851  pcz  12895  pcmpt  12906  fldivp1  12911  pcfac  12913  expnprm  12916  oddprmdvds  12917  prmpwdvds  12918  infpnlem1  12922  1arith  12930  4sqlem2  12952  4sqlemafi  12958  4sqleminfi  12960  4sqexercise2  12962  4sqlemsdc  12963  ctinfom  13039  enctlem  13043  nninfdclemlt  13062  setsfun  13107  setsfun0  13108  setscom  13112  gsumfzval  13464  mndissubm  13548  resmhm  13560  resmhm2  13561  mhmco  13563  gsumfzz  13568  gsumwsubmcl  13569  gsumwmhm  13571  dfgrp2  13600  isgrpinv  13627  mulgval  13699  mulgnnp1  13707  mulgz  13727  grpissubg  13771  resghm  13837  qusecsub  13908  isrng  13937  lmodfopne  14330  dflidl2rng  14485  gsumfzfsumlemm  14591  mulgrhm2  14614  znidomb  14662  znunit  14663  psrbaglesuppg  14676  psrbagfi  14677  tgdom  14786  ssrest  14896  cnfval  14908  cnpfval  14909  cnpval  14912  iscnp3  14917  ssidcn  14924  cnpnei  14933  cnntr  14939  cncnp  14944  cnptopresti  14952  tx1cn  14983  upxp  14986  imasnopn  15013  bdmet  15216  metcnp  15226  ivthinclemlr  15351  ivthinclemur  15353  ivthinc  15357  dvrecap  15427  dvmptfsum  15439  elply2  15449  plymullem1  15462  plycolemc  15472  plycjlemc  15474  dvply1  15479  pilem3  15497  relogeftb  15579  logbgcd1irr  15681  mpodvdsmulf1o  15704  mersenne  15711  lgslem4  15722  lgsval  15723  lgsfvalg  15724  lgsval2lem  15729  lgsmod  15745  lgsdir2lem4  15750  lgsdinn0  15767  lgsquad2lem2  15801  lgsquad3  15803  2lgslem1c  15809  2sqlem6  15839  2sqlem7  15840  isupgren  15936  wrdupgren  15937  isumgren  15946  wrdumgren  15947  isuspgren  15996  isusgren  15997  clwwlkext2edg  16217  clwwlknonex2  16234  2omap  16530  pw1map  16532  nnsf  16543  peano4nninf  16544  nninfalllem1  16546  nninfsellemqall  16553  nninfsellemeqinf  16554  nninffeq  16558  exmidsbthrlem  16562  isomninnlem  16570  iswomninnlem  16589  iswomni0  16591  ismkvnnlem  16592