Theorem adantld 494

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

Syntax hints:   → wi 4   ∧ wa 399

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 210  df-an 400

This theorem is referenced by:  im2anan9  623  jaoa  956  dedlema  1046  dedlemb  1047  prlem1  1055  dfsb1  2484  elneeldif  3867  unineq  4178  2nreu  4342  3elpr2eq  4804  tz7.7  6217  ordsssuc2  6279  fpropnf1  7057  nnsuc  7640  releldmdifi  7794  el2mpocsbcl  7831  poxp  7873  suppimacnv  7894  ressuppss  7903  onnseq  8059  tz7.49  8159  oaass  8267  omordi  8272  nnmordi  8337  eroprf  8475  xpdom2  8718  unfi  8828  infsupprpr  9098  inf3lem2  9222  trcl  9322  r1pwss  9365  cardaleph  9668  dfac2b  9709  axcc4  10018  acncc  10019  zorn2lem7  10081  iundom2g  10119  cfpwsdom  10163  grothomex  10408  ltexprlem2  10616  1re  10798  00id  10972  mulge0  11315  nn0ge2m1nn  12124  zle0orge1  12158  xrlttr  12695  xmullem2  12820  snunioo  13031  fzen  13094  eluzgtdifelfzo  13269  ssfzo12bi  13302  modirr  13480  hash2pr  14000  hash3tr  14021  cshf1  14340  cshweqrep  14351  limsupbnd2  15009  climrlim2  15073  climuni  15078  mulcn2  15122  serf0  15209  cvgcmp  15343  ntrivcvg  15424  smuval2  16004  dfgcd2  16069  lcmgcdlem  16126  lcmdvds  16128  lcmf  16153  qnumdencl  16258  infpnlem1  16426  ram0  16538  prmgaplem6  16572  prmgaplem7  16573  prmlem1  16624  prmlem2  16636  setsstruct  16705  catass  17143  inveq  17233  sscfn1  17276  catsubcat  17299  subccocl  17305  funcco  17331  initoeu2  17476  funcestrcsetclem8  17608  funcsetcestrclem8  17623  gsmsymgrfixlem1  18773  psgnran  18861  efgi  19063  efgi2  19069  cntzcmnss  19180  telgsumfzs  19328  dprddisj2  19380  prmirredlem  20413  psgnghm  20496  scmatghm  21384  cpmatacl  21567  pm2mpf1  21650  fvmptnn04if  21700  lmcls  22153  isfild  22709  flffbas  22846  cnpflf2  22851  qustgplem  22972  tngngp3  23508  reperflem  23669  nmhmcn  23971  iscau2  24128  iscmet3lem2  24143  ivthlem2  24303  ovolmge0  24328  itg2seq  24594  limciun  24745  dvres  24762  dveflem  24830  lhop1  24865  ftc1lem6  24892  mdegnn0cl  24923  aalioulem6  25184  lgsqrmod  26187  gausslemma2dlem3  26203  2sqreulem1  26281  2sqreunnlem1  26284  2sqreulem3  26288  pntlem3  26444  axlowdimlem16  27002  axcontlem12  27020  umgrislfupgrlem  27167  uhgr2edg  27250  ushgredgedg  27271  ushgredgedgloop  27273  nbuhgr2vtx1edgb  27394  edgnbusgreu  27409  usgredgsscusgredg  27501  wlkdlem2  27725  pthdivtx  27770  upgrwlkdvdelem  27777  spthonepeq  27793  pthdlem1  27807  wwlksnprcl  27877  wlknewwlksn  27925  clwlkclwwlklem2a4  28034  clwlkclwwlklem2  28037  clwwlkwwlksb  28091  clwwlknun  28149  uhgr3cyclexlem  28218  eucrctshift  28280  frgrncvvdeqlem2  28337  frgrncvvdeqlem9  28344  numclwwlk1lem2foa  28391  numclwwlk1lem2f1  28394  ubthlem2  28906  shsvs  29358  mdsl2i  30357  mdsl2bi  30358  mdslmd1lem1  30360  atss  30381  chcv1  30390  chrelat2i  30400  atexch  30416  cdj3lem1  30469  bian1d  30482  disjxpin  30600  fpwrelmap  30742  nn0min  30808  sigaclci  31766  dya2iocuni  31916  omssubadd  31933  fnrelpredd  32728  hashfundm  32741  umgr2cycllem  32769  subfacp1lem6  32814  fmlasuc  33015  satffunlem  33030  satffunlem1lem1  33031  satffunlem2lem1  33033  mthmblem  33209  dfon2lem6  33434  naddelim  33524  sltlpss  33773  dfrdg4  33939  altopth2  33954  cgrtriv  33990  cgrextend  33996  lineext  34064  btwnconn1  34089  colinbtwnle  34106  trer  34191  elicc3  34192  poimirlem27  35490  poimirlem29  35492  poimir  35496  itg2addnc  35517  ftc1cnnc  35535  areacirclem1  35551  prnc  35911  ispridlc  35914  lcvexchlem4  36737  lcvexchlem5  36738  lkrss2N  36869  cvrnbtwn  36971  hlrelat2  37103  atle  37136  lvolex3N  37238  lplnnlelln  37243  llncvrlpln2  37257  lvolnlelln  37284  lvolnlelpln  37285  lplncvrlvol2  37315  snatpsubN  37450  linepsubN  37452  pmodlem2  37547  linepsubclN  37651  dihatexv  39038  eldioph2b  40229  pell1234qrreccl  40320  islssfg2  40540  hbtlem2  40593  clss2lem  40836  clsk1indlem3  41271  mnuop3d  41503  sspwtrALT2  42057  fcoresf1  44178  2reu3  44217  2reu8i  44220  elsetpreimafvbi  44459  iccpartres  44486  iccpartiltu  44490  icceuelpart  44504  sprsymrelfvlem  44558  prpair  44569  prproropf1olem4  44574  prprelb  44584  goldbachthlem2  44614  lighneallem4  44678  requad2  44691  sbgoldbwt  44845  sbgoldbst  44846  nnsum4primesoddALTV  44865  nnsum4primeseven  44868  nnsum4primesevenALTV  44869  bgoldbtbndlem2  44874  mgmpropd  44945  rnghmsubcsetclem2  45150  funcrngcsetc  45172  rhmsubcsetclem2  45196  rhmsubcrngclem2  45202  funcringcsetc  45209  srhmsubc  45250  rhmsubclem4  45263  srhmsubcALTV  45268  rhmsubcALTVlem4  45281  ztprmneprm  45299  pgrpgt2nabl  45318  snlindsntor  45428  elbigo2  45514  eenglngeehlnm  45701  itschlc0yqe  45722  itscnhlc0xyqsol  45727  itsclc0  45733  itsclquadeu  45739