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  5114  f1oprg  5502  cnvf1olem  6220  tfrcl  6360  nnaordi  6504  swoer  6558  0er  6564  mapxpen  6843  fict  6863  dif1enen  6875  php5fin  6877  fin0  6880  fin0or  6881  diffisn  6888  infnfi  6890  unsnfi  6913  fidcenumlemrk  6948  sbthlemi8  6958  fiuni  6972  supmoti  6987  eldju2ndl  7066  eldju2ndr  7067  omp1eomlem  7088  difinfsnlem  7093  ctmlemr  7102  nninfwlpor  7167  exmidfodomrlemr  7196  exmidfodomrlemrALT  7197  enq0sym  7426  nqnq0pi  7432  addlocpr  7530  nqprl  7545  addnqprlemrl  7551  addnqprlemru  7552  mulnqprlemrl  7567  mulnqprlemru  7568  archpr  7637  cauappcvgprlemloc  7646  cauappcvgprlemladdfl  7649  archrecpr  7658  caucvgprlemdisj  7668  caucvgprlemloc  7669  caucvgprprlemml  7688  caucvgprprlemopl  7691  caucvgprprlemdisj  7696  caucvgprprlemloc  7697  suplocexprlemmu  7712  suplocexprlemdisj  7714  mulcmpblnrlemg  7734  caucvgsrlemgt1  7789  axarch  7885  axcaucvglemres  7893  cnegexlem2  8127  mulge0  8570  divdivap1  8674  divdivap2  8675  conjmulap  8680  ltdivmul  8827  nn0ge0div  9334  peano2uz2  9354  peano5uzti  9355  eluzp1m1  9545  xleadd1a  9867  iooshf  9946  divelunit  9996  eluzgtdifelfzo  10190  ioom  10254  modqcyc2  10353  modaddmodup  10380  uzennn  10429  seq3fveq2  10462  seq3id2  10502  seqfeq3  10505  expineg2  10522  mulexpzap  10553  leexp2r  10567  expnlbnd2  10638  hashfacen  10807  resqrexlemp1rp  11006  resqrexlemfp1  11009  negfi  11227  climcaucn  11350  fsum3cvg3  11395  fsum2dlemstep  11433  mptfzshft  11441  expcnvre  11502  fprodrev  11618  fprod2dlemstep  11621  moddvds  11797  dvdsflip  11847  addmodlteqALT  11855  nn0o  11902  zsupcllemex  11937  dfgcd2  12005  lcmgcdlem  12067  cncongr1  12093  prmind2  12110  isprm5lem  12131  isprm6  12137  cncongrprm  12147  oddpwdclemdc  12163  sqrt2irrap  12170  hashdvds  12211  crth  12214  prmdiveq  12226  hashgcdlem  12228  hashgcdeq  12229  pclem0  12276  pclemub  12277  pcprendvds2  12281  pcmul  12291  pcexp  12299  pcneg  12314  pc2dvds  12319  pcmpt  12331  prmpwdvds  12343  pockthg  12345  1arith  12355  4sqlem2  12377  ennnfonelemex  12405  setscom  12492  insubm  12800  isgrpinv  12854  subsubg  12983  tgcl  13346  lmbr2  13496  txcn  13557  txdis1cn  13560  txlm  13561  hmeoimaf1o  13596  txhmeo  13601  bl2in  13685  blssps  13709  blss  13710  blssexps  13711  blssex  13712  bdxmet  13783  xmetxp  13789  xmetxpbl  13790  xmettx  13792  metcnp3  13793  metcnpi3  13799  dedekindicc  13893  limcimolemlt  13915  rprelogbmul  14155  logbgcd1irr  14167  lgsne0  14221  2sqlem8  14241  qdencn  14546  trilpolemlt1  14560