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

Theorem adantld 483
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 477 . 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 197  df-an 386
This theorem is referenced by:  jaoa  532  dedlema  1001  dedlemb  1002  prlem1  1004  2eu3  2554  unineq  3859  tz7.7  5718  ordsssuc2  5783  fpropnf1  6489  nnsuc  7044  el2mpt2csbcl  7210  poxp  7249  suppimacnv  7266  ressuppss  7274  imacosupp  7295  onnseq  7401  tz7.49  7500  oaass  7601  omordi  7606  nnmordi  7671  eroprf  7805  xpdom2  8015  inf3lem2  8486  trcl  8564  r1pwss  8607  cardaleph  8872  dfac2  8913  axcc4  9221  acncc  9222  zorn2lem7  9284  iundom2g  9322  cfpwsdom  9366  grothomex  9611  ltexprlem2  9819  1re  9999  00id  10171  mulge0  10506  nn0ge2m1nn  11320  xrlttr  11933  xmullem2  12054  snunioo  12256  fzen  12316  eluzgtdifelfzo  12486  ssfzo12bi  12520  modirr  12697  hash2pr  13205  hash3tr  13227  cshf1  13509  cshweqrep  13520  limsupbnd2  14164  climrlim2  14228  climuni  14233  mulcn2  14276  serf0  14361  cvgcmp  14494  ntrivcvg  14573  smuval2  15147  dfgcd2  15206  lcmgcdlem  15262  lcmdvds  15264  lcmf  15289  qnumdencl  15390  infpnlem1  15557  ram0  15669  prmgaplem6  15703  prmgaplem7  15704  prmlem1  15757  prmlem2  15770  setsstruct  15838  catass  16287  inveq  16374  sscfn1  16417  catsubcat  16439  subccocl  16445  funcco  16471  initoeu2  16606  funcestrcsetclem8  16727  funcsetcestrclem8  16742  gsmsymgrfixlem1  17787  psgnran  17875  efgi  18072  efgi2  18078  cntzcmnss  18186  telgsumfzs  18326  dprddisj2  18378  prmirredlem  19781  psgnghm  19866  scmatghm  20279  cpmatacl  20461  pm2mpf1  20544  fvmptnn04if  20594  lmcls  21046  isfild  21602  flffbas  21739  cnpflf2  21744  qustgplem  21864  tngngp3  22400  reperflem  22561  nmhmcn  22860  iscau2  23015  iscmet3lem2  23030  ivthlem2  23161  ovolmge0  23185  itg2seq  23449  limciun  23598  dveflem  23680  lhop1  23715  ftc1lem6  23742  mdegnn0cl  23769  aalioulem6  24030  lgsqrmod  25011  gausslemma2dlem3  25027  pntlem3  25232  axlowdimlem16  25771  axcontlem12  25789  umgrislfupgrlem  25946  uhgr2edg  26027  ushgredgedg  26048  ushgredgedgloop  26050  nbuhgr2vtx1edgb  26169  edgnbusgreu  26190  usgredgsscusgredg  26276  wlkdlem2  26483  pthdivtx  26528  upgrwlkdvdelem  26535  spthonepeq  26551  pthdlem1  26565  wlknewwlksn  26676  clwlkclwwlklem2a4  26799  clwlkclwwlklem2  26802  clwwlksnun  26874  uhgr3cyclexlem  26941  eucrctshift  27003  fusgr2wsp2nb  27090  2wspmdisj  27093  extwwlkfablem2  27102  ubthlem2  27615  shsvs  28070  mdsl2i  29069  mdsl2bi  29070  mdslmd1lem1  29072  atss  29093  chcv1  29102  chrelat2i  29112  atexch  29128  cdj3lem1  29181  bian1d  29194  disjxpin  29287  fpwrelmap  29392  nn0min  29450  sigaclci  30018  dya2iocuni  30168  omssubadd  30185  subfacp1lem6  30928  mthmblem  31238  dfon2lem6  31447  dfrdg4  31753  altopth2  31768  cgrtriv  31804  cgrextend  31810  lineext  31878  btwnconn1  31903  colinbtwnle  31920  trer  32005  elicc3  32006  poimirlem27  33107  poimirlem29  33109  poimir  33113  itg2addnc  33135  ftc1cnnc  33155  areacirclem1  33171  prnc  33537  ispridlc  33540  lcvexchlem4  33843  lcvexchlem5  33844  lkrss2N  33975  cvrnbtwn  34077  hlrelat2  34208  atle  34241  lvolex3N  34343  lplnnlelln  34348  llncvrlpln2  34362  lvolnlelln  34389  lvolnlelpln  34390  lplncvrlvol2  34420  snatpsubN  34555  linepsubN  34557  pmodlem2  34652  linepsubclN  34756  dihatexv  36146  eldioph2b  36845  pell1234qrreccl  36937  islssfg2  37160  hbtlem2  37214  clss2lem  37438  clsk1indlem3  37862  sspwtrALT2  38580  2reu3  40522  iccpartres  40682  iccpartiltu  40686  icceuelpart  40700  goldbachthlem2  40787  lighneallem4  40856  bgoldbwt  40990  bgoldbst  40991  nnsum4primesoddALTV  41004  nnsum4primeseven  41007  nnsum4primesevenALTV  41008  bgoldbtbndlem2  41013  sprsymrelfvlem  41058  mgmpropd  41093  rnghmsubcsetclem2  41294  funcrngcsetc  41316  rhmsubcsetclem2  41340  rhmsubcrngclem2  41346  funcringcsetc  41353  srhmsubc  41394  rhmsubclem4  41407  srhmsubcALTV  41412  rhmsubcALTVlem4  41425  ztprmneprm  41443  pgrpgt2nabl  41465  snlindsntor  41578  elbigo2  41668
  Copyright terms: Public domain W3C validator