Theorem ad2antrl 482

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 274	. 2 |- ( ( ph /\ th ) -> ps )
3	2	adantl 275	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:  simprl  521  simprll  527  simprlr  528  elxp5  5035  f1oprg  5419  cnvf1olem  6129  tfrcl  6269  nnaordi  6412  swoer  6465  0er  6471  mapxpen  6750  fict  6770  dif1enen  6782  php5fin  6784  fin0  6787  fin0or  6788  diffisn  6795  infnfi  6797  unsnfi  6815  fidcenumlemrk  6850  sbthlemi8  6860  fiuni  6874  supmoti  6888  eldju2ndl  6965  eldju2ndr  6966  omp1eomlem  6987  difinfsnlem  6992  ctmlemr  7001  exmidfodomrlemr  7075  exmidfodomrlemrALT  7076  enq0sym  7264  nqnq0pi  7270  addlocpr  7368  nqprl  7383  addnqprlemrl  7389  addnqprlemru  7390  mulnqprlemrl  7405  mulnqprlemru  7406  archpr  7475  cauappcvgprlemloc  7484  cauappcvgprlemladdfl  7487  archrecpr  7496  caucvgprlemdisj  7506  caucvgprlemloc  7507  caucvgprprlemml  7526  caucvgprprlemopl  7529  caucvgprprlemdisj  7534  caucvgprprlemloc  7535  suplocexprlemmu  7550  suplocexprlemdisj  7552  mulcmpblnrlemg  7572  caucvgsrlemgt1  7627  axarch  7723  axcaucvglemres  7731  cnegexlem2  7962  mulge0  8405  divdivap1  8507  divdivap2  8508  conjmulap  8513  ltdivmul  8658  nn0ge0div  9162  peano2uz2  9182  peano5uzti  9183  eluzp1m1  9373  xleadd1a  9686  iooshf  9765  divelunit  9815  eluzgtdifelfzo  10005  ioom  10069  modqcyc2  10164  modaddmodup  10191  uzennn  10240  seq3fveq2  10273  seq3id2  10313  seqfeq3  10316  expineg2  10333  mulexpzap  10364  leexp2r  10378  expnlbnd2  10448  hashfacen  10611  resqrexlemp1rp  10810  resqrexlemfp1  10813  negfi  11031  climcaucn  11152  fsum3cvg3  11197  fsum2dlemstep  11235  mptfzshft  11243  expcnvre  11304  moddvds  11538  dvdsflip  11585  addmodlteqALT  11593  nn0o  11640  zsupcllemex  11675  dfgcd2  11738  lcmgcdlem  11794  cncongr1  11820  prmind2  11837  isprm6  11861  cncongrprm  11871  oddpwdclemdc  11887  sqrt2irrap  11894  hashdvds  11933  crth  11936  hashgcdlem  11939  hashgcdeq  11940  ennnfonelemex  11963  setscom  12038  tgcl  12272  lmbr2  12422  txcn  12483  txdis1cn  12486  txlm  12487  hmeoimaf1o  12522  txhmeo  12527  bl2in  12611  blssps  12635  blss  12636  blssexps  12637  blssex  12638  bdxmet  12709  xmetxp  12715  xmetxpbl  12716  xmettx  12718  metcnp3  12719  metcnpi3  12725  dedekindicc  12819  limcimolemlt  12841  rprelogbmul  13080  logbgcd1irr  13092  qdencn  13397  trilpolemlt1  13409