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

Theorem adantrd 466
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 455 . 2  |-  ( ( ps  /\  th )  ->  ps )
2 adantrd.1 . 2  |-  ( ph  ->  ( ps  ->  ch ) )
31, 2syl5 30 1  |-  ( ph  ->  ( ( ps  /\  th )  ->  ch )
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 367
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 369
This theorem is referenced by:  syldan  468  jaoa  508  prlem1  963  cad0  1486  19.40b  1719  2eu3  2330  unineq  3699  dfopif  4155  axsep  4515  elssabg  4548  exopxfr2  4967  tz7.7  5435  oneqmini  5460  suctr  5492  fvun1  5919  fconst5  6108  fconstfvOLD  6114  isomin  6215  isofrlem  6218  poxp  6895  tposfo2  6980  onfununi  7044  tfrlem9a  7088  oecl  7223  oawordri  7235  omwordri  7257  odi  7264  pssnn  7772  prdom2  8415  acni2  8458  cardinfima  8509  cfslb2n  8679  infpssrlem4  8717  axdc3lem4  8864  brdom6disj  8941  tskr1om  9174  indpi  9314  1idpr  9436  1re  9624  mulge0  10110  infm3  10541  uzind  10994  suprfinzcl  11017  uzwo  11189  xrlttr  11398  xmullem2  11509  snunico  11699  fzen  11755  fz0fzelfz0  11833  sqlecan  12317  hashf1lem2  12552  lo1le  13621  fsumss  13694  ntrivcvgfvn0  13858  fprodss  13905  smupvallem  14340  exprmfct  14458  infpnlem1  14635  prmlem0  14798  sscfn2  15429  isssc  15431  iszeroi  15610  funcsetcestrclem8  15753  dirge  16189  efgval  17057  dmdprd  17347  dprdw  17361  dprdwOLD  17368  lpigen  18222  psrbaglefi  18341  psrbaglefiOLD  18342  matvscl  19223  scmatghm  19325  slesolinv  19472  cpmatacl  19507  pnfnei  20012  mnfnei  20013  cmpcld  20193  isfildlem  20648  metrest  21317  blval2  21368  iscmet3lem2  22021  ivthlem3  22155  mbfi1fseqlem4  22415  itg2seq  22439  dvres  22605  aalioulem6  23023  chpchtsum  23873  dchrmulcl  23903  bcmono  23931  brbtwn2  24612  axeuclid  24670  usgraedgprv  24780  usgranloopv  24782  4cycl4dv  25071  0clwlk  25169  wwlkext2clwwlk  25207  frg2wot1  25461  elghomlem2OLD  25764  rngo2  25790  shsvs  26641  cnlnssadj  27398  atexch  27699  mdsymlem5  27725  disjxpin  27866  sigaclci  28566  poseq  30051  nocvxminlem  30137  nofulllem5  30153  elfuns  30240  altopth1  30290  btwnexch2  30348  ifscgr  30369  colinbtwnle  30443  trer  30531  elicc3  30532  bj-axsep  30930  bj-finsumval0  31214  cnambfre  31415  itg2addnclem2  31420  itg2addnc  31422  areacirclem1  31458  heiborlem4  31572  ispridl2  31697  ispridlc  31729  paddasslem14  32830  ispsubcl2N  32944  cdleme29ex  33373  cdlemefr29exN  33401  eldiophss  35049  rencldnfilem  35095  ioounsn  35521  lcmgcdlem  36040  lcmdvds  36042  ax6e2ndeq  36336  suctrALT2  36647  2reu3  37542  iccpartiltu  37670  bgoldbtbndlem2  37835  rhmsubclem4  38389  aacllem  38841
  Copyright terms: Public domain W3C validator