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  5075  f1oprg  5459  cnvf1olem  6172  tfrcl  6312  nnaordi  6456  swoer  6509  0er  6515  mapxpen  6794  fict  6814  dif1enen  6826  php5fin  6828  fin0  6831  fin0or  6832  diffisn  6839  infnfi  6841  unsnfi  6864  fidcenumlemrk  6899  sbthlemi8  6909  fiuni  6923  supmoti  6938  eldju2ndl  7017  eldju2ndr  7018  omp1eomlem  7039  difinfsnlem  7044  ctmlemr  7053  exmidfodomrlemr  7138  exmidfodomrlemrALT  7139  enq0sym  7353  nqnq0pi  7359  addlocpr  7457  nqprl  7472  addnqprlemrl  7478  addnqprlemru  7479  mulnqprlemrl  7494  mulnqprlemru  7495  archpr  7564  cauappcvgprlemloc  7573  cauappcvgprlemladdfl  7576  archrecpr  7585  caucvgprlemdisj  7595  caucvgprlemloc  7596  caucvgprprlemml  7615  caucvgprprlemopl  7618  caucvgprprlemdisj  7623  caucvgprprlemloc  7624  suplocexprlemmu  7639  suplocexprlemdisj  7641  mulcmpblnrlemg  7661  caucvgsrlemgt1  7716  axarch  7812  axcaucvglemres  7820  cnegexlem2  8052  mulge0  8495  divdivap1  8597  divdivap2  8598  conjmulap  8603  ltdivmul  8748  nn0ge0div  9252  peano2uz2  9272  peano5uzti  9273  eluzp1m1  9463  xleadd1a  9778  iooshf  9857  divelunit  9907  eluzgtdifelfzo  10100  ioom  10164  modqcyc2  10263  modaddmodup  10290  uzennn  10339  seq3fveq2  10372  seq3id2  10412  seqfeq3  10415  expineg2  10432  mulexpzap  10463  leexp2r  10477  expnlbnd2  10547  hashfacen  10711  resqrexlemp1rp  10910  resqrexlemfp1  10913  negfi  11131  climcaucn  11252  fsum3cvg3  11297  fsum2dlemstep  11335  mptfzshft  11343  expcnvre  11404  fprodrev  11520  fprod2dlemstep  11523  moddvds  11699  dvdsflip  11747  addmodlteqALT  11755  nn0o  11802  zsupcllemex  11837  dfgcd2  11902  lcmgcdlem  11958  cncongr1  11984  prmind2  12001  isprm6  12026  cncongrprm  12036  oddpwdclemdc  12052  sqrt2irrap  12059  hashdvds  12100  crth  12103  prmdiveq  12115  hashgcdlem  12117  hashgcdeq  12118  ennnfonelemex  12185  setscom  12272  tgcl  12506  lmbr2  12656  txcn  12717  txdis1cn  12720  txlm  12721  hmeoimaf1o  12756  txhmeo  12761  bl2in  12845  blssps  12869  blss  12870  blssexps  12871  blssex  12872  bdxmet  12943  xmetxp  12949  xmetxpbl  12950  xmettx  12952  metcnp3  12953  metcnpi3  12959  dedekindicc  13053  limcimolemlt  13075  rprelogbmul  13314  logbgcd1irr  13326  qdencn  13640  trilpolemlt1  13654