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

Theorem adantld 482
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 476 . 2 ((𝜃𝜓) → 𝜓)
2 adantld.1 . 2 (𝜑 → (𝜓𝜒))
31, 2syl5 34 1 (𝜑 → ((𝜃𝜓) → 𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383
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 197  df-an 385
This theorem is referenced by:  jaoa  531  dedlema  1014  dedlemb  1015  prlem1  1025  2eu3  2584  unineq  3910  3elpr2eq  4467  tz7.7  5787  ordsssuc2  5852  fpropnf1  6564  nnsuc  7124  el2mpt2csbcl  7295  poxp  7334  suppimacnv  7351  ressuppss  7359  imacosupp  7380  onnseq  7486  tz7.49  7585  oaass  7686  omordi  7691  nnmordi  7756  eroprf  7888  xpdom2  8096  inf3lem2  8564  trcl  8642  r1pwss  8685  cardaleph  8950  dfac2  8991  axcc4  9299  acncc  9300  zorn2lem7  9362  iundom2g  9400  cfpwsdom  9444  grothomex  9689  ltexprlem2  9897  1re  10077  00id  10249  mulge0  10584  nn0ge2m1nn  11398  xrlttr  12011  xmullem2  12133  snunioo  12336  fzen  12396  eluzgtdifelfzo  12569  ssfzo12bi  12603  modirr  12781  hash2pr  13289  hash3tr  13310  cshf1  13602  cshweqrep  13613  limsupbnd2  14258  climrlim2  14322  climuni  14327  mulcn2  14370  serf0  14455  cvgcmp  14592  ntrivcvg  14673  smuval2  15251  dfgcd2  15310  lcmgcdlem  15366  lcmdvds  15368  lcmf  15393  qnumdencl  15494  infpnlem1  15661  ram0  15773  prmgaplem6  15807  prmgaplem7  15808  prmlem1  15861  prmlem2  15874  setsstruct  15945  catass  16394  inveq  16481  sscfn1  16524  catsubcat  16546  subccocl  16552  funcco  16578  initoeu2  16713  funcestrcsetclem8  16834  funcsetcestrclem8  16849  gsmsymgrfixlem1  17893  psgnran  17981  efgi  18178  efgi2  18184  cntzcmnss  18292  telgsumfzs  18432  dprddisj2  18484  prmirredlem  19889  psgnghm  19974  scmatghm  20387  cpmatacl  20569  pm2mpf1  20652  fvmptnn04if  20702  lmcls  21154  isfild  21709  flffbas  21846  cnpflf2  21851  qustgplem  21971  tngngp3  22507  reperflem  22668  nmhmcn  22966  iscau2  23121  iscmet3lem2  23136  ivthlem2  23267  ovolmge0  23291  itg2seq  23554  limciun  23703  dveflem  23787  lhop1  23822  ftc1lem6  23849  mdegnn0cl  23876  aalioulem6  24137  lgsqrmod  25122  gausslemma2dlem3  25138  pntlem3  25343  axlowdimlem16  25882  axcontlem12  25900  umgrislfupgrlem  26062  uhgr2edg  26145  ushgredgedg  26166  ushgredgedgloop  26168  nbuhgr2vtx1edgb  26293  edgnbusgreu  26313  usgredgsscusgredg  26411  wlkdlem2  26636  pthdivtx  26681  upgrwlkdvdelem  26688  spthonepeq  26704  pthdlem1  26718  wwlksnprcl  26787  wlknewwlksn  26841  clwlkclwwlklem2a4  26963  clwlkclwwlklem2  26966  clwwlkwwlksb  27018  clwwlknun  27087  clwwlknunOLD  27091  uhgr3cyclexlem  27159  eucrctshift  27221  frgrncvvdeqlem2  27280  frgrncvvdeqlem9  27287  2clwwlk2clwwlklem2  27330  numclwlk1lem2foa  27344  numclwlk1lem2f1  27347  ubthlem2  27855  shsvs  28310  mdsl2i  29309  mdsl2bi  29310  mdslmd1lem1  29312  atss  29333  chcv1  29342  chrelat2i  29352  atexch  29368  cdj3lem1  29421  bian1d  29434  disjxpin  29527  fpwrelmap  29636  nn0min  29695  sigaclci  30323  dya2iocuni  30473  omssubadd  30490  subfacp1lem6  31293  mthmblem  31603  dfon2lem6  31817  dfrdg4  32183  altopth2  32198  cgrtriv  32234  cgrextend  32240  lineext  32308  btwnconn1  32333  colinbtwnle  32350  trer  32435  elicc3  32436  poimirlem27  33566  poimirlem29  33568  poimir  33572  itg2addnc  33594  ftc1cnnc  33614  areacirclem1  33630  prnc  33996  ispridlc  33999  lcvexchlem4  34642  lcvexchlem5  34643  lkrss2N  34774  cvrnbtwn  34876  hlrelat2  35007  atle  35040  lvolex3N  35142  lplnnlelln  35147  llncvrlpln2  35161  lvolnlelln  35188  lvolnlelpln  35189  lplncvrlvol2  35219  snatpsubN  35354  linepsubN  35356  pmodlem2  35451  linepsubclN  35555  dihatexv  36944  eldioph2b  37643  pell1234qrreccl  37735  islssfg2  37958  hbtlem2  38011  clss2lem  38235  clsk1indlem3  38658  sspwtrALT2  39372  2reu3  41509  iccpartres  41679  iccpartiltu  41683  icceuelpart  41697  goldbachthlem2  41783  lighneallem4  41852  sbgoldbwt  41990  sbgoldbst  41991  nnsum4primesoddALTV  42010  nnsum4primeseven  42013  nnsum4primesevenALTV  42014  bgoldbtbndlem2  42019  sprsymrelfvlem  42065  mgmpropd  42100  rnghmsubcsetclem2  42301  funcrngcsetc  42323  rhmsubcsetclem2  42347  rhmsubcrngclem2  42353  funcringcsetc  42360  srhmsubc  42401  rhmsubclem4  42414  srhmsubcALTV  42419  rhmsubcALTVlem4  42432  ztprmneprm  42450  pgrpgt2nabl  42472  snlindsntor  42585  elbigo2  42671
  Copyright terms: Public domain W3C validator