MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  adantrd Unicode version

Theorem adantrd 454
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
StepHypRef Expression
1 simpl 443 . 2  |-  ( ( ps  /\  th )  ->  ps )
2 adantrd.1 . 2  |-  ( ph  ->  ( ps  ->  ch ) )
31, 2syl5 28 1  |-  ( ph  ->  ( ( ps  /\  th )  ->  ch )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358
This theorem is referenced by:  syldan  456  jaoa  496  prlem1  928  cad0  1391  equveli  1960  2eu3  2258  unineq  3453  dfopif  3830  axsep  4177  elssabg  4203  tz7.7  4455  oneqmini  4480  suctr  4512  fvun1  5628  fconst5  5770  fconstfv  5775  isomin  5876  isofrlem  5879  exopxfr2  6226  poxp  6269  tposfo2  6299  onfununi  6400  tfrlem9a  6444  oecl  6578  oawordri  6590  omwordri  6612  odi  6619  pssnn  7124  prdom2  7681  acni2  7718  cardinfima  7769  cfslb2n  7939  infpssrlem4  7977  axdc3lem4  8124  brdom6disj  8202  tskr1om  8434  indpi  8576  1idpr  8698  1re  8882  mulge0  9336  infm3  9758  uzind  10150  uzwo  10328  uzwoOLD  10329  xrlttr  10521  xmullem2  10632  snunico  10810  fzen  10858  sqlecan  11256  hashf1lem2  11441  lo1le  12172  fsumss  12245  smupvallem  12721  exprmfct  12836  infpnlem1  13004  prmlem0  13154  sscfn2  13744  isssc  13746  dirge  14408  efgval  15075  dmdprd  15285  dprdw  15294  lpigen  16057  psrbaglefi  16167  pnfnei  17006  mnfnei  17007  cmpcld  17185  isfildlem  17604  metrest  18122  iscmet3lem2  18771  ivthlem3  18866  mbfi1fseqlem4  19126  itg2seq  19150  dvres  19314  aalioulem6  19770  chpchtsum  20511  dchrmulcl  20541  bcmono  20569  elghomlem2  21082  rngo2  21108  shsvs  21957  cnlnssadj  22715  atexch  23016  mdsymlem5  23042  blval2  23506  sigaclci  23691  ntrivcvgfvn0  24404  fprodss  24451  poseq  24638  nocvxminlem  24729  nofulllem5  24745  altopth1  24885  brbtwn2  24919  axeuclid  24977  btwnexch2  25032  ifscgr  25053  colinbtwnle  25127  itg2addnclem2  25318  itg2addnc  25319  areacirclem2  25342  trer  25376  elicc3  25377  heiborlem4  25686  ispridl2  25811  ispridlc  25843  eldiophss  26002  rencldnfilem  26051  2reu3  27114  opabbrex  27248  usgraedgprv  27348  4cycl4dv  27551  a9e2ndeq  27819  suctrALT2  28124  equveliNEW7  28698  paddasslem14  29840  ispsubcl2N  29954  cdleme29ex  30381  cdlemefr29exN  30409
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 177  df-an 360
  Copyright terms: Public domain W3C validator