Theorem adantrd 484

Description: Deduction adding a conjunct to the right of an antecedent. (Contributed by NM, 4-May-1994.)

Hypothesis

Ref	Expression
adantrd.1	|- ( ph -> ( ps -> ch ) )

Assertion

Ref	Expression
adantrd	|- ( ph -> ( ( ps /\ th ) -> ch ) )

Proof of Theorem adantrd

Step	Hyp	Ref	Expression
1		simpl 473	. 2 |- ( ( ps /\ th ) -> ps )
2		adantrd.1	. 2 |- ( ph -> ( ps -> ch ) )
3	1, 2	syl5 34	1 |- ( ph -> ( ( ps /\ th ) -> ch ) )

Syntax hints:   -> wi 4   /\ wa 384

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 197  df-an 386

This theorem is referenced by:  syldan  487  jaoa  532  prlem1  1005  cad0  1556  2eu3  2555  unineq  3877  dfopif  4399  axsep  4780  elssabg  4819  exopxfr2  5266  tz7.7  5749  oneqmini  5776  suctrOLD  5809  fvun1  6269  fconst5  6471  fpropnf1  6524  isomin  6587  isofrlem  6590  poxp  7289  tposfo2  7375  onfununi  7438  tfrlem9a  7482  oecl  7617  oawordri  7630  omwordri  7652  odi  7659  pssnn  8178  prdom2  8829  acni2  8869  cardinfima  8920  cfslb2n  9090  infpssrlem4  9128  axdc3lem4  9275  brdom6disj  9354  tskr1om  9589  indpi  9729  1idpr  9851  1re  10039  mulge0  10546  infm3  10982  uzind  11469  suprfinzcl  11492  uzwo  11751  xrlttr  11973  xmullem2  12095  snunico  12299  fzen  12358  fz0fzelfz0  12445  sqlecan  12971  hashf1lem2  13240  lo1le  14382  fsumss  14456  ntrivcvgfvn0  14631  fprodss  14678  smupvallem  15205  zeqzmulgcd  15232  lcmgcdlem  15319  lcmdvds  15321  lcmfunsnlem2lem1  15351  coprmproddvdslem  15376  cncongr2  15382  exprmfct  15416  infpnlem1  15614  prmdvdsprmop  15747  prmgaplem7  15761  prmlem0  15812  sscfn2  16478  isssc  16480  iszeroi  16659  funcsetcestrclem8  16802  dirge  17237  efgval  18130  dmdprd  18397  dprdw  18409  ringadd2  18575  lpigen  19256  psrbaglefi  19372  matvscl  20237  scmatghm  20339  slesolinv  20486  cpmatacl  20521  pnfnei  21024  mnfnei  21025  cmpcld  21205  isfildlem  21661  metrest  22329  blval2  22367  iscmet3lem2  23090  ivthlem3  23222  mbfi1fseqlem4  23485  itg2seq  23509  dvres  23675  aalioulem6  24092  chpchtsum  24944  dchrmulcl  24974  bcmono  25002  cgrg3col4  25734  brbtwn2  25785  axeuclid  25843  umgredg  26033  pthdivtx  26625  pthdlem1  26662  wwlksext2clwwlk  26924  clwlksfoclwwlk  26963  shsvs  28182  cnlnssadj  28939  atexch  29240  mdsymlem5  29266  disjxpin  29401  sigaclci  30195  poseq  31750  nosupno  31849  nosupbday  31851  nocvxminlem  31893  elfuns  32022  altopth1  32072  btwnexch2  32130  ifscgr  32151  colinbtwnle  32225  trer  32310  elicc3  32311  bj-axsep  32793  bj-finsumval0  33147  poimirlem27  33436  poimir  33442  cnambfre  33458  itg2addnclem2  33462  itg2addnc  33464  areacirclem1  33500  heiborlem4  33613  elghomlem2OLD  33685  rngo2  33706  ispridl2  33837  ispridlc  33869  iss2  34112  paddasslem14  35119  ispsubcl2N  35233  cdleme29ex  35662  cdlemefr29exN  35690  eldiophss  37338  rencldnfilem  37384  ioounsn  37795  clsk1indlem3  38341  ntrneikb  38392  ax6e2ndeq  38775  suctrALT2  39072  2reu3  41188  iccpartiltu  41358  bgoldbtbndlem2  41694  rhmsubclem4  42089  elsetrecslem  42444  aacllem  42547