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  5091  f1oprg  5475  cnvf1olem  6188  tfrcl  6328  nnaordi  6472  swoer  6525  0er  6531  mapxpen  6810  fict  6830  dif1enen  6842  php5fin  6844  fin0  6847  fin0or  6848  diffisn  6855  infnfi  6857  unsnfi  6880  fidcenumlemrk  6915  sbthlemi8  6925  fiuni  6939  supmoti  6954  eldju2ndl  7033  eldju2ndr  7034  omp1eomlem  7055  difinfsnlem  7060  ctmlemr  7069  exmidfodomrlemr  7154  exmidfodomrlemrALT  7155  enq0sym  7369  nqnq0pi  7375  addlocpr  7473  nqprl  7488  addnqprlemrl  7494  addnqprlemru  7495  mulnqprlemrl  7510  mulnqprlemru  7511  archpr  7580  cauappcvgprlemloc  7589  cauappcvgprlemladdfl  7592  archrecpr  7601  caucvgprlemdisj  7611  caucvgprlemloc  7612  caucvgprprlemml  7631  caucvgprprlemopl  7634  caucvgprprlemdisj  7639  caucvgprprlemloc  7640  suplocexprlemmu  7655  suplocexprlemdisj  7657  mulcmpblnrlemg  7677  caucvgsrlemgt1  7732  axarch  7828  axcaucvglemres  7836  cnegexlem2  8070  mulge0  8513  divdivap1  8615  divdivap2  8616  conjmulap  8621  ltdivmul  8767  nn0ge0div  9274  peano2uz2  9294  peano5uzti  9295  eluzp1m1  9485  xleadd1a  9805  iooshf  9884  divelunit  9934  eluzgtdifelfzo  10128  ioom  10192  modqcyc2  10291  modaddmodup  10318  uzennn  10367  seq3fveq2  10400  seq3id2  10440  seqfeq3  10443  expineg2  10460  mulexpzap  10491  leexp2r  10505  expnlbnd2  10576  hashfacen  10745  resqrexlemp1rp  10944  resqrexlemfp1  10947  negfi  11165  climcaucn  11288  fsum3cvg3  11333  fsum2dlemstep  11371  mptfzshft  11379  expcnvre  11440  fprodrev  11556  fprod2dlemstep  11559  moddvds  11735  dvdsflip  11785  addmodlteqALT  11793  nn0o  11840  zsupcllemex  11875  dfgcd2  11943  lcmgcdlem  12005  cncongr1  12031  prmind2  12048  isprm5lem  12069  isprm6  12075  cncongrprm  12085  oddpwdclemdc  12101  sqrt2irrap  12108  hashdvds  12149  crth  12152  prmdiveq  12164  hashgcdlem  12166  hashgcdeq  12167  pclem0  12214  pclemub  12215  pcprendvds2  12219  pcmul  12229  pcexp  12237  pcneg  12252  pc2dvds  12257  pcmpt  12269  prmpwdvds  12281  pockthg  12283  1arith  12293  4sqlem2  12315  ennnfonelemex  12343  setscom  12430  tgcl  12664  lmbr2  12814  txcn  12875  txdis1cn  12878  txlm  12879  hmeoimaf1o  12914  txhmeo  12919  bl2in  13003  blssps  13027  blss  13028  blssexps  13029  blssex  13030  bdxmet  13101  xmetxp  13107  xmetxpbl  13108  xmettx  13110  metcnp3  13111  metcnpi3  13117  dedekindicc  13211  limcimolemlt  13233  rprelogbmul  13473  logbgcd1irr  13485  lgsne0  13539  2sqlem8  13559  qdencn  13866  trilpolemlt1  13880