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  960  cad0  1452  2eu3  2389  unineq  3748  dfopif  4210  axsep  4567  elssabg  4602  tz7.7  4904  oneqmini  4929  suctr  4961  exopxfr2  5147  fvun1  5938  fconst5  6118  fconstfv  6123  isomin  6221  isofrlem  6224  opabbrex  6324  poxp  6895  tposfo2  6978  onfununi  7012  tfrlem9a  7055  oecl  7187  oawordri  7199  omwordri  7221  odi  7228  pssnn  7738  prdom2  8384  acni2  8427  cardinfima  8478  cfslb2n  8648  infpssrlem4  8686  axdc3lem4  8833  brdom6disj  8910  tskr1om  9145  indpi  9285  1idpr  9407  1re  9595  mulge0  10070  infm3  10502  uzind  10952  suprfinzcl  10975  uzwo  11144  uzwoOLD  11145  xrlttr  11346  xmullem2  11457  snunico  11647  fzen  11703  fz0fzelfz0  11778  sqlecan  12242  hashf1lem2  12471  lo1le  13437  fsumss  13510  smupvallem  13992  exprmfct  14110  infpnlem1  14287  prmlem0  14449  sscfn2  15048  isssc  15050  dirge  15724  efgval  16541  dmdprd  16832  dprdw  16846  dprdwOLD  16852  lpigen  17703  psrbaglefi  17822  psrbaglefiOLD  17823  matvscl  18728  scmatghm  18830  slesolinv  18977  cpmatacl  19012  pnfnei  19515  mnfnei  19516  cmpcld  19696  isfildlem  20121  metrest  20790  blval2  20841  iscmet3lem2  21494  ivthlem3  21628  mbfi1fseqlem4  21888  itg2seq  21912  dvres  22078  aalioulem6  22495  chpchtsum  23250  dchrmulcl  23280  bcmono  23308  brbtwn2  23912  axeuclid  23970  usgraedgprv  24080  usgranloopv  24082  4cycl4dv  24371  0clwlk  24469  wwlkext2clwwlk  24507  frg2wot1  24762  elghomlem2  25068  rngo2  25094  shsvs  25945  cnlnssadj  26703  atexch  27004  mdsymlem5  27030  disjxpin  27148  sigaclci  27800  ntrivcvgfvn0  28638  fprodss  28685  poseq  28938  nocvxminlem  29055  nofulllem5  29071  elfuns  29170  altopth1  29220  btwnexch2  29278  ifscgr  29299  colinbtwnle  29373  cnambfre  29668  itg2addnclem2  29672  itg2addnc  29674  areacirclem1  29712  trer  29739  elicc3  29740  heiborlem4  29941  ispridl2  30066  ispridlc  30098  eldiophss  30340  rencldnfilem  30386  ioounsn  30810  lcmgcdlem  30840  lcmdvds  30842  2reu3  31688  ax6e2ndeq  32430  suctrALT2  32735  bj-dfif5ALT  33248  bj-19.40b  33326  bj-axsep  33478  bj-finsumval0  33753  paddasslem14  34647  ispsubcl2N  34761  cdleme29ex  35188  cdlemefr29exN  35216
  Copyright terms: Public domain W3C validator