Theorem ad2antrl 487

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  526  simprll  532  simprlr  533  elxp5  5099  f1oprg  5486  cnvf1olem  6203  tfrcl  6343  nnaordi  6487  swoer  6541  0er  6547  mapxpen  6826  fict  6846  dif1enen  6858  php5fin  6860  fin0  6863  fin0or  6864  diffisn  6871  infnfi  6873  unsnfi  6896  fidcenumlemrk  6931  sbthlemi8  6941  fiuni  6955  supmoti  6970  eldju2ndl  7049  eldju2ndr  7050  omp1eomlem  7071  difinfsnlem  7076  ctmlemr  7085  nninfwlpor  7150  exmidfodomrlemr  7179  exmidfodomrlemrALT  7180  enq0sym  7394  nqnq0pi  7400  addlocpr  7498  nqprl  7513  addnqprlemrl  7519  addnqprlemru  7520  mulnqprlemrl  7535  mulnqprlemru  7536  archpr  7605  cauappcvgprlemloc  7614  cauappcvgprlemladdfl  7617  archrecpr  7626  caucvgprlemdisj  7636  caucvgprlemloc  7637  caucvgprprlemml  7656  caucvgprprlemopl  7659  caucvgprprlemdisj  7664  caucvgprprlemloc  7665  suplocexprlemmu  7680  suplocexprlemdisj  7682  mulcmpblnrlemg  7702  caucvgsrlemgt1  7757  axarch  7853  axcaucvglemres  7861  cnegexlem2  8095  mulge0  8538  divdivap1  8640  divdivap2  8641  conjmulap  8646  ltdivmul  8792  nn0ge0div  9299  peano2uz2  9319  peano5uzti  9320  eluzp1m1  9510  xleadd1a  9830  iooshf  9909  divelunit  9959  eluzgtdifelfzo  10153  ioom  10217  modqcyc2  10316  modaddmodup  10343  uzennn  10392  seq3fveq2  10425  seq3id2  10465  seqfeq3  10468  expineg2  10485  mulexpzap  10516  leexp2r  10530  expnlbnd2  10601  hashfacen  10771  resqrexlemp1rp  10970  resqrexlemfp1  10973  negfi  11191  climcaucn  11314  fsum3cvg3  11359  fsum2dlemstep  11397  mptfzshft  11405  expcnvre  11466  fprodrev  11582  fprod2dlemstep  11585  moddvds  11761  dvdsflip  11811  addmodlteqALT  11819  nn0o  11866  zsupcllemex  11901  dfgcd2  11969  lcmgcdlem  12031  cncongr1  12057  prmind2  12074  isprm5lem  12095  isprm6  12101  cncongrprm  12111  oddpwdclemdc  12127  sqrt2irrap  12134  hashdvds  12175  crth  12178  prmdiveq  12190  hashgcdlem  12192  hashgcdeq  12193  pclem0  12240  pclemub  12241  pcprendvds2  12245  pcmul  12255  pcexp  12263  pcneg  12278  pc2dvds  12283  pcmpt  12295  prmpwdvds  12307  pockthg  12309  1arith  12319  4sqlem2  12341  ennnfonelemex  12369  setscom  12456  insubm  12703  isgrpinv  12756  tgcl  12858  lmbr2  13008  txcn  13069  txdis1cn  13072  txlm  13073  hmeoimaf1o  13108  txhmeo  13113  bl2in  13197  blssps  13221  blss  13222  blssexps  13223  blssex  13224  bdxmet  13295  xmetxp  13301  xmetxpbl  13302  xmettx  13304  metcnp3  13305  metcnpi3  13311  dedekindicc  13405  limcimolemlt  13427  rprelogbmul  13667  logbgcd1irr  13679  lgsne0  13733  2sqlem8  13753  qdencn  14059  trilpolemlt1  14073