Theorem adantld 496

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 490	. 2 ⊢ ((𝜃 ∧ 𝜓) → 𝜓)
2		adantld.1	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
3	1, 2	syl5 35	1 ⊢ (𝜑 → ((𝜃 ∧ 𝜓) → 𝜒))

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  im2anan9  632  jaoa  970  dedlema  1061  dedlemb  1062  prlem1  1070  dfsb1  2510  elneeldif  3913  unineq  4234  2nreu  4402  3elpr2eq  4866  tz7.7  6383  ordsssuc2  6451  fpropnf1  7264  nnsuc  7880  releldmdifi  8042  el2mpocsbcl  8082  poxp  8126  suppimacnv  8172  ressuppss  8181  onnseq  8333  tz7.49  8434  oaass  8548  omordi  8553  nnmordi  8619  naddelim  8675  eroprf  8815  xpdom2  9070  unfi  9165  infsupprpr  9476  inf3lem2  9608  trcl  9707  r1pwss  9766  cardaleph  10092  dfac2b  10133  axcc4  10441  acncc  10442  zorn2lem7  10504  iundom2g  10548  cfpwsdom  10593  grothomex  10838  ltexprlem2  11046  1re  11232  00id  11409  mulge0  11756  nn0ge2m1nn  12598  zle0orge1  12632  xrlttr  13191  xmullem2  13317  snunioo  13531  fzen  13595  eluzgtdifelfzo  13783  ssfzo12bi  13817  modirr  14006  hashfundm  14507  hash2pr  14534  hash3tr  14556  hash3tpde  14558  cshf1  14881  cshweqrep  14892  limsupbnd2  15570  climrlim2  15634  climuni  15639  mulcn2  15683  serf0  15768  cvgcmp  15903  ntrivcvg  15986  smuval2  16572  dfgcd2  16636  lcmgcdlem  16696  lcmdvds  16698  lcmf  16723  qnumdencl  16830  infpnlem1  17002  ram0  17114  prmgaplem6  17148  prmgaplem7  17149  prmlem1  17199  prmlem2  17212  setsstruct  17268  catass  17774  inveq  17863  sscfn1  17906  catsubcat  17928  subccocl  17934  funcco  17960  initoeu2  18105  funcestrcsetclem8  18235  funcsetcestrclem8  18250  mgmpropd  18743  idressidex0  18773  idressid  18775  gsmsymgrfixlem1  19554  psgnran  19642  efgi  19846  efgi2  19852  cntzcmnss  19968  telgsumfzs  20116  dprddisj2  20168  rnghmsubcsetclem2  20794  funcrngcsetc  20802  rhmsubcsetclem2  20823  rhmsubcrngclem2  20829  funcringcsetc  20836  srhmsubc  20842  rhmsubclem4  20850  rnglidlmcl  21404  df2idl2crng  21484  prmirredlem  21685  psgnghm  21793  scmatghm  22755  cpmatacl  22941  pm2mpf1  23024  fvmptnn04if  23074  lmcls  23527  isfild  24084  flffbas  24221  cnpflf2  24226  qustgplem  24347  tngngp3  24882  reperflem  25045  nmhmcn  25348  iscau2  25505  iscmet3lem2  25520  ivthlem2  25680  ovolmge0  25705  itg2seq  25970  limciun  26121  dvres  26138  dveflem  26206  lhop1  26241  ftc1lem6  26268  mdegnn0cl  26296  aalioulem6  26573  lgsqrmod  27588  gausslemma2dlem3  27604  2sqreulem1  27682  2sqreunnlem1  27685  2sqreulem3  27689  pntlem3  27845  ltslpss  28173  axlowdimlem16  29414  axcontlem12  29432  umgrislfupgrlem  29579  uhgr2edg  29668  ushgredgedg  29689  ushgredgedgloop  29691  nbuhgr2vtx1edgb  29812  edgnbusgreu  29827  usgredgsscusgredg  29919  wlkdlem2  30141  pthdivtx  30191  upgrwlkdvdelem  30201  spthonepeq  30217  pthdlem1  30231  wwlksnprcl  30307  wlknewwlksn  30355  clwlkclwwlklem2a4  30467  clwlkclwwlklem2  30470  clwwlkwwlksb  30524  clwwlknun  30582  uhgr3cyclexlem  30661  eucrctshift  30723  frgrncvvdeqlem2  30780  frgrncvvdeqlem9  30787  numclwwlk1lem2foa  30834  numclwwlk1lem2f1  30837  ubthlem2  31352  shsvs  31804  mdsl2i  32803  mdsl2bi  32804  mdslmd1lem1  32806  atss  32827  chcv1  32836  chrelat2i  32846  atexch  32862  cdj3lem1  32915  disjxpin  33061  fpwrelmap  33204  nn0min  33291  sigaclci  34642  dya2iocuni  34794  omssubadd  34811  fnrelpredd  35596  subfacp1lem6  35764  fmlasuc  35965  satffunlem  35980  satffunlem1lem1  35981  satffunlem2lem1  35983  mthmblem  36159  dfon2lem6  36365  dfrdg4  36530  altopth2  36546  cgrtriv  36582  cgrextend  36588  lineext  36656  btwnconn1  36681  colinbtwnle  36698  trer  36935  elicc3  36936  poimirlem27  38396  poimirlem29  38398  poimir  38402  itg2addnc  38423  ftc1cnnc  38441  areacirclem1  38457  prnc  38817  ispridlc  38820  refressn  39281  lcvexchlem4  39910  lcvexchlem5  39911  lkrss2N  40042  cvrnbtwn  40144  hlrelat2  40276  atle  40309  lvolex3N  40411  lplnnlelln  40416  llncvrlpln2  40430  lvolnlelln  40457  lvolnlelpln  40458  lplncvrlvol2  40488  snatpsubN  40623  linepsubN  40625  pmodlem2  40720  linepsubclN  40824  dihatexv  42211  eldioph2b  43608  pell1234qrreccl  43695  islssfg2  43912  hbtlem2  43965  onexomgt  44082  cantnfresb  44165  clss2lem  44451  clsk1indlem3  44883  mnuop3d  45095  sspwtrALT2  45645  relpfrlem  45776  fcoresf1  47957  2reu3  47998  2reu8i  48001  elsetpreimafvbi  48291  iccpartres  48318  iccpartiltu  48322  icceuelpart  48336  sprsymrelfvlem  48390  prpair  48401  prproropf1olem4  48406  prprelb  48416  nprmmul2  48428  goldbachthlem2  48449  lighneallem4  48513  requad2  48539  sbgoldbwt  48693  sbgoldbst  48694  nnsum4primesoddALTV  48713  nnsum4primeseven  48716  nnsum4primesevenALTV  48717  bgoldbtbndlem2  48722  uhgrimisgrgric  48847  grtriprop  48857  isubgr3stgrlem4  48885  isubgr3stgrlem6  48887  uspgrlimlem4  48907  grlimedgclnbgr  48911  grlimprclnbgrvtx  48915  gpgedg2ov  48982  gpgedg2iv  48983  pgnbgreunbgrlem1  49029  pgnbgreunbgrlem2  49033  pgnbgreunbgrlem4  49035  pgnbgreunbgrlem5  49039  rhmsubcALTVlem4  49199  srhmsubcALTV  49240  ztprmneprm  49277  pgrpgt2nabl  49296  snlindsntor  49401  elbigo2  49482  eenglngeehlnm  49669  itschlc0yqe  49690  itscnhlc0xyqsol  49695  itsclc0  49701  itsclquadeu  49707