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  529  simprll  537  simprlr  538  elxp5  5155  f1oprg  5545  elovmporab1w  6121  cnvf1olem  6279  tfrcl  6419  nnaordi  6563  swoer  6617  0er  6623  pw2f1odclem  6892  mapxpen  6906  fict  6926  dif1enen  6938  php5fin  6940  fin0  6943  fin0or  6944  diffisn  6951  infnfi  6953  unsnfi  6977  fidcenumlemrk  7015  sbthlemi8  7025  fiuni  7039  supmoti  7054  eldju2ndl  7133  eldju2ndr  7134  omp1eomlem  7155  difinfsnlem  7160  ctmlemr  7169  nninfninc  7184  nninfwlpor  7235  exmidfodomrlemr  7264  exmidfodomrlemrALT  7265  enq0sym  7494  nqnq0pi  7500  addlocpr  7598  nqprl  7613  addnqprlemrl  7619  addnqprlemru  7620  mulnqprlemrl  7635  mulnqprlemru  7636  archpr  7705  cauappcvgprlemloc  7714  cauappcvgprlemladdfl  7717  archrecpr  7726  caucvgprlemdisj  7736  caucvgprlemloc  7737  caucvgprprlemml  7756  caucvgprprlemopl  7759  caucvgprprlemdisj  7764  caucvgprprlemloc  7765  suplocexprlemmu  7780  suplocexprlemdisj  7782  mulcmpblnrlemg  7802  caucvgsrlemgt1  7857  axarch  7953  axcaucvglemres  7961  cnegexlem2  8197  mulge0  8640  divdivap1  8744  divdivap2  8745  conjmulap  8750  ltdivmul  8897  nn0ge0div  9407  peano2uz2  9427  peano5uzti  9428  eluzp1m1  9619  xleadd1a  9942  iooshf  10021  divelunit  10071  eluzgtdifelfzo  10267  ioom  10332  modqcyc2  10434  modaddmodup  10461  uzennn  10510  seq3fveq2  10549  seqfveq2g  10551  seq3id2  10600  seqfeq3  10603  expineg2  10622  mulexpzap  10653  leexp2r  10667  expnlbnd2  10739  hashfacen  10910  wrdred1hash  10960  resqrexlemp1rp  11153  resqrexlemfp1  11156  negfi  11374  climcaucn  11497  fsum3cvg3  11542  fsum2dlemstep  11580  mptfzshft  11588  expcnvre  11649  fprodrev  11765  fprod2dlemstep  11768  moddvds  11945  dvdsflip  11996  addmodlteqALT  12004  nn0o  12051  zsupcllemex  12086  dfgcd2  12154  lcmgcdlem  12218  cncongr1  12244  prmind2  12261  isprm5lem  12282  isprm6  12288  cncongrprm  12298  oddpwdclemdc  12314  sqrt2irrap  12321  hashdvds  12362  crth  12365  prmdiveq  12377  hashgcdlem  12379  hashgcdeq  12380  pclem0  12427  pclemub  12428  pcprendvds2  12432  pcmul  12442  pcexp  12450  pcneg  12466  pc2dvds  12471  pcmpt  12484  prmpwdvds  12496  pockthg  12498  1arith  12508  4sqlem2  12530  4sqlemafi  12536  4sqlem11  12542  ennnfonelemex  12574  setscom  12661  subsubm  13058  insubm  13060  isgrpinv  13129  subsubg  13270  subsubrng  13713  subsubrg  13744  islss4  13881  znf1o  14150  znidomb  14157  tgcl  14243  lmbr2  14393  txcn  14454  txdis1cn  14457  txlm  14458  hmeoimaf1o  14493  txhmeo  14498  bl2in  14582  blssps  14606  blss  14607  blssexps  14608  blssex  14609  bdxmet  14680  xmetxp  14686  xmetxpbl  14687  xmettx  14689  metcnp3  14690  metcnpi3  14696  dedekindicc  14812  ivthdichlem  14830  limcimolemlt  14843  dvmptfsum  14904  rprelogbmul  15128  logbgcd1irr  15140  lgsne0  15195  gausslemma2dlem1a  15215  lgseisenlem2  15228  lgsquadlemsfi  15232  lgsquadlem1  15234  lgsquadlem2  15235  lgsquadlem3  15236  lgsquad2lem2  15239  2sqlem8  15280  qdencn  15587  trilpolemlt1  15601