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

Theorem adantrd 468
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 457 . 2  |-  ( ( ps  /\  th )  ->  ps )
2 adantrd.1 . 2  |-  ( ph  ->  ( ps  ->  ch ) )
31, 2syl5 32 1  |-  ( ph  ->  ( ( ps  /\  th )  ->  ch )
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369
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 185  df-an 371
This theorem is referenced by:  syldan  470  jaoa  510  prlem1  962  cad0  1455  19.40b  1685  2eu3  2365  unineq  3733  dfopif  4199  axsep  4557  elssabg  4592  tz7.7  4894  oneqmini  4919  suctr  4951  exopxfr2  5137  fvun1  5929  fconst5  6113  fconstfvOLD  6119  isomin  6218  isofrlem  6221  poxp  6897  tposfo2  6980  onfununi  7014  tfrlem9a  7057  oecl  7189  oawordri  7201  omwordri  7223  odi  7230  pssnn  7740  prdom2  8387  acni2  8430  cardinfima  8481  cfslb2n  8651  infpssrlem4  8689  axdc3lem4  8836  brdom6disj  8913  tskr1om  9148  indpi  9288  1idpr  9410  1re  9598  mulge0  10077  infm3  10509  uzind  10961  suprfinzcl  10984  uzwo  11154  uzwoOLD  11155  xrlttr  11356  xmullem2  11467  snunico  11657  fzen  11713  fz0fzelfz0  11790  sqlecan  12255  hashf1lem2  12486  lo1le  13455  fsumss  13528  ntrivcvgfvn0  13689  fprodss  13736  smupvallem  14114  exprmfct  14232  infpnlem1  14409  prmlem0  14572  sscfn2  15168  isssc  15170  dirge  15845  efgval  16713  dmdprd  17007  dprdw  17021  dprdwOLD  17028  lpigen  17882  psrbaglefi  18001  psrbaglefiOLD  18002  matvscl  18910  scmatghm  19012  slesolinv  19159  cpmatacl  19194  pnfnei  19698  mnfnei  19699  cmpcld  19879  isfildlem  20335  metrest  21004  blval2  21055  iscmet3lem2  21708  ivthlem3  21842  mbfi1fseqlem4  22102  itg2seq  22126  dvres  22292  aalioulem6  22709  chpchtsum  23470  dchrmulcl  23500  bcmono  23528  brbtwn2  24184  axeuclid  24242  usgraedgprv  24352  usgranloopv  24354  4cycl4dv  24643  0clwlk  24741  wwlkext2clwwlk  24779  frg2wot1  25033  elghomlem2OLD  25340  rngo2  25366  shsvs  26217  cnlnssadj  26975  atexch  27276  mdsymlem5  27302  disjxpin  27423  sigaclci  28109  poseq  29308  nocvxminlem  29425  nofulllem5  29441  elfuns  29540  altopth1  29590  btwnexch2  29648  ifscgr  29669  colinbtwnle  29743  cnambfre  30038  itg2addnclem2  30042  itg2addnc  30044  areacirclem1  30082  trer  30109  elicc3  30110  heiborlem4  30285  ispridl2  30410  ispridlc  30442  eldiophss  30683  rencldnfilem  30729  ioounsn  31153  lcmgcdlem  31188  lcmdvds  31190  2reu3  32031  rhmsubclem4  32630  ax6e2ndeq  33065  suctrALT2  33370  bj-dfif5ALT  33897  bj-axsep  34127  bj-finsumval0  34403  paddasslem14  35297  ispsubcl2N  35411  cdleme29ex  35840  cdlemefr29exN  35868
  Copyright terms: Public domain W3C validator