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  5158  f1oprg  5548  elovmporab1w  6124  cnvf1olem  6282  tfrcl  6422  nnaordi  6566  swoer  6620  0er  6626  pw2f1odclem  6895  mapxpen  6909  fict  6929  dif1enen  6941  php5fin  6943  fin0  6946  fin0or  6947  diffisn  6954  infnfi  6956  unsnfi  6980  fidcenumlemrk  7020  sbthlemi8  7030  fiuni  7044  supmoti  7059  eldju2ndl  7138  eldju2ndr  7139  omp1eomlem  7160  difinfsnlem  7165  ctmlemr  7174  nninfninc  7189  nninfwlpor  7240  exmidfodomrlemr  7269  exmidfodomrlemrALT  7270  enq0sym  7499  nqnq0pi  7505  addlocpr  7603  nqprl  7618  addnqprlemrl  7624  addnqprlemru  7625  mulnqprlemrl  7640  mulnqprlemru  7641  archpr  7710  cauappcvgprlemloc  7719  cauappcvgprlemladdfl  7722  archrecpr  7731  caucvgprlemdisj  7741  caucvgprlemloc  7742  caucvgprprlemml  7761  caucvgprprlemopl  7764  caucvgprprlemdisj  7769  caucvgprprlemloc  7770  suplocexprlemmu  7785  suplocexprlemdisj  7787  mulcmpblnrlemg  7807  caucvgsrlemgt1  7862  axarch  7958  axcaucvglemres  7966  cnegexlem2  8202  mulge0  8646  divdivap1  8750  divdivap2  8751  conjmulap  8756  ltdivmul  8903  nn0ge0div  9413  peano2uz2  9433  peano5uzti  9434  eluzp1m1  9625  xleadd1a  9948  iooshf  10027  divelunit  10077  eluzgtdifelfzo  10273  zsupcllemex  10320  ioom  10350  modqcyc2  10452  modaddmodup  10479  uzennn  10528  seq3fveq2  10567  seqfveq2g  10569  seq3id2  10618  seqfeq3  10621  expineg2  10640  mulexpzap  10671  leexp2r  10685  expnlbnd2  10757  hashfacen  10928  wrdred1hash  10978  resqrexlemp1rp  11171  resqrexlemfp1  11174  negfi  11393  climcaucn  11516  fsum3cvg3  11561  fsum2dlemstep  11599  mptfzshft  11607  expcnvre  11668  fprodrev  11784  fprod2dlemstep  11787  moddvds  11964  dvdsflip  12016  addmodlteqALT  12024  nn0o  12072  dfgcd2  12181  lcmgcdlem  12245  cncongr1  12271  prmind2  12288  isprm5lem  12309  isprm6  12315  cncongrprm  12325  oddpwdclemdc  12341  sqrt2irrap  12348  hashdvds  12389  crth  12392  prmdiveq  12404  hashgcdlem  12406  hashgcdeq  12408  pclem0  12455  pclemub  12456  pcprendvds2  12460  pcmul  12470  pcexp  12478  pcneg  12494  pc2dvds  12499  pcmpt  12512  prmpwdvds  12524  pockthg  12526  1arith  12536  4sqlem2  12558  4sqlemafi  12564  4sqlem11  12570  ennnfonelemex  12631  setscom  12718  subsubm  13115  insubm  13117  isgrpinv  13186  subsubg  13327  subsubrng  13770  subsubrg  13801  islss4  13938  znf1o  14207  znidomb  14214  tgcl  14300  lmbr2  14450  txcn  14511  txdis1cn  14514  txlm  14515  hmeoimaf1o  14550  txhmeo  14555  bl2in  14639  blssps  14663  blss  14664  blssexps  14665  blssex  14666  bdxmet  14737  xmetxp  14743  xmetxpbl  14744  xmettx  14746  metcnp3  14747  metcnpi3  14753  dedekindicc  14869  ivthdichlem  14887  limcimolemlt  14900  dvmptfsum  14961  rprelogbmul  15191  logbgcd1irr  15203  mpodvdsmulf1o  15226  lgsne0  15279  gausslemma2dlem1a  15299  lgseisenlem2  15312  lgsquadlemsfi  15316  lgsquadlem1  15318  lgsquadlem2  15319  lgsquadlem3  15320  lgsquad2lem2  15323  2sqlem8  15364  qdencn  15671  trilpolemlt1  15685