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

Theorem adantld 480
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 473 . 2 ((𝜃𝜓) → 𝜓)
2 adantld.1 . 2 (𝜑 → (𝜓𝜒))
31, 2syl5 34 1 (𝜑 → ((𝜃𝜓) → 𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384
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 198  df-an 385
This theorem is referenced by:  jaoa  969  dedlema  1059  dedlemb  1060  prlem1  1070  2eu3  2719  unineq  4076  3elpr2eq  4625  tz7.7  5959  ordsssuc2  6024  fpropnf1  6745  nnsuc  7309  el2mpt2csbcl  7480  poxp  7520  suppimacnv  7537  ressuppss  7545  imacosupp  7567  onnseq  7674  tz7.49  7773  oaass  7875  omordi  7880  nnmordi  7945  eroprf  8078  xpdom2  8291  inf3lem2  8770  trcl  8848  r1pwss  8891  cardaleph  9192  dfac2b  9233  dfac2OLD  9235  axcc4  9543  acncc  9544  zorn2lem7  9606  iundom2g  9644  cfpwsdom  9688  grothomex  9933  ltexprlem2  10141  1re  10322  00id  10493  mulge0  10828  nn0ge2m1nn  11622  xrlttr  12185  xmullem2  12309  snunioo  12517  fzen  12577  eluzgtdifelfzo  12750  ssfzo12bi  12783  modirr  12961  hash2pr  13464  hash3tr  13485  cshf1  13776  cshweqrep  13787  limsupbnd2  14433  climrlim2  14497  climuni  14502  mulcn2  14545  serf0  14630  cvgcmp  14766  ntrivcvg  14846  smuval2  15419  dfgcd2  15478  lcmgcdlem  15534  lcmdvds  15536  lcmf  15561  qnumdencl  15660  infpnlem1  15827  ram0  15939  prmgaplem6  15973  prmgaplem7  15974  prmlem1  16022  prmlem2  16034  setsstruct  16105  catass  16547  inveq  16634  sscfn1  16677  catsubcat  16699  subccocl  16705  funcco  16731  initoeu2  16866  funcestrcsetclem8  16988  funcsetcestrclem8  17003  gsmsymgrfixlem1  18044  psgnran  18132  efgi  18329  efgi2  18335  cntzcmnss  18443  telgsumfzs  18584  dprddisj2  18636  prmirredlem  20045  psgnghm  20129  scmatghm  20546  cpmatacl  20730  pm2mpf1  20813  fvmptnn04if  20863  lmcls  21316  isfild  21871  flffbas  22008  cnpflf2  22013  qustgplem  22133  tngngp3  22669  reperflem  22830  nmhmcn  23128  iscau2  23283  iscmet3lem2  23298  ivthlem2  23429  ovolmge0  23454  itg2seq  23719  limciun  23868  dveflem  23952  lhop1  23987  ftc1lem6  24014  mdegnn0cl  24041  aalioulem6  24302  lgsqrmod  25287  gausslemma2dlem3  25303  pntlem3  25508  axlowdimlem16  26047  axcontlem12  26065  umgrislfupgrlem  26227  uhgr2edg  26311  ushgredgedg  26332  ushgredgedgloop  26334  ushgredgedgloopOLD  26335  nbuhgr2vtx1edgb  26460  edgnbusgreu  26480  edgnbusgreuOLD  26481  usgredgsscusgredg  26579  wlkdlem2  26804  pthdivtx  26849  upgrwlkdvdelem  26856  spthonepeq  26872  pthdlem1  26886  wwlksnprcl  26956  wlknewwlksn  27010  clwlkclwwlklem2a4  27136  clwlkclwwlklem2  27139  clwwlkwwlksb  27200  clwwlknun  27277  clwwlknunOLD  27282  uhgr3cyclexlem  27350  eucrctshift  27412  frgrncvvdeqlem2  27471  frgrncvvdeqlem9  27478  numclwwlk1lem2foa  27529  numclwwlk1lem2f1  27532  ubthlem2  28052  shsvs  28507  mdsl2i  29506  mdsl2bi  29507  mdslmd1lem1  29509  atss  29530  chcv1  29539  chrelat2i  29549  atexch  29565  cdj3lem1  29618  bian1d  29631  disjxpin  29723  fpwrelmap  29832  nn0min  29891  sigaclci  30517  dya2iocuni  30667  omssubadd  30684  subfacp1lem6  31487  mthmblem  31797  dfon2lem6  32010  dfrdg4  32376  altopth2  32391  cgrtriv  32427  cgrextend  32433  lineext  32501  btwnconn1  32526  colinbtwnle  32543  trer  32628  elicc3  32629  poimirlem27  33746  poimirlem29  33748  poimir  33752  itg2addnc  33773  ftc1cnnc  33793  areacirclem1  33809  prnc  34174  ispridlc  34177  lcvexchlem4  34814  lcvexchlem5  34815  lkrss2N  34946  cvrnbtwn  35048  hlrelat2  35180  atle  35213  lvolex3N  35315  lplnnlelln  35320  llncvrlpln2  35334  lvolnlelln  35361  lvolnlelpln  35362  lplncvrlvol2  35392  snatpsubN  35527  linepsubN  35529  pmodlem2  35624  linepsubclN  35728  dihatexv  37116  eldioph2b  37825  pell1234qrreccl  37917  islssfg2  38139  hbtlem2  38192  clss2lem  38415  clsk1indlem3  38838  sspwtrALT2  39549  2reu3  41697  iccpartres  41926  iccpartiltu  41930  icceuelpart  41944  goldbachthlem2  42030  lighneallem4  42099  sbgoldbwt  42237  sbgoldbst  42238  nnsum4primesoddALTV  42257  nnsum4primeseven  42260  nnsum4primesevenALTV  42261  bgoldbtbndlem2  42266  sprsymrelfvlem  42305  mgmpropd  42340  rnghmsubcsetclem2  42541  funcrngcsetc  42563  rhmsubcsetclem2  42587  rhmsubcrngclem2  42593  funcringcsetc  42600  srhmsubc  42641  rhmsubclem4  42654  srhmsubcALTV  42659  rhmsubcALTVlem4  42672  ztprmneprm  42690  pgrpgt2nabl  42712  snlindsntor  42825  elbigo2  42911
  Copyright terms: Public domain W3C validator