Theorem ad2antrl 481

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  520  simprll  526  simprlr  527  elxp5  5027  f1oprg  5411  cnvf1olem  6121  tfrcl  6261  nnaordi  6404  swoer  6457  0er  6463  mapxpen  6742  fict  6762  dif1enen  6774  php5fin  6776  fin0  6779  fin0or  6780  diffisn  6787  infnfi  6789  unsnfi  6807  fidcenumlemrk  6842  sbthlemi8  6852  fiuni  6866  supmoti  6880  eldju2ndl  6957  eldju2ndr  6958  omp1eomlem  6979  difinfsnlem  6984  ctmlemr  6993  exmidfodomrlemr  7058  exmidfodomrlemrALT  7059  enq0sym  7240  nqnq0pi  7246  addlocpr  7344  nqprl  7359  addnqprlemrl  7365  addnqprlemru  7366  mulnqprlemrl  7381  mulnqprlemru  7382  archpr  7451  cauappcvgprlemloc  7460  cauappcvgprlemladdfl  7463  archrecpr  7472  caucvgprlemdisj  7482  caucvgprlemloc  7483  caucvgprprlemml  7502  caucvgprprlemopl  7505  caucvgprprlemdisj  7510  caucvgprprlemloc  7511  suplocexprlemmu  7526  suplocexprlemdisj  7528  mulcmpblnrlemg  7548  caucvgsrlemgt1  7603  axarch  7699  axcaucvglemres  7707  cnegexlem2  7938  mulge0  8381  divdivap1  8483  divdivap2  8484  conjmulap  8489  ltdivmul  8634  nn0ge0div  9138  peano2uz2  9158  peano5uzti  9159  eluzp1m1  9349  xleadd1a  9656  iooshf  9735  divelunit  9785  eluzgtdifelfzo  9974  ioom  10038  modqcyc2  10133  modaddmodup  10160  uzennn  10209  seq3fveq2  10242  seq3id2  10282  seqfeq3  10285  expineg2  10302  mulexpzap  10333  leexp2r  10347  expnlbnd2  10417  hashfacen  10579  resqrexlemp1rp  10778  resqrexlemfp1  10781  negfi  10999  climcaucn  11120  fsum3cvg3  11165  fsum2dlemstep  11203  mptfzshft  11211  expcnvre  11272  moddvds  11502  dvdsflip  11549  addmodlteqALT  11557  nn0o  11604  zsupcllemex  11639  dfgcd2  11702  lcmgcdlem  11758  cncongr1  11784  prmind2  11801  isprm6  11825  cncongrprm  11835  oddpwdclemdc  11851  sqrt2irrap  11858  hashdvds  11897  crth  11900  hashgcdlem  11903  hashgcdeq  11904  ennnfonelemex  11927  setscom  11999  tgcl  12233  lmbr2  12383  txcn  12444  txdis1cn  12447  txlm  12448  hmeoimaf1o  12483  txhmeo  12488  bl2in  12572  blssps  12596  blss  12597  blssexps  12598  blssex  12599  bdxmet  12670  xmetxp  12676  xmetxpbl  12677  xmettx  12679  metcnp3  12680  metcnpi3  12686  dedekindicc  12780  limcimolemlt  12802  qdencn  13222  trilpolemlt1  13234