Theorem ad2antrl 490

Description: Deduction adding two conjuncts to antecedent. (Contributed by NM, 19-Oct-1999.)

Hypothesis

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

Assertion

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

Proof of Theorem ad2antrl

Step	Hyp	Ref	Expression
1		ad2ant.1	. . 3 |- ( ph -> ps )
2	1	adantr 276	. 2 |- ( ( ph /\ th ) -> ps )
3	2	adantl 277	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:  simprl  531  simprll  539  simprlr  540  elxp5  5232  f1oprg  5638  elovmporab1w  6233  cnvf1olem  6398  ressuppss  6432  tfrcl  6573  nnaordi  6719  swoer  6773  0er  6779  modom  7037  pw2f1odclem  7063  mapxpen  7077  fict  7098  dif1enen  7112  php5fin  7114  fin0  7117  fin0or  7118  diffisn  7125  infnfi  7127  unsnfi  7154  fidcenumlemrk  7196  sbthlemi8  7206  fiuni  7237  supmoti  7252  eldju2ndl  7331  eldju2ndr  7332  omp1eomlem  7353  difinfsnlem  7358  ctmlemr  7367  nninfninc  7382  nninfwlpor  7433  exmidfodomrlemr  7473  exmidfodomrlemrALT  7474  enq0sym  7712  nqnq0pi  7718  addlocpr  7816  nqprl  7831  addnqprlemrl  7837  addnqprlemru  7838  mulnqprlemrl  7853  mulnqprlemru  7854  archpr  7923  cauappcvgprlemloc  7932  cauappcvgprlemladdfl  7935  archrecpr  7944  caucvgprlemdisj  7954  caucvgprlemloc  7955  caucvgprprlemml  7974  caucvgprprlemopl  7977  caucvgprprlemdisj  7982  caucvgprprlemloc  7983  suplocexprlemmu  7998  suplocexprlemdisj  8000  mulcmpblnrlemg  8020  caucvgsrlemgt1  8075  axarch  8171  axcaucvglemres  8179  cnegexlem2  8414  mulge0  8858  divdivap1  8962  divdivap2  8963  conjmulap  8968  ltdivmul  9115  nn0ge0div  9628  peano2uz2  9648  peano5uzti  9649  eluzp1m1  9841  xleadd1a  10169  iooshf  10248  divelunit  10298  eluzgtdifelfzo  10505  zsupcllemex  10553  ioom  10583  modqcyc2  10685  modaddmodup  10712  uzennn  10761  seq3fveq2  10800  seqfveq2g  10802  seq3id2  10851  seqfeq3  10854  expineg2  10873  mulexpzap  10904  leexp2r  10918  expnlbnd2  10990  hashfacen  11163  wrdred1hash  11223  ccatsymb  11245  swrdwrdsymbg  11311  swrdsb0eq  11312  ccatpfx  11348  swrdswrd  11352  wrdind  11369  wrd2ind  11370  swrdccatin1  11372  swrdccatin2  11376  pfxccatin12lem2  11378  pfxccatin12  11380  pfxccat3  11381  swrdccat  11382  resqrexlemp1rp  11646  resqrexlemfp1  11649  negfi  11868  climcaucn  11991  fsum3cvg3  12037  fsum2dlemstep  12075  mptfzshft  12083  expcnvre  12144  fprodrev  12260  fprod2dlemstep  12263  moddvds  12440  dvdsflip  12492  addmodlteqALT  12500  nn0o  12548  dfgcd2  12665  lcmgcdlem  12729  cncongr1  12755  prmind2  12772  isprm5lem  12793  isprm6  12799  cncongrprm  12809  oddpwdclemdc  12825  sqrt2irrap  12832  hashdvds  12873  crth  12876  prmdiveq  12888  hashgcdlem  12890  hashgcdeq  12892  pclem0  12939  pclemub  12940  pcprendvds2  12944  pcmul  12954  pcexp  12962  pcneg  12978  pc2dvds  12983  pcmpt  12996  prmpwdvds  13008  pockthg  13010  1arith  13020  4sqlem2  13042  4sqlemafi  13048  4sqlem11  13054  ennnfonelemex  13115  setscom  13202  subsubm  13646  insubm  13648  isgrpinv  13717  subsubg  13864  subsubrng  14309  subsubrg  14340  islss4  14478  znf1o  14747  znidomb  14754  tgcl  14875  lmbr2  15025  txcn  15086  txdis1cn  15089  txlm  15090  hmeoimaf1o  15125  txhmeo  15130  bl2in  15214  blssps  15238  blss  15239  blssexps  15240  blssex  15241  bdxmet  15312  xmetxp  15318  xmetxpbl  15319  xmettx  15321  metcnp3  15322  metcnpi3  15328  dedekindicc  15444  ivthdichlem  15462  limcimolemlt  15475  dvmptfsum  15536  rprelogbmul  15766  logbgcd1irr  15778  mpodvdsmulf1o  15804  lgsne0  15857  gausslemma2dlem1a  15877  lgseisenlem2  15890  lgsquadlemsfi  15894  lgsquadlem1  15896  lgsquadlem2  15897  lgsquadlem3  15898  lgsquad2lem2  15901  2sqlem8  15942  uspgredg2vlem  16161  subuhgr  16213  subupgr  16214  subumgr  16215  iswlkg  16270  wlkl1loop  16299  upgriswlkdc  16301  clwwlkccatlem  16341  clwwlkn1loopb  16361  clwwlknonex2e  16381  2omap  16715  qdencn  16755  trilpolemlt1  16773