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	|- ( ph -> ( ps -> ch ) )

Assertion

Ref	Expression
adantld	|- ( ph -> ( ( th /\ ps ) -> ch ) )

Proof of Theorem adantld

Step	Hyp	Ref	Expression
1		simpr 477	. 2 |- ( ( th /\ ps ) -> ps )
2		adantld.1	. 2 |- ( ph -> ( ps -> ch ) )
3	1, 2	syl5 34	1 |- ( ph -> ( ( th /\ ps ) -> ch ) )

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  1002  dedlemb  1003  prlem1  1005  2eu3  2555  unineq  3877  3elpr2eq  4435  tz7.7  5749  ordsssuc2  5814  fpropnf1  6524  nnsuc  7082  el2mpt2csbcl  7250  poxp  7289  suppimacnv  7306  ressuppss  7314  imacosupp  7335  onnseq  7441  tz7.49  7540  oaass  7641  omordi  7646  nnmordi  7711  eroprf  7845  xpdom2  8055  inf3lem2  8526  trcl  8604  r1pwss  8647  cardaleph  8912  dfac2  8953  axcc4  9261  acncc  9262  zorn2lem7  9324  iundom2g  9362  cfpwsdom  9406  grothomex  9651  ltexprlem2  9859  1re  10039  00id  10211  mulge0  10546  nn0ge2m1nn  11360  xrlttr  11973  xmullem2  12095  snunioo  12298  fzen  12358  eluzgtdifelfzo  12529  ssfzo12bi  12563  modirr  12741  hash2pr  13251  hash3tr  13272  cshf1  13556  cshweqrep  13567  limsupbnd2  14214  climrlim2  14278  climuni  14283  mulcn2  14326  serf0  14411  cvgcmp  14548  ntrivcvg  14629  smuval2  15204  dfgcd2  15263  lcmgcdlem  15319  lcmdvds  15321  lcmf  15346  qnumdencl  15447  infpnlem1  15614  ram0  15726  prmgaplem6  15760  prmgaplem7  15761  prmlem1  15814  prmlem2  15827  setsstruct  15898  catass  16347  inveq  16434  sscfn1  16477  catsubcat  16499  subccocl  16505  funcco  16531  initoeu2  16666  funcestrcsetclem8  16787  funcsetcestrclem8  16802  gsmsymgrfixlem1  17847  psgnran  17935  efgi  18132  efgi2  18138  cntzcmnss  18246  telgsumfzs  18386  dprddisj2  18438  prmirredlem  19841  psgnghm  19926  scmatghm  20339  cpmatacl  20521  pm2mpf1  20604  fvmptnn04if  20654  lmcls  21106  isfild  21662  flffbas  21799  cnpflf2  21804  qustgplem  21924  tngngp3  22460  reperflem  22621  nmhmcn  22920  iscau2  23075  iscmet3lem2  23090  ivthlem2  23221  ovolmge0  23245  itg2seq  23509  limciun  23658  dveflem  23742  lhop1  23777  ftc1lem6  23804  mdegnn0cl  23831  aalioulem6  24092  lgsqrmod  25077  gausslemma2dlem3  25093  pntlem3  25298  axlowdimlem16  25837  axcontlem12  25855  umgrislfupgrlem  26017  uhgr2edg  26100  ushgredgedg  26121  ushgredgedgloop  26123  nbuhgr2vtx1edgb  26248  edgnbusgreu  26269  usgredgsscusgredg  26355  wlkdlem2  26580  pthdivtx  26625  upgrwlkdvdelem  26632  spthonepeq  26648  pthdlem1  26662  wlknewwlksn  26773  clwlkclwwlklem2a4  26898  clwlkclwwlklem2  26901  clwwlksnun  26974  uhgr3cyclexlem  27041  eucrctshift  27103  frgrncvvdeqlem2  27164  frgrncvvdeqlem9  27171  ubthlem2  27727  shsvs  28182  mdsl2i  29181  mdsl2bi  29182  mdslmd1lem1  29184  atss  29205  chcv1  29214  chrelat2i  29224  atexch  29240  cdj3lem1  29293  bian1d  29306  disjxpin  29401  fpwrelmap  29508  nn0min  29567  sigaclci  30195  dya2iocuni  30345  omssubadd  30362  subfacp1lem6  31167  mthmblem  31477  dfon2lem6  31693  dfrdg4  32058  altopth2  32073  cgrtriv  32109  cgrextend  32115  lineext  32183  btwnconn1  32208  colinbtwnle  32225  trer  32310  elicc3  32311  poimirlem27  33436  poimirlem29  33438  poimir  33442  itg2addnc  33464  ftc1cnnc  33484  areacirclem1  33500  prnc  33866  ispridlc  33869  lcvexchlem4  34324  lcvexchlem5  34325  lkrss2N  34456  cvrnbtwn  34558  hlrelat2  34689  atle  34722  lvolex3N  34824  lplnnlelln  34829  llncvrlpln2  34843  lvolnlelln  34870  lvolnlelpln  34871  lplncvrlvol2  34901  snatpsubN  35036  linepsubN  35038  pmodlem2  35133  linepsubclN  35237  dihatexv  36627  eldioph2b  37326  pell1234qrreccl  37418  islssfg2  37641  hbtlem2  37694  clss2lem  37918  clsk1indlem3  38341  sspwtrALT2  39058  2reu3  41188  iccpartres  41354  iccpartiltu  41358  icceuelpart  41372  goldbachthlem2  41458  lighneallem4  41527  sbgoldbwt  41665  sbgoldbst  41666  nnsum4primesoddALTV  41685  nnsum4primeseven  41688  nnsum4primesevenALTV  41689  bgoldbtbndlem2  41694  sprsymrelfvlem  41740  mgmpropd  41775  rnghmsubcsetclem2  41976  funcrngcsetc  41998  rhmsubcsetclem2  42022  rhmsubcrngclem2  42028  funcringcsetc  42035  srhmsubc  42076  rhmsubclem4  42089  srhmsubcALTV  42094  rhmsubcALTVlem4  42107  ztprmneprm  42125  pgrpgt2nabl  42147  snlindsntor  42260  elbigo2  42346