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

Theorem adantrd 470
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 459 . 2  |-  ( ( ps  /\  th )  ->  ps )
2 adantrd.1 . 2  |-  ( ph  ->  ( ps  ->  ch ) )
31, 2syl5 33 1  |-  ( ph  ->  ( ( ps  /\  th )  ->  ch )
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 371
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 189  df-an 373
This theorem is referenced by:  syldan  473  jaoa  513  prlem1  974  cad0  1522  19.40bOLD  1753  2eu3  2386  unineq  3695  dfopif  4166  axsep  4527  elssabg  4561  exopxfr2  4982  tz7.7  5452  oneqmini  5477  suctr  5509  fvun1  5941  fconst5  6127  fconstfvOLD  6132  isomin  6233  isofrlem  6236  poxp  6913  tposfo2  7001  onfununi  7065  tfrlem9a  7109  oecl  7244  oawordri  7256  omwordri  7278  odi  7285  pssnn  7795  prdom2  8442  acni2  8482  cardinfima  8533  cfslb2n  8703  infpssrlem4  8741  axdc3lem4  8888  brdom6disj  8965  tskr1om  9197  indpi  9337  1idpr  9459  1re  9647  mulge0  10139  infm3  10575  uzind  11034  suprfinzcl  11057  uzwo  11229  xrlttr  11446  xmullem2  11558  snunico  11766  fzen  11823  fz0fzelfz0  11903  sqlecan  12388  hashf1lem2  12626  lo1le  13727  fsumss  13803  ntrivcvgfvn0  13967  fprodss  14014  smupvallem  14469  lcmgcdlem  14583  lcmdvds  14585  lcmfunsnlem2lem1  14623  exprmfct  14660  coprmproddvdslem  14691  infpnlem1  14866  prmdvdsprmop  15013  prmdvdsprmorpOLD  15028  prmgaplem7  15039  prmlem0  15089  sscfn2  15735  isssc  15737  iszeroi  15916  funcsetcestrclem8  16059  dirge  16495  efgval  17379  dmdprd  17642  dprdw  17654  lpigen  18492  psrbaglefi  18608  matvscl  19468  scmatghm  19570  slesolinv  19717  cpmatacl  19752  pnfnei  20248  mnfnei  20249  cmpcld  20429  isfildlem  20884  metrest  21551  blval2  21589  iscmet3lem2  22274  ivthlem3  22416  mbfi1fseqlem4  22688  itg2seq  22712  dvres  22878  aalioulem6  23305  chpchtsum  24159  dchrmulcl  24189  bcmono  24217  cgrg3col4  24896  brbtwn2  24947  axeuclid  25005  usgraedgprv  25115  usgranloopv  25117  4cycl4dv  25407  0clwlk  25505  wwlkext2clwwlk  25543  frg2wot1  25797  elghomlem2OLD  26102  rngo2  26128  shsvs  26988  cnlnssadj  27745  atexch  28046  mdsymlem5  28072  disjxpin  28210  sigaclci  28966  poseq  30503  nocvxminlem  30591  nofulllem5  30607  elfuns  30694  altopth1  30744  btwnexch2  30802  ifscgr  30823  colinbtwnle  30897  trer  30984  elicc3  30985  bj-axsep  31420  bj-finsumval0  31714  poimirlem27  31979  poimir  31985  cnambfre  32001  itg2addnclem2  32006  itg2addnc  32008  areacirclem1  32044  heiborlem4  32158  ispridl2  32283  ispridlc  32315  paddasslem14  33410  ispsubcl2N  33524  cdleme29ex  33953  cdlemefr29exN  33981  eldiophss  35629  rencldnfilem  35675  ioounsn  36106  ax6e2ndeq  36937  suctrALT2  37243  2reu3  38619  iccpartiltu  38746  bgoldbtbndlem2  38911  fpropnf1  39046  umgredg  39239  rhmsubclem4  40195  aacllem  40644
  Copyright terms: Public domain W3C validator