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

Theorem adantld 467
Description: Deduction adding a conjunct to the left of an antecedent. (Contributed by NM, 4-May-1994.) (Proof shortened by Wolf Lammen, 20-Dec-2012.)
Hypothesis
Ref Expression
adantld.1
Assertion
Ref Expression
adantld

Proof of Theorem adantld
StepHypRef Expression
1 simpr 461 . 2
2 adantld.1 . 2
31, 2syl5 32 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  /\wa 369
This theorem is referenced by:  jaoa  510  dedlema  954  dedlemb  955  prlem1  962  19.40b  1698  2eu3  2379  unineq  3747  tz7.7  4909  ordsssuc2  4971  nnsuc  6717  poxp  6912  suppimacnv  6929  ressuppss  6938  imacosupp  6959  onnseq  7034  tz7.49  7129  oaass  7229  omordi  7234  nnmordi  7299  eroprf  7428  xpdom2  7632  inf3lem2  8067  trcl  8180  r1pwss  8223  cardaleph  8491  dfac2  8532  axcc4  8840  acncc  8841  zorn2lem7  8903  iundom2g  8936  cfpwsdom  8980  grothomex  9228  ltexprlem2  9436  1re  9616  00id  9776  mulge0  10095  nn0ge2m1nn  10886  uzindOLD  10982  xrlttr  11375  xmullem2  11486  snunioo  11675  fzen  11732  eluzgtdifelfzo  11878  ssfzo12bi  11907  modirr  12057  hash2pr  12515  hash3tr  12529  cshweqrep  12789  limsupbnd2  13306  climrlim2  13370  climuni  13375  mulcn2  13418  serf0  13503  cvgcmp  13630  ntrivcvg  13706  smuval2  14132  qnumdencl  14272  infpnlem1  14428  ram0  14540  prmlem1  14593  prmlem2  14605  catass  15083  sscfn1  15186  catsubcat  15208  subccocl  15214  funcco  15240  gsmsymgrfixlem1  16452  psgnran  16540  efgi  16737  efgi2  16743  cntzcmnss  16849  telgsumfzs  17018  dprddisj2  17087  dprddisj2OLD  17088  prmirredlem  18523  prmirredlemOLD  18526  psgnghm  18616  scmatghm  19035  cpmatacl  19217  pm2mpf1  19300  fvmptnn04if  19350  lmcls  19803  isfild  20359  flffbas  20496  cnpflf2  20501  qustgplem  20619  reperflem  21323  nmhmcn  21603  iscau2  21716  iscmet3lem2  21731  ivthlem2  21864  ovolmge0  21888  itg2seq  22149  limciun  22298  dveflem  22380  lhop1  22415  ftc1lem6  22442  mdegnn0cl  22471  aalioulem6  22733  pntlem3  23794  axlowdimlem16  24260  axcontlem12  24278  usgraedgprv  24376  usgra2wlkspthlem2  24620  usgrcyclnl2  24641  nvnencycllem  24643  wlkv0  24760  clwlkisclwwlklem2a4  24784  clwlkisclwwlklem1  24787  2spontn0vne  24887  usg2spthonot0  24889  iseupa  24965  frgra3vlem1  25000  ubthlem2  25787  shsvs  26241  mdsl2i  27241  mdsl2bi  27242  mdslmd1lem1  27244  atss  27265  chcv1  27274  chrelat2i  27284  atexch  27300  cdj3lem1  27353  bian1d  27366  disjxpin  27447  fpwrelmap  27556  nn0min  27611  sigaclci  28132  dya2iocuni  28254  subfacp1lem6  28629  mthmblem  28940  dfon2lem6  29220  dfrdg4  29600  altopth2  29616  cgrtriv  29652  cgrextend  29658  lineext  29726  btwnconn1  29751  colinbtwnle  29768  itg2addnc  30069  ftc1cnnc  30089  areacirclem1  30107  trer  30134  elicc3  30135  prnc  30464  ispridlc  30467  eldioph2b  30696  pell1234qrreccl  30790  islssfg2  31017  hbtlem2  31073  lcmgcdlem  31212  lcmdvds  31214  2reu3  32193  usgvincvad  32404  usgvincvadALT  32407  mgmpropd  32463  inveq  32565  initoeu2  32622  funcestrcsetclem8  32653  funcsetcestrclem8  32668  rnghmsubcsetclem2  32784  funcrngcsetc  32806  rhmsubcsetclem2  32830  rhmsubcrngclem2  32836  funcringcsetc  32843  srhmsubc  32884  rhmsubclem4  32897  srhmsubcOLD  32903  rhmsubcOLDlem4  32916  ztprmneprm  32936  pgrpgt2nabl  32959  snlindsntor  33072  sspwtrALT2  33623  lcvexchlem4  34762  lcvexchlem5  34763  lkrss2N  34894  cvrnbtwn  34996  hlrelat2  35127  atle  35160  lvolex3N  35262  lplnnlelln  35267  llncvrlpln2  35281  lvolnlelln  35308  lvolnlelpln  35309  lplncvrlvol2  35339  snatpsubN  35474  linepsubN  35476  pmodlem2  35571  linepsubclN  35675  dihatexv  37065
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