MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  adantrd 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
Assertion
Ref Expression
adantrd

Proof of Theorem adantrd
StepHypRef Expression
1 simpl 457 . 2
2 adantrd.1 . 2
31, 2syl5 32 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  /\wa 369
This theorem is referenced by:  syldan  470  jaoa  510  prlem1  962  cad0  1467  19.40b  1698  2eu3  2379  unineq  3747  dfopif  4214  axsep  4572  elssabg  4607  tz7.7  4909  oneqmini  4934  suctr  4966  exopxfr2  5152  fvun1  5944  fconst5  6128  fconstfvOLD  6134  isomin  6233  isofrlem  6236  poxp  6912  tposfo2  6997  onfununi  7031  tfrlem9a  7074  oecl  7206  oawordri  7218  omwordri  7240  odi  7247  pssnn  7758  prdom2  8405  acni2  8448  cardinfima  8499  cfslb2n  8669  infpssrlem4  8707  axdc3lem4  8854  brdom6disj  8931  tskr1om  9166  indpi  9306  1idpr  9428  1re  9616  mulge0  10095  infm3  10527  uzind  10979  suprfinzcl  11003  uzwo  11173  uzwoOLD  11174  xrlttr  11375  xmullem2  11486  snunico  11676  fzen  11732  fz0fzelfz0  11809  sqlecan  12274  hashf1lem2  12505  lo1le  13474  fsumss  13547  ntrivcvgfvn0  13708  fprodss  13755  smupvallem  14133  exprmfct  14251  infpnlem1  14428  prmlem0  14591  sscfn2  15187  isssc  15189  dirge  15867  efgval  16735  dmdprd  17029  dprdw  17043  dprdwOLD  17050  lpigen  17904  psrbaglefi  18023  psrbaglefiOLD  18024  matvscl  18933  scmatghm  19035  slesolinv  19182  cpmatacl  19217  pnfnei  19721  mnfnei  19722  cmpcld  19902  isfildlem  20358  metrest  21027  blval2  21078  iscmet3lem2  21731  ivthlem3  21865  mbfi1fseqlem4  22125  itg2seq  22149  dvres  22315  aalioulem6  22733  chpchtsum  23494  dchrmulcl  23524  bcmono  23552  brbtwn2  24208  axeuclid  24266  usgraedgprv  24376  usgranloopv  24378  4cycl4dv  24667  0clwlk  24765  wwlkext2clwwlk  24803  frg2wot1  25057  elghomlem2OLD  25364  rngo2  25390  shsvs  26241  cnlnssadj  26999  atexch  27300  mdsymlem5  27326  disjxpin  27447  sigaclci  28132  poseq  29333  nocvxminlem  29450  nofulllem5  29466  elfuns  29565  altopth1  29615  btwnexch2  29673  ifscgr  29694  colinbtwnle  29768  cnambfre  30063  itg2addnclem2  30067  itg2addnc  30069  areacirclem1  30107  trer  30134  elicc3  30135  heiborlem4  30310  ispridl2  30435  ispridlc  30467  eldiophss  30708  rencldnfilem  30754  ioounsn  31177  lcmgcdlem  31212  lcmdvds  31214  2reu3  32193  iszeroi  32615  funcsetcestrclem8  32668  rhmsubclem4  32897  aacllem  33216  ax6e2ndeq  33332  suctrALT2  33637  bj-axsep  34379  bj-finsumval0  34663  paddasslem14  35557  ispsubcl2N  35671  cdleme29ex  36100  cdlemefr29exN  36128
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
  Copyright terms: Public domain W3C validator