Theorem adantld 490

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

Step	Hyp	Ref	Expression
1		simpr 484	. 2 ⊢ ((𝜃 ∧ 𝜓) → 𝜓)
2		adantld.1	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
3	1, 2	syl5 34	1 ⊢ (𝜑 → ((𝜃 ∧ 𝜓) → 𝜒))

Syntax hints:   → wi 4   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  im2anan9  620  jaoa  957  dedlema  1045  dedlemb  1046  prlem1  1054  dfsb1  2479  elneeldif  3919  unineq  4241  2nreu  4397  3elpr2eq  4860  tz7.7  6337  ordsssuc2  6404  fpropnf1  7208  nnsuc  7824  releldmdifi  7987  el2mpocsbcl  8025  poxp  8068  suppimacnv  8114  ressuppss  8123  onnseq  8274  tz7.49  8374  oaass  8486  omordi  8491  nnmordi  8556  naddelim  8611  eroprf  8749  xpdom2  8996  unfi  9095  infsupprpr  9415  inf3lem2  9544  trcl  9643  r1pwss  9699  cardaleph  10002  dfac2b  10044  axcc4  10352  acncc  10353  zorn2lem7  10415  iundom2g  10453  cfpwsdom  10497  grothomex  10742  ltexprlem2  10950  1re  11134  00id  11309  mulge0  11656  nn0ge2m1nn  12472  zle0orge1  12506  xrlttr  13060  xmullem2  13185  snunioo  13399  fzen  13462  eluzgtdifelfzo  13648  ssfzo12bi  13682  modirr  13867  hashfundm  14367  hash2pr  14394  hash3tr  14416  hash3tpde  14418  cshf1  14734  cshweqrep  14745  limsupbnd2  15408  climrlim2  15472  climuni  15477  mulcn2  15521  serf0  15606  cvgcmp  15741  ntrivcvg  15822  smuval2  16411  dfgcd2  16475  lcmgcdlem  16535  lcmdvds  16537  lcmf  16562  qnumdencl  16668  infpnlem1  16840  ram0  16952  prmgaplem6  16986  prmgaplem7  16987  prmlem1  17037  prmlem2  17049  setsstruct  17105  catass  17610  inveq  17699  sscfn1  17742  catsubcat  17764  subccocl  17770  funcco  17796  initoeu2  17941  funcestrcsetclem8  18071  funcsetcestrclem8  18086  mgmpropd  18543  gsmsymgrfixlem1  19324  psgnran  19412  efgi  19616  efgi2  19622  cntzcmnss  19738  telgsumfzs  19886  dprddisj2  19938  rnghmsubcsetclem2  20535  funcrngcsetc  20543  rhmsubcsetclem2  20564  rhmsubcrngclem2  20570  funcringcsetc  20577  srhmsubc  20583  rhmsubclem4  20591  rnglidlmcl  21141  prmirredlem  21397  psgnghm  21505  scmatghm  22436  cpmatacl  22619  pm2mpf1  22702  fvmptnn04if  22752  lmcls  23205  isfild  23761  flffbas  23898  cnpflf2  23903  qustgplem  24024  tngngp3  24560  reperflem  24723  nmhmcn  25036  iscau2  25193  iscmet3lem2  25208  ivthlem2  25369  ovolmge0  25394  itg2seq  25659  limciun  25811  dvres  25828  dveflem  25899  lhop1  25935  ftc1lem6  25964  mdegnn0cl  25992  aalioulem6  26261  lgsqrmod  27279  gausslemma2dlem3  27295  2sqreulem1  27373  2sqreunnlem1  27376  2sqreulem3  27380  pntlem3  27536  sltlpss  27840  axlowdimlem16  28920  axcontlem12  28938  umgrislfupgrlem  29085  uhgr2edg  29171  ushgredgedg  29192  ushgredgedgloop  29194  nbuhgr2vtx1edgb  29315  edgnbusgreu  29330  usgredgsscusgredg  29423  wlkdlem2  29645  pthdivtx  29690  upgrwlkdvdelem  29699  spthonepeq  29715  pthdlem1  29729  wwlksnprcl  29802  wlknewwlksn  29850  clwlkclwwlklem2a4  29959  clwlkclwwlklem2  29962  clwwlkwwlksb  30016  clwwlknun  30074  uhgr3cyclexlem  30143  eucrctshift  30205  frgrncvvdeqlem2  30262  frgrncvvdeqlem9  30269  numclwwlk1lem2foa  30316  numclwwlk1lem2f1  30319  ubthlem2  30833  shsvs  31285  mdsl2i  32284  mdsl2bi  32285  mdslmd1lem1  32287  atss  32308  chcv1  32317  chrelat2i  32327  atexch  32343  cdj3lem1  32396  bian1dOLD  32419  disjxpin  32550  fpwrelmap  32689  nn0min  32778  sigaclci  34101  dya2iocuni  34253  omssubadd  34270  fnrelpredd  35058  umgr2cycllem  35115  subfacp1lem6  35160  fmlasuc  35361  satffunlem  35376  satffunlem1lem1  35377  satffunlem2lem1  35379  mthmblem  35555  dfon2lem6  35764  dfrdg4  35927  altopth2  35942  cgrtriv  35978  cgrextend  35984  lineext  36052  btwnconn1  36077  colinbtwnle  36094  trer  36292  elicc3  36293  poimirlem27  37629  poimirlem29  37631  poimir  37635  itg2addnc  37656  ftc1cnnc  37674  areacirclem1  37690  prnc  38049  ispridlc  38052  refressn  38422  lcvexchlem4  39018  lcvexchlem5  39019  lkrss2N  39150  cvrnbtwn  39252  hlrelat2  39385  atle  39418  lvolex3N  39520  lplnnlelln  39525  llncvrlpln2  39539  lvolnlelln  39566  lvolnlelpln  39567  lplncvrlvol2  39597  snatpsubN  39732  linepsubN  39734  pmodlem2  39829  linepsubclN  39933  dihatexv  41320  eldioph2b  42739  pell1234qrreccl  42830  islssfg2  43047  hbtlem2  43100  onexomgt  43217  cantnfresb  43300  clss2lem  43587  clsk1indlem3  44019  mnuop3d  44247  sspwtrALT2  44799  relpfrlem  44930  fcoresf1  47057  2reu3  47098  2reu8i  47101  elsetpreimafvbi  47379  iccpartres  47406  iccpartiltu  47410  icceuelpart  47424  sprsymrelfvlem  47478  prpair  47489  prproropf1olem4  47494  prprelb  47504  goldbachthlem2  47534  lighneallem4  47598  requad2  47611  sbgoldbwt  47765  sbgoldbst  47766  nnsum4primesoddALTV  47785  nnsum4primeseven  47788  nnsum4primesevenALTV  47789  bgoldbtbndlem2  47794  uhgrimisgrgric  47919  grtriprop  47929  isubgr3stgrlem4  47957  isubgr3stgrlem6  47959  uspgrlimlem4  47979  grlimedgclnbgr  47983  grlimprclnbgrvtx  47987  gpgedg2ov  48054  gpgedg2iv  48055  pgnbgreunbgrlem1  48101  pgnbgreunbgrlem2  48105  pgnbgreunbgrlem4  48107  pgnbgreunbgrlem5  48111  rhmsubcALTVlem4  48272  srhmsubcALTV  48313  ztprmneprm  48335  pgrpgt2nabl  48354  snlindsntor  48460  elbigo2  48541  eenglngeehlnm  48728  itschlc0yqe  48749  itscnhlc0xyqsol  48754  itsclc0  48760  itsclquadeu  48766