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

Theorem adantld 467
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 461 . 2  |-  ( ( th  /\  ps )  ->  ps )
2 adantld.1 . 2  |-  ( ph  ->  ( ps  ->  ch ) )
31, 2syl5 32 1  |-  ( ph  ->  ( ( th  /\  ps )  ->  ch )
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369
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 185  df-an 371
This theorem is referenced by:  jaoa  510  dedlema  954  dedlemb  955  prlem1  962  19.40b  1685  2eu3  2365  unineq  3733  tz7.7  4894  ordsssuc2  4956  nnsuc  6702  poxp  6897  suppimacnv  6914  ressuppss  6921  imacosupp  6942  onnseq  7017  tz7.49  7112  oaass  7212  omordi  7217  nnmordi  7282  eroprf  7411  xpdom2  7614  inf3lem2  8049  trcl  8162  r1pwss  8205  cardaleph  8473  dfac2  8514  axcc4  8822  acncc  8823  zorn2lem7  8885  iundom2g  8918  cfpwsdom  8962  grothomex  9210  ltexprlem2  9418  1re  9598  00id  9758  mulge0  10076  nn0ge2m1nn  10867  uzindOLD  10963  xrlttr  11355  xmullem2  11466  snunioo  11655  fzen  11712  eluzgtdifelfzo  11857  ssfzo12bi  11886  modirr  12036  hash2pr  12494  hash3tr  12508  cshweqrep  12768  limsupbnd2  13285  climrlim2  13349  climuni  13354  mulcn2  13397  serf0  13482  cvgcmp  13609  smuval2  14009  qnumdencl  14149  infpnlem1  14305  ram0  14417  prmlem1  14470  prmlem2  14482  catass  14960  sscfn1  15063  subccocl  15088  funcco  15114  gsmsymgrfixlem1  16326  psgnran  16414  efgi  16611  efgi2  16617  cntzcmnss  16723  telgsumfzs  16892  dprddisj2  16961  dprddisj2OLD  16962  prmirredlem  18396  prmirredlemOLD  18399  psgnghm  18489  scmatghm  18908  cpmatacl  19090  pm2mpf1  19173  fvmptnn04if  19223  lmcls  19676  isfild  20232  flffbas  20369  cnpflf2  20374  qustgplem  20492  reperflem  21196  nmhmcn  21476  iscau2  21589  iscmet3lem2  21604  ivthlem2  21737  ovolmge0  21761  itg2seq  22022  limciun  22171  dveflem  22253  lhop1  22288  ftc1lem6  22315  mdegnn0cl  22344  aalioulem6  22605  pntlem3  23666  axlowdimlem16  24132  axcontlem12  24150  usgraedgprv  24248  usgra2wlkspthlem2  24492  usgrcyclnl2  24513  nvnencycllem  24515  wlkv0  24632  clwlkisclwwlklem2a4  24656  clwlkisclwwlklem1  24659  2spontn0vne  24759  usg2spthonot0  24761  iseupa  24837  frgra3vlem1  24872  ubthlem2  25659  shsvs  26113  mdsl2i  27113  mdsl2bi  27114  mdslmd1lem1  27116  atss  27137  chcv1  27146  chrelat2i  27156  atexch  27172  cdj3lem1  27225  bian1d  27238  disjxpin  27319  fpwrelmap  27428  nn0min  27484  sigaclci  28005  dya2iocuni  28127  subfacp1lem6  28502  mthmblem  28813  ntrivcvg  29006  dfon2lem6  29195  dfrdg4  29575  altopth2  29591  cgrtriv  29627  cgrextend  29633  lineext  29701  btwnconn1  29726  colinbtwnle  29743  itg2addnc  30044  ftc1cnnc  30064  areacirclem1  30082  trer  30109  elicc3  30110  prnc  30439  ispridlc  30442  eldioph2b  30671  pell1234qrreccl  30765  islssfg2  30992  hbtlem2  31048  lcmgcdlem  31188  lcmdvds  31190  2reu3  32031  usgvincvad  32242  usgvincvadALT  32245  mgmpropd  32301  funcestrcsetclem8  32502  rnghmsubcsetclem2  32524  funcrngcsetc  32546  rhmsubcsetclem2  32567  rhmsubcrngclem2  32573  funcringcsetc  32580  srhmsubc  32617  rhmsubclem4  32630  srhmsubcOLD  32636  rhmsubcOLDlem4  32649  ztprmneprm  32669  pgrpgt2nabl  32692  snlindsntor  32807  sspwtrALT2  33356  bj-dfif5ALT  33897  lcvexchlem4  34502  lcvexchlem5  34503  lkrss2N  34634  cvrnbtwn  34736  hlrelat2  34867  atle  34900  lvolex3N  35002  lplnnlelln  35007  llncvrlpln2  35021  lvolnlelln  35048  lvolnlelpln  35049  lplncvrlvol2  35079  snatpsubN  35214  linepsubN  35216  pmodlem2  35311  linepsubclN  35415  dihatexv  36805
  Copyright terms: Public domain W3C validator