Theorem ad2antlr 481

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 274	. 2 |- ( ( ph /\ th ) -> ps )
3	2	adantll 468	1 |- ( ( ( ch /\ ph ) /\ th ) -> ps )

Syntax hints:   -> wi 4   /\ wa 103

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

This theorem is referenced by:  ad3antlr  485  simplr  520  simplrl  525  simplrr  526  ordtri2or2exmidlem  4449  en2lp  4477  foun  5394  f1oprg  5419  fcof1o  5698  foeqcnvco  5699  f1eqcocnv  5700  caovord3  5952  f1o2ndf1  6133  smores2  6199  frecrdg  6313  nnaordex  6431  xpdom2  6733  xpen  6747  mapen  6748  xpmapenlem  6751  nndomo  6766  phpm  6767  fidifsnen  6772  isinfinf  6799  finexdc  6804  fientri3  6811  fiintim  6825  xpfi  6826  f1dmvrnfibi  6840  sbthlemi8  6860  djudom  6986  omp1eomlem  6987  difinfsn  6993  ctmlemr  7001  ctssdccl  7004  enomnilem  7018  finomni  7020  ismkvnex  7037  enmkvlem  7043  exmidfodomrlemrALT  7076  dfplpq2  7186  recclnq  7224  subhalfnqq  7246  distrnq0  7291  prarloclem3step  7328  genpml  7349  genpmu  7350  addnqprl  7361  addnqpru  7362  appdivnq  7395  mulnqprl  7400  mulnqpru  7401  mullocpr  7403  ltexprlemfl  7441  ltexprlemfu  7443  ltmprr  7474  archpr  7475  cauappcvgprlemm  7477  caucvgprlemladdrl  7510  caucvgprprlemopl  7529  caucvgprprlemopu  7531  recexgt0sr  7605  mulgt0sr  7610  elrealeu  7661  axcaucvglemcau  7730  axcaucvglemres  7731  cnegex  7964  apirr  8391  mulge0  8405  lemul12a  8644  lediv2a  8677  creur  8741  nndiv  8785  zaddcllemneg  9117  peano5uzti  9183  supinfneg  9417  infsupneg  9418  divfnzn  9440  xrltso  9612  xpncan  9684  xltadd1  9689  xleaddadd  9700  elioc2  9749  elico2  9750  elicc2  9751  exfzdc  10048  exbtwnzlemex  10058  rebtwn2z  10063  modqid  10153  modqcyc  10163  mulqaddmodid  10168  modqadd2mod  10178  addmodlteq  10202  frecuzrdgg  10220  seq3val  10262  seqvalcd  10263  seq3clss  10271  iseqf1olemqcl  10290  iseqf1olemnab  10292  seq3f1olemp  10306  seq3f1o  10308  fser0const  10320  ser3ge0  10321  exp3vallem  10325  facndiv  10517  faclbnd  10519  bcval5  10541  hashen  10562  fihashdom  10581  hashunlem  10582  hashfacen  10611  zfz1isolemiso  10614  seq3coll  10617  caucvgre  10785  resqrexlemlo  10817  cau3lem  10918  qdenre  11006  rexico  11025  fimaxre2  11030  xrmaxiflemcl  11046  xrmaxifle  11047  xrmaxiflemcom  11050  2clim  11102  cn1lem  11115  climsqz  11136  climsqz2  11137  climcau  11148  sumrbdclem  11178  summodclem2a  11182  fsum3  11188  fsumcl2lem  11199  fsumadd  11207  sumsnf  11210  fsum2dlemstep  11235  fisum0diag2  11248  fsummulc2  11249  mertenslemub  11335  mertenslemi1  11336  mertensabs  11338  ntrivcvgap  11349  prodrbdclem  11372  prodmodclem3  11376  prodmodclem2a  11377  prodmodc  11379  efaddlem  11417  tanaddaplem  11481  zdvdsdc  11550  dvdseq  11582  dvdsext  11589  odd2np1  11606  sqoddm1div8z  11619  nno  11639  zsupcllemstep  11674  infssuzex  11678  dfgcd3  11734  dvdslcm  11786  lcmneg  11791  lcmgcdlem  11794  ncoprmgcdne1b  11806  qredeq  11813  qredeu  11814  divgcdcoprm0  11818  exprmfct  11854  prmdvdsfz  11855  rpexp1i  11868  sqrt2irr  11876  nonsq  11921  ctinfom  11977  enctlem  11981  setsfun  12033  setsfun0  12034  setscom  12038  tgdom  12280  ssrest  12390  cnfval  12402  cnpfval  12403  cnpval  12406  iscnp3  12411  ssidcn  12418  cnpnei  12427  cnntr  12433  cncnp  12438  cnptopresti  12446  tx1cn  12477  upxp  12480  imasnopn  12507  bdmet  12710  metcnp  12720  ivthinclemlr  12823  ivthinclemur  12825  ivthinc  12829  dvrecap  12885  pilem3  12912  relogeftb  12994  logbgcd1irr  13092  nnsf  13374  peano4nninf  13375  nninfalllemn  13377  nninfalllem1  13378  nninfsellemqall  13386  nninfsellemeqinf  13387  nninffeq  13391  exmidsbthrlem  13392  isomninnlem  13400  iswomninnlem  13417  ismkvnnlem  13419