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  5154  f1oprg  5544  elovmporab1w  6119  cnvf1olem  6277  tfrcl  6417  nnaordi  6561  swoer  6615  0er  6621  pw2f1odclem  6890  mapxpen  6904  fict  6924  dif1enen  6936  php5fin  6938  fin0  6941  fin0or  6942  diffisn  6949  infnfi  6951  unsnfi  6975  fidcenumlemrk  7013  sbthlemi8  7023  fiuni  7037  supmoti  7052  eldju2ndl  7131  eldju2ndr  7132  omp1eomlem  7153  difinfsnlem  7158  ctmlemr  7167  nninfninc  7182  nninfwlpor  7233  exmidfodomrlemr  7262  exmidfodomrlemrALT  7263  enq0sym  7492  nqnq0pi  7498  addlocpr  7596  nqprl  7611  addnqprlemrl  7617  addnqprlemru  7618  mulnqprlemrl  7633  mulnqprlemru  7634  archpr  7703  cauappcvgprlemloc  7712  cauappcvgprlemladdfl  7715  archrecpr  7724  caucvgprlemdisj  7734  caucvgprlemloc  7735  caucvgprprlemml  7754  caucvgprprlemopl  7757  caucvgprprlemdisj  7762  caucvgprprlemloc  7763  suplocexprlemmu  7778  suplocexprlemdisj  7780  mulcmpblnrlemg  7800  caucvgsrlemgt1  7855  axarch  7951  axcaucvglemres  7959  cnegexlem2  8195  mulge0  8638  divdivap1  8742  divdivap2  8743  conjmulap  8748  ltdivmul  8895  nn0ge0div  9404  peano2uz2  9424  peano5uzti  9425  eluzp1m1  9616  xleadd1a  9939  iooshf  10018  divelunit  10068  eluzgtdifelfzo  10264  ioom  10329  modqcyc2  10431  modaddmodup  10458  uzennn  10507  seq3fveq2  10546  seqfveq2g  10548  seq3id2  10597  seqfeq3  10600  expineg2  10619  mulexpzap  10650  leexp2r  10664  expnlbnd2  10736  hashfacen  10907  wrdred1hash  10957  resqrexlemp1rp  11150  resqrexlemfp1  11153  negfi  11371  climcaucn  11494  fsum3cvg3  11539  fsum2dlemstep  11577  mptfzshft  11585  expcnvre  11646  fprodrev  11762  fprod2dlemstep  11765  moddvds  11942  dvdsflip  11993  addmodlteqALT  12001  nn0o  12048  zsupcllemex  12083  dfgcd2  12151  lcmgcdlem  12215  cncongr1  12241  prmind2  12258  isprm5lem  12279  isprm6  12285  cncongrprm  12295  oddpwdclemdc  12311  sqrt2irrap  12318  hashdvds  12359  crth  12362  prmdiveq  12374  hashgcdlem  12376  hashgcdeq  12377  pclem0  12424  pclemub  12425  pcprendvds2  12429  pcmul  12439  pcexp  12447  pcneg  12463  pc2dvds  12468  pcmpt  12481  prmpwdvds  12493  pockthg  12495  1arith  12505  4sqlem2  12527  4sqlemafi  12533  4sqlem11  12539  ennnfonelemex  12571  setscom  12658  subsubm  13055  insubm  13057  isgrpinv  13126  subsubg  13267  subsubrng  13710  subsubrg  13741  islss4  13878  znf1o  14139  znidomb  14146  tgcl  14232  lmbr2  14382  txcn  14443  txdis1cn  14446  txlm  14447  hmeoimaf1o  14482  txhmeo  14487  bl2in  14571  blssps  14595  blss  14596  blssexps  14597  blssex  14598  bdxmet  14669  xmetxp  14675  xmetxpbl  14676  xmettx  14678  metcnp3  14679  metcnpi3  14685  dedekindicc  14787  ivthdichlem  14805  limcimolemlt  14818  rprelogbmul  15087  logbgcd1irr  15099  lgsne0  15154  gausslemma2dlem1a  15174  lgseisenlem2  15187  lgsquadlem1  15191  2sqlem8  15210  qdencn  15517  trilpolemlt1  15531