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  1390  equveli  1928  2eu3  2225  unineq  3419  dfopif  3793  axsep  4140  elssabg  4166  tz7.7  4418  oneqmini  4443  suctr  4475  fvun1  5590  fconst5  5731  fconstfv  5734  isomin  5834  isofrlem  5837  exopxfr2  6184  poxp  6227  tposfo2  6257  onfununi  6358  tfrlem9a  6402  oecl  6536  oawordri  6548  omwordri  6570  odi  6577  pssnn  7081  prdom2  7636  acni2  7673  cardinfima  7724  cfslb2n  7894  infpssrlem4  7932  axdc3lem4  8079  brdom6disj  8157  tskr1om  8389  indpi  8531  1idpr  8653  1re  8837  mulge0  9291  infm3  9713  uzind  10103  uzwo  10281  uzwoOLD  10282  xrlttr  10474  xmullem2  10585  snunico  10763  fzen  10811  sqlecan  11209  hashf1lem2  11394  lo1le  12125  fsumss  12198  smupvallem  12674  exprmfct  12789  infpnlem1  12957  prmlem0  13107  sscfn2  13695  isssc  13697  dirge  14359  efgval  15026  dmdprd  15236  dprdw  15245  lpigen  16008  psrbaglefi  16118  pnfnei  16950  mnfnei  16951  cmpcld  17129  isfildlem  17552  metrest  18070  iscmet3lem2  18718  ivthlem3  18813  mbfi1fseqlem4  19073  itg2seq  19097  dvres  19261  aalioulem6  19717  chpchtsum  20458  dchrmulcl  20488  bcmono  20516  elghomlem2  21029  rngo2  21055  shsvs  21902  cnlnssadj  22660  atexch  22961  mdsymlem5  22987  sigaclci  23493  poseq  24253  nocvxminlem  24344  nofulllem5  24360  altopth1  24499  brbtwn2  24533  axeuclid  24591  btwnexch2  24646  ifscgr  24667  colinbtwnle  24741  areacirclem2  24925  ridlideq  25335  intcont  25543  limptlimpr2lem1  25574  islimrs3  25581  islimrs4  25582  distsava  25689  cmpmon  25815  iepiclem  25823  setiscat  25979  clscnc  26010  trer  26227  elicc3  26228  heiborlem4  26538  ispridl2  26663  ispridlc  26695  eldiophss  26854  rencldnfilem  26903  2reu3  27966  usgraedgprv  28122  a9e2ndeq  28325  suctrALT2  28613  paddasslem14  30022  ispsubcl2N  30136  cdleme29ex  30563  cdlemefr29exN  30591
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