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

Theorem adantld 468
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  |-  ( ph  ->  ( ps  ->  ch ) )
Assertion
Ref Expression
adantld  |-  ( ph  ->  ( ( th  /\  ps )  ->  ch )
)

Proof of Theorem adantld
StepHypRef Expression
1 simpr 462 . 2  |-  ( ( th  /\  ps )  ->  ps )
2 adantld.1 . 2  |-  ( ph  ->  ( ps  ->  ch ) )
31, 2syl5 33 1  |-  ( ph  ->  ( ( th  /\  ps )  ->  ch )
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 370
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 188  df-an 372
This theorem is referenced by:  jaoa  512  dedlema  962  dedlemb  963  prlem1  970  19.40b  1745  2eu3  2357  unineq  3729  tz7.7  5468  ordsssuc2  5530  nnsuc  6723  poxp  6919  suppimacnv  6936  ressuppss  6945  imacosupp  6966  onnseq  7071  tz7.49  7170  oaass  7270  omordi  7275  nnmordi  7340  eroprf  7469  xpdom2  7673  inf3lem2  8134  trcl  8211  r1pwss  8254  cardaleph  8518  dfac2  8559  axcc4  8867  acncc  8868  zorn2lem7  8930  iundom2g  8963  cfpwsdom  9007  grothomex  9253  ltexprlem2  9461  1re  9641  00id  9807  mulge0  10131  nn0ge2m1nn  10934  xrlttr  11439  xmullem2  11551  snunioo  11756  fzen  11814  eluzgtdifelfzo  11973  ssfzo12bi  12003  modirr  12157  hash2pr  12624  hash3tr  12638  cshweqrep  12905  limsupbnd2  13524  limsupbnd2OLD  13525  climrlim2  13589  climuni  13594  mulcn2  13637  serf0  13725  cvgcmp  13854  ntrivcvg  13931  smuval2  14430  lcmgcdlem  14542  lcmdvds  14544  lcmf  14577  qnumdencl  14659  infpnlem1  14817  ram0  14943  prmgaplem6  14989  prmgaplem7  14990  prmlem1  15042  prmlem2  15054  catass  15543  inveq  15630  sscfn1  15673  catsubcat  15695  subccocl  15701  funcco  15727  initoeu2  15862  funcestrcsetclem8  15983  funcsetcestrclem8  15998  gsmsymgrfixlem1  17019  psgnran  17107  efgi  17304  efgi2  17310  cntzcmnss  17416  telgsumfzs  17554  dprddisj2  17607  prmirredlem  18995  psgnghm  19079  scmatghm  19489  cpmatacl  19671  pm2mpf1  19754  fvmptnn04if  19804  lmcls  20249  isfild  20804  flffbas  20941  cnpflf2  20946  qustgplem  21066  reperflem  21747  nmhmcn  22027  iscau2  22140  iscmet3lem2  22155  ivthlem2  22284  ovolmge0  22308  itg2seq  22577  limciun  22726  dveflem  22808  lhop1  22843  ftc1lem6  22870  mdegnn0cl  22897  aalioulem6  23158  pntlem3  24310  axlowdimlem16  24833  axcontlem12  24851  usgraedgprv  24949  usgra2wlkspthlem2  25193  usgrcyclnl2  25214  nvnencycllem  25216  wlkv0  25333  clwlkisclwwlklem2a4  25357  clwlkisclwwlklem1  25360  2spontn0vne  25460  usg2spthonot0  25462  iseupa  25538  frgra3vlem1  25573  ubthlem2  26358  shsvs  26811  mdsl2i  27810  mdsl2bi  27811  mdslmd1lem1  27813  atss  27834  chcv1  27843  chrelat2i  27853  atexch  27869  cdj3lem1  27922  bian1d  27935  disjxpin  28037  fpwrelmap  28161  nn0min  28222  sigaclci  28793  dya2iocuni  28944  omssubadd  28961  subfacp1lem6  29696  mthmblem  30006  dfon2lem6  30221  dfrdg4  30503  altopth2  30518  cgrtriv  30554  cgrextend  30560  lineext  30628  btwnconn1  30653  colinbtwnle  30670  trer  30757  elicc3  30758  poimirlem27  31671  poimirlem29  31673  poimir  31677  itg2addnc  31700  ftc1cnnc  31720  areacirclem1  31736  prnc  32004  ispridlc  32007  lcvexchlem4  32312  lcvexchlem5  32313  lkrss2N  32444  cvrnbtwn  32546  hlrelat2  32677  atle  32710  lvolex3N  32812  lplnnlelln  32817  llncvrlpln2  32831  lvolnlelln  32858  lvolnlelpln  32859  lplncvrlvol2  32889  snatpsubN  33024  linepsubN  33026  pmodlem2  33121  linepsubclN  33225  dihatexv  34615  eldioph2b  35314  pell1234qrreccl  35408  islssfg2  35635  hbtlem2  35689  sspwtrALT2  36859  2reu3  38000  iccpartres  38122  iccpartiltu  38126  icceuelpart  38140  bgoldbwt  38268  bgoldbst  38269  nnsum4primesoddALTV  38282  nnsum4primeseven  38285  nnsum4primesevenALTV  38286  bgoldbtbndlem2  38291  usgvincvad  38474  usgvincvadALT  38477  mgmpropd  38533  rnghmsubcsetclem2  38736  funcrngcsetc  38758  rhmsubcsetclem2  38782  rhmsubcrngclem2  38788  funcringcsetc  38795  srhmsubc  38836  rhmsubclem4  38849  srhmsubcALTV  38855  rhmsubcALTVlem4  38868  ztprmneprm  38888  pgrpgt2nabl  38911  snlindsntor  39024  elbigo2  39124
  Copyright terms: Public domain W3C validator