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

Theorem adantld 494
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 488 . 2 ((𝜃𝜓) → 𝜓)
2 adantld.1 . 2 (𝜑 → (𝜓𝜒))
31, 2syl5 34 1 (𝜑 → ((𝜃𝜓) → 𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 399
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 210  df-an 400
This theorem is referenced by:  im2anan9  622  jaoa  953  dedlema  1041  dedlemb  1042  prlem1  1050  dfsb1  2499  elneeldif  3895  unineq  4204  2nreu  4349  3elpr2eq  4799  tz7.7  6185  ordsssuc2  6247  fpropnf1  7003  nnsuc  7577  releldmdifi  7726  el2mpocsbcl  7763  poxp  7805  suppimacnv  7824  ressuppss  7832  imacosuppOLD  7858  onnseq  7964  tz7.49  8064  oaass  8170  omordi  8175  nnmordi  8240  eroprf  8378  xpdom2  8595  infsupprpr  8952  inf3lem2  9076  trcl  9154  r1pwss  9197  cardaleph  9500  dfac2b  9541  axcc4  9850  acncc  9851  zorn2lem7  9913  iundom2g  9951  cfpwsdom  9995  grothomex  10240  ltexprlem2  10448  1re  10630  00id  10804  mulge0  11147  nn0ge2m1nn  11952  zle0orge1  11986  xrlttr  12521  xmullem2  12646  snunioo  12856  fzen  12919  eluzgtdifelfzo  13094  ssfzo12bi  13127  modirr  13305  hash2pr  13823  hash3tr  13844  cshf1  14163  cshweqrep  14174  limsupbnd2  14832  climrlim2  14896  climuni  14901  mulcn2  14944  serf0  15029  cvgcmp  15163  ntrivcvg  15245  smuval2  15821  dfgcd2  15884  lcmgcdlem  15940  lcmdvds  15942  lcmf  15967  qnumdencl  16069  infpnlem1  16236  ram0  16348  prmgaplem6  16382  prmgaplem7  16383  prmlem1  16433  prmlem2  16445  setsstruct  16515  catass  16949  inveq  17036  sscfn1  17079  catsubcat  17101  subccocl  17107  funcco  17133  initoeu2  17268  funcestrcsetclem8  17389  funcsetcestrclem8  17404  gsmsymgrfixlem1  18547  psgnran  18635  efgi  18837  efgi2  18843  cntzcmnss  18954  telgsumfzs  19102  dprddisj2  19154  prmirredlem  20186  psgnghm  20269  scmatghm  21138  cpmatacl  21321  pm2mpf1  21404  fvmptnn04if  21454  lmcls  21907  isfild  22463  flffbas  22600  cnpflf2  22605  qustgplem  22726  tngngp3  23262  reperflem  23423  nmhmcn  23725  iscau2  23881  iscmet3lem2  23896  ivthlem2  24056  ovolmge0  24081  itg2seq  24346  limciun  24497  dvres  24514  dveflem  24582  lhop1  24617  ftc1lem6  24644  mdegnn0cl  24672  aalioulem6  24933  lgsqrmod  25936  gausslemma2dlem3  25952  2sqreulem1  26030  2sqreunnlem1  26033  2sqreulem3  26037  pntlem3  26193  axlowdimlem16  26751  axcontlem12  26769  umgrislfupgrlem  26915  uhgr2edg  26998  ushgredgedg  27019  ushgredgedgloop  27021  nbuhgr2vtx1edgb  27142  edgnbusgreu  27157  usgredgsscusgredg  27249  wlkdlem2  27473  pthdivtx  27518  upgrwlkdvdelem  27525  spthonepeq  27541  pthdlem1  27555  wwlksnprcl  27625  wlknewwlksn  27673  clwlkclwwlklem2a4  27782  clwlkclwwlklem2  27785  clwwlkwwlksb  27839  clwwlknun  27897  uhgr3cyclexlem  27966  eucrctshift  28028  frgrncvvdeqlem2  28085  frgrncvvdeqlem9  28092  numclwwlk1lem2foa  28139  numclwwlk1lem2f1  28142  ubthlem2  28654  shsvs  29106  mdsl2i  30105  mdsl2bi  30106  mdslmd1lem1  30108  atss  30129  chcv1  30138  chrelat2i  30148  atexch  30164  cdj3lem1  30217  bian1d  30230  disjxpin  30351  fpwrelmap  30495  nn0min  30562  sigaclci  31501  dya2iocuni  31651  omssubadd  31668  hashfundm  32464  fnrelpredd  32472  umgr2cycllem  32500  subfacp1lem6  32545  fmlasuc  32746  satffunlem  32761  satffunlem1lem1  32762  satffunlem2lem1  32764  mthmblem  32940  dfon2lem6  33146  dfrdg4  33525  altopth2  33540  cgrtriv  33576  cgrextend  33582  lineext  33650  btwnconn1  33675  colinbtwnle  33692  trer  33777  elicc3  33778  poimirlem27  35084  poimirlem29  35086  poimir  35090  itg2addnc  35111  ftc1cnnc  35129  areacirclem1  35145  prnc  35505  ispridlc  35508  lcvexchlem4  36333  lcvexchlem5  36334  lkrss2N  36465  cvrnbtwn  36567  hlrelat2  36699  atle  36732  lvolex3N  36834  lplnnlelln  36839  llncvrlpln2  36853  lvolnlelln  36880  lvolnlelpln  36881  lplncvrlvol2  36911  snatpsubN  37046  linepsubN  37048  pmodlem2  37143  linepsubclN  37247  dihatexv  38634  eldioph2b  39702  pell1234qrreccl  39793  islssfg2  40013  hbtlem2  40066  clss2lem  40309  clsk1indlem3  40744  mnuop3d  40977  sspwtrALT2  41527  2reu3  43664  2reu8i  43667  elsetpreimafvbi  43906  iccpartres  43933  iccpartiltu  43937  icceuelpart  43951  sprsymrelfvlem  44005  prpair  44016  prproropf1olem4  44021  prprelb  44031  goldbachthlem2  44061  lighneallem4  44126  requad2  44139  sbgoldbwt  44293  sbgoldbst  44294  nnsum4primesoddALTV  44313  nnsum4primeseven  44316  nnsum4primesevenALTV  44317  bgoldbtbndlem2  44322  mgmpropd  44393  rnghmsubcsetclem2  44598  funcrngcsetc  44620  rhmsubcsetclem2  44644  rhmsubcrngclem2  44650  funcringcsetc  44657  srhmsubc  44698  rhmsubclem4  44711  srhmsubcALTV  44716  rhmsubcALTVlem4  44729  ztprmneprm  44747  pgrpgt2nabl  44766  snlindsntor  44878  elbigo2  44964  eenglngeehlnm  45151  itschlc0yqe  45172  itscnhlc0xyqsol  45177  itsclc0  45183  itsclquadeu  45189
  Copyright terms: Public domain W3C validator