Theorem ad2antrl 475

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 271	. 2 |- ( ( ph /\ th ) -> ps )
3	2	adantl 272	1 |- ( ( ch /\ ( ph /\ th ) ) -> ps )

Syntax hints:   -> wi 4   /\ wa 103

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

This theorem is referenced by:  simprl  499  simprll  505  simprlr  506  elxp5  4932  f1oprg  5308  cnvf1olem  6003  tfrcl  6143  nnaordi  6281  swoer  6334  0er  6340  mapxpen  6618  fict  6638  dif1enen  6650  php5fin  6652  fin0  6655  fin0or  6656  diffisn  6663  infnfi  6665  unsnfi  6683  fidcenumlemrk  6717  sbthlemi8  6727  supmoti  6742  eldju2ndl  6817  eldju2ndr  6818  ctmlemr  6844  exmidfodomrlemr  6889  exmidfodomrlemrALT  6890  enq0sym  7052  nqnq0pi  7058  addlocpr  7156  nqprl  7171  addnqprlemrl  7177  addnqprlemru  7178  mulnqprlemrl  7193  mulnqprlemru  7194  archpr  7263  cauappcvgprlemloc  7272  cauappcvgprlemladdfl  7275  archrecpr  7284  caucvgprlemdisj  7294  caucvgprlemloc  7295  caucvgprprlemml  7314  caucvgprprlemopl  7317  caucvgprprlemdisj  7322  caucvgprprlemloc  7323  mulcmpblnrlemg  7347  caucvgsrlemgt1  7401  axarch  7487  axcaucvglemres  7495  cnegexlem2  7719  mulge0  8157  divdivap1  8251  divdivap2  8252  conjmulap  8257  ltdivmul  8398  nn0ge0div  8894  peano2uz2  8914  peano5uzti  8915  eluzp1m1  9103  iooshf  9431  divelunit  9480  eluzgtdifelfzo  9669  ioom  9733  modqcyc2  9828  modaddmodup  9855  iseqval  9932  iseqfveq2  9951  seq3fveq2  9953  seq3id2  10001  iseqid2  10002  expineg2  10025  mulexpzap  10056  leexp2r  10070  expnlbnd2  10140  hashfacen  10302  resqrexlemp1rp  10500  resqrexlemfp1  10503  negfi  10720  climcaucn  10801  fsum3cvg3  10850  fsum2dlemstep  10889  mptfzshft  10897  expcnvre  10958  moddvds  11144  dvdsflip  11191  addmodlteqALT  11199  nn0o  11246  zsupcllemex  11281  dfgcd2  11342  lcmgcdlem  11398  cncongr1  11424  prmind2  11441  isprm6  11465  cncongrprm  11475  oddpwdclemdc  11490  sqrt2irrap  11497  hashdvds  11536  crth  11539  hashgcdlem  11542  hashgcdeq  11543  setscom  11595  tgcl  11825  qdencn  12187