Theorem adantld 489

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

Syntax hints:   → wi 4   ∧ wa 394

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 206  df-an 395

This theorem is referenced by:  im2anan9  618  jaoa  952  dedlema  1042  dedlemb  1043  prlem1  1051  dfsb1  2478  elneeldif  3961  unineq  4276  2nreu  4440  3elpr2eq  4906  tz7.7  6389  ordsssuc2  6454  fpropnf1  7268  nnsuc  7875  releldmdifi  8033  el2mpocsbcl  8073  poxp  8116  suppimacnv  8161  ressuppss  8170  onnseq  8346  tz7.49  8447  oaass  8563  omordi  8568  nnmordi  8633  naddelim  8687  eroprf  8811  xpdom2  9069  unfi  9174  infsupprpr  9501  inf3lem2  9626  trcl  9725  r1pwss  9781  cardaleph  10086  dfac2b  10127  axcc4  10436  acncc  10437  zorn2lem7  10499  iundom2g  10537  cfpwsdom  10581  grothomex  10826  ltexprlem2  11034  1re  11218  00id  11393  mulge0  11736  nn0ge2m1nn  12545  zle0orge1  12579  xrlttr  13123  xmullem2  13248  snunioo  13459  fzen  13522  eluzgtdifelfzo  13698  ssfzo12bi  13731  modirr  13911  hashfundm  14406  hash2pr  14434  hash3tr  14455  cshf1  14764  cshweqrep  14775  limsupbnd2  15431  climrlim2  15495  climuni  15500  mulcn2  15544  serf0  15631  cvgcmp  15766  ntrivcvg  15847  smuval2  16427  dfgcd2  16492  lcmgcdlem  16547  lcmdvds  16549  lcmf  16574  qnumdencl  16679  infpnlem1  16847  ram0  16959  prmgaplem6  16993  prmgaplem7  16994  prmlem1  17045  prmlem2  17057  setsstruct  17113  catass  17634  inveq  17725  sscfn1  17768  catsubcat  17793  subccocl  17799  funcco  17825  initoeu2  17970  funcestrcsetclem8  18103  funcsetcestrclem8  18118  mgmpropd  18576  gsmsymgrfixlem1  19336  psgnran  19424  efgi  19628  efgi2  19634  cntzcmnss  19750  telgsumfzs  19898  dprddisj2  19950  rnglidlmcl  20982  prmirredlem  21243  psgnghm  21352  scmatghm  22255  cpmatacl  22438  pm2mpf1  22521  fvmptnn04if  22571  lmcls  23026  isfild  23582  flffbas  23719  cnpflf2  23724  qustgplem  23845  tngngp3  24393  reperflem  24554  nmhmcn  24867  iscau2  25025  iscmet3lem2  25040  ivthlem2  25201  ovolmge0  25226  itg2seq  25492  limciun  25643  dvres  25660  dveflem  25731  lhop1  25766  ftc1lem6  25793  mdegnn0cl  25824  aalioulem6  26086  lgsqrmod  27091  gausslemma2dlem3  27107  2sqreulem1  27185  2sqreunnlem1  27188  2sqreulem3  27192  pntlem3  27348  sltlpss  27638  axlowdimlem16  28482  axcontlem12  28500  umgrislfupgrlem  28649  uhgr2edg  28732  ushgredgedg  28753  ushgredgedgloop  28755  nbuhgr2vtx1edgb  28876  edgnbusgreu  28891  usgredgsscusgredg  28983  wlkdlem2  29207  pthdivtx  29253  upgrwlkdvdelem  29260  spthonepeq  29276  pthdlem1  29290  wwlksnprcl  29360  wlknewwlksn  29408  clwlkclwwlklem2a4  29517  clwlkclwwlklem2  29520  clwwlkwwlksb  29574  clwwlknun  29632  uhgr3cyclexlem  29701  eucrctshift  29763  frgrncvvdeqlem2  29820  frgrncvvdeqlem9  29827  numclwwlk1lem2foa  29874  numclwwlk1lem2f1  29877  ubthlem2  30391  shsvs  30843  mdsl2i  31842  mdsl2bi  31843  mdslmd1lem1  31845  atss  31866  chcv1  31875  chrelat2i  31885  atexch  31901  cdj3lem1  31954  bian1d  31967  disjxpin  32086  fpwrelmap  32225  nn0min  32293  sigaclci  33428  dya2iocuni  33580  omssubadd  33597  fnrelpredd  34390  umgr2cycllem  34429  subfacp1lem6  34474  fmlasuc  34675  satffunlem  34690  satffunlem1lem1  34691  satffunlem2lem1  34693  mthmblem  34869  dfon2lem6  35064  dfrdg4  35227  altopth2  35242  cgrtriv  35278  cgrextend  35284  lineext  35352  btwnconn1  35377  colinbtwnle  35394  trer  35504  elicc3  35505  poimirlem27  36818  poimirlem29  36820  poimir  36824  itg2addnc  36845  ftc1cnnc  36863  areacirclem1  36879  prnc  37238  ispridlc  37241  refressn  37616  lcvexchlem4  38210  lcvexchlem5  38211  lkrss2N  38342  cvrnbtwn  38444  hlrelat2  38577  atle  38610  lvolex3N  38712  lplnnlelln  38717  llncvrlpln2  38731  lvolnlelln  38758  lvolnlelpln  38759  lplncvrlvol2  38789  snatpsubN  38924  linepsubN  38926  pmodlem2  39021  linepsubclN  39125  dihatexv  40512  eldioph2b  41803  pell1234qrreccl  41894  islssfg2  42115  hbtlem2  42168  onexomgt  42292  cantnfresb  42376  clss2lem  42664  clsk1indlem3  43096  mnuop3d  43332  sspwtrALT2  43886  fcoresf1  46077  2reu3  46116  2reu8i  46119  elsetpreimafvbi  46357  iccpartres  46384  iccpartiltu  46388  icceuelpart  46402  sprsymrelfvlem  46456  prpair  46467  prproropf1olem4  46472  prprelb  46482  goldbachthlem2  46512  lighneallem4  46576  requad2  46589  sbgoldbwt  46743  sbgoldbst  46744  nnsum4primesoddALTV  46763  nnsum4primeseven  46766  nnsum4primesevenALTV  46767  bgoldbtbndlem2  46772  rnghmsubcsetclem2  46962  funcrngcsetc  46984  rhmsubcsetclem2  47008  rhmsubcrngclem2  47014  funcringcsetc  47021  srhmsubc  47062  rhmsubclem4  47075  srhmsubcALTV  47080  rhmsubcALTVlem4  47093  ztprmneprm  47111  pgrpgt2nabl  47130  snlindsntor  47239  elbigo2  47325  eenglngeehlnm  47512  itschlc0yqe  47533  itscnhlc0xyqsol  47538  itsclc0  47544  itsclquadeu  47550