Theorem ad2antlr 493

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 480	1 |- ( ( ( ch /\ ph ) /\ th ) -> ps )

This proof depends on syntax axioms:   -> wi 4   /\ wa 104

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem is used by:  ad3antlr  497  simplr  533  simplrl  541  simplrr  542  ordtri2or2exmidlem  4673  en2lp  4701  foun  5658  f1oprg  5685  fcof1o  5995  foeqcnvco  5996  f1eqcocnv  5997  caovord3  6263  f1o2ndf1  6464  suppfnss  6497  suppssdc  6500  suppssfvg  6503  smores2  6565  frecrdg  6679  nnaordex  6801  xpdom2  7129  xpen  7145  mapen  7146  xpmapenlem  7149  nndomo  7165  phpm  7167  fidifsnen  7172  isinfinf  7201  fidcen  7203  finexdc  7207  elssdc  7209  fientri3  7222  fiintim  7238  xpfi  7239  f1dmvrnfibi  7258  sbthlemi8  7281  2omap  7319  2omapfi  7321  djudom  7434  omp1eomlem  7435  difinfsn  7441  ctmlemr  7449  ctssdccl  7452  nnnninfeq  7469  enomnilem  7479  finomni  7481  ismkvnex  7496  enmkvlem  7502  nninfwlpoimlemginf  7517  exmidfodomrlemrALT  7556  exmidontriim  7582  netap  7621  exmidapne  7627  acnccim  7639  dfplpq2  7722  recclnq  7760  subhalfnqq  7782  distrnq0  7827  prarloclem3step  7864  genpml  7885  genpmu  7886  addnqprl  7897  addnqpru  7898  appdivnq  7931  mulnqprl  7936  mulnqpru  7937  mullocpr  7939  ltexprlemfl  7977  ltexprlemfu  7979  ltmprr  8010  archpr  8011  cauappcvgprlemm  8013  caucvgprlemladdrl  8046  caucvgprprlemopl  8065  caucvgprprlemopu  8067  recexgt0sr  8141  mulgt0sr  8146  elrealeu  8197  axcaucvglemcau  8266  axcaucvglemres  8267  cnegex  8506  apirr  8936  mulge0  8950  lemul12a  9195  lediv2a  9228  creur  9292  nndiv  9348  zaddcllemneg  9688  peano5uzti  9759  supinfneg  10005  infsupneg  10006  divfnzn  10031  xrltso  10209  xpncan  10284  xltadd1  10289  xleaddadd  10300  elioc2  10349  elico2  10350  elicc2  10351  exfzdc  10670  zsupcllemstep  10673  infssuzex  10677  suprzubdc  10682  exbtwnzlemex  10695  rebtwn2z  10700  modqid  10801  modqcyc  10811  mulqaddmodid  10816  modqadd2mod  10826  addmodlteq  10850  frecuzrdgg  10868  nninfinf  10895  seq3val  10912  seqvalcd  10913  seq3clss  10923  iseqf1olemqcl  10951  iseqf1olemnab  10953  seq3f1olemp  10967  seq3f1o  10969  seqf1oglem1  10971  seqfeq4g  10983  fser0const  10987  ser3ge0  10988  exp3vallem  10992  qsqeqor  11102  nn0sqdc  11162  facndiv  11193  faclbnd  11195  bcval5  11217  hashen  11239  fihashdom  11259  hashunlem  11260  hashfacen  11300  zfz1isolemiso  11307  seq3coll  11310  ccatsymb  11386  ccatrn  11393  ccatw2s1p2  11430  swrdccatin1  11513  swrdccatin2  11517  swrdccat3b  11528  caucvgre  11763  resqrexlemlo  11795  cau3lem  11897  qdenre  11985  rexico  12004  fimaxre2  12010  2zinfmin  12028  xrmaxiflemcl  12030  xrmaxifle  12031  xrmaxiflemcom  12034  2clim  12086  cn1lem  12099  climsqz  12120  climsqz2  12121  climcau  12132  sumrbdclem  12163  summodclem2a  12167  fsum3  12173  fsumcl2lem  12184  fsumadd  12192  sumsnf  12195  fsum2dlemstep  12220  fisum0diag2  12233  fsummulc2  12234  mertenslemub  12320  mertenslemi1  12321  mertensabs  12323  ntrivcvgap  12334  prodrbdclem  12357  prodmodclem3  12361  prodmodclem2a  12362  prodmodc  12364  prod1dc  12372  prodsnf  12378  fprod2dlemstep  12408  efaddlem  12460  tanaddaplem  12524  zdvdsdc  12598  dvdseq  12634  dvdsext  12641  odd2np1  12659  sqoddm1div8z  12672  nno  12692  dfgcd3  12806  nninfctlemfo  12836  dvdslcm  12866  lcmneg  12871  lcmgcdlem  12874  ncoprmgcdne1b  12886  qredeq  12893  qredeu  12894  divgcdcoprm0  12898  exprmfct  12936  prmdvdsfz  12937  isprm5  12940  rpexp1i  12952  sqrt2irr  12960  nonsq  13006  sqrtrirr  13008  eulerthlemrprm  13030  eulerthlema  13031  phisum  13042  modprmn0modprm0  13058  pclemdc  13090  pcz  13134  pcmpt  13145  fldivp1  13150  pcfac  13152  expnprm  13155  oddprmdvds  13156  prmpwdvds  13157  infpnlem1  13161  1arith  13169  4sqlem2  13191  4sqlemafi  13197  4sqleminfi  13199  4sqexercise2  13201  4sqlemsdc  13202  ballotfilemsv  13305  ballotfilemsima  13311  ctinfom  13371  enctlem  13375  nninfdclemlt  13394  setsfun  13439  setsfun0  13440  setscom  13444  gzsumfzval  13764  mndissubm  13835  resmhm  13847  resmhm2  13848  mhmco  13850  gzsumwsubmcl  13854  gzsumwmhm  13856  dfgrp2  13885  isgrpinv  13912  mulgval  13978  mulgnnp1  13986  mulgz  14006  grpissubg  14050  resghm  14116  cntzsgrpcl  14161  cntzsubm  14164  cntzmhm  14167  qusecsub  14219  gsumf1ofi  14244  isrng  14317  lmodfopne  14747  dflidl2rng  14902  mulgrhm2  15029  znidomb  15077  znunit  15078  issubassa2  15119  psrbaglesuppg  15141  psrbagfi  15143  tgdom  15264  ssrest  15374  cnfval  15386  cnpfval  15387  cnpval  15390  iscnp3  15395  ssidcn  15402  cnpnei  15411  cnntr  15417  cncnp  15422  cnptopresti  15430  tx1cn  15461  upxp  15464  imasnopn  15491  bdmet  15694  metcnp  15704  ivthinclemlr  15829  ivthinclemur  15831  ivthinc  15835  dvrecap  15905  dvmptfsum  15917  elply2  15927  plymullem1  15940  plycolemc  15950  plycjlemc  15952  dvply1  15957  pilem3  15976  relogeftb  16058  logbgcd1irr  16164  birthdaylem3  16188  mpodvdsmulf1o  16245  chtublem  16256  mersenne  16258  bposlem1  16272  bposlem3  16274  bposlem5  16276  lgslem4  16288  lgsval  16289  lgsfvalg  16290  lgsval2lem  16295  lgsmod  16311  lgsdir2lem4  16316  lgsdinn0  16333  lgsquad2lem2  16367  lgsquad3  16369  2lgslem1c  16375  2sqlem6  16405  2sqlem7  16406  isupgren  16502  wrdupgren  16503  isumgren  16512  wrdumgren  16513  isuspgren  16564  isusgren  16565  clwwlkext2edg  16829  clwwlknonex2  16846  depindlem3  16915  pw1map  17191  nnsf  17214  peano4nninf  17215  nninfalllem1  17217  nninfsellemqall  17224  nninfsellemeqinf  17225  nninffeq  17229  exmidsbthrlem  17233  isomninnlem  17245  iswomninnlem  17266  iswomni0  17268  ismkvnnlem  17269