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  2513  elneeldif  4056  unineq  4236  2nreu  4405  3elpr2eq  4839  tz7.7  6414  ordsssuc2  6482  fpropnf1  7302  nnsuc  7929  releldmdifi  8091  el2mpocsbcl  8131  poxp  8177  suppimacnv  8229  ressuppss  8238  onnseq  8390  tz7.49  8493  oaass  8607  omordi  8612  nnmordi  8678  naddelim  8734  eroprf  8874  xpdom2  9129  unfi  9224  infsupprpr  9535  inf3lem2  9667  trcl  9766  r1pwss  9828  cardaleph  10207  dfac2b  10248  axcc4  10556  acncc  10557  zorn2lem7  10619  iundom2g  10663  cfpwsdom  10708  grothomex  10953  ltexprlem2  11161  1re  11347  00id  11524  mulge0  11874  nn0ge2m1nn  12716  zle0orge1  12750  xrlttr  13309  xmullem2  13435  snunioo  13649  fzen  13714  eluzgtdifelfzo  13902  ssfzo12bi  13936  modirr  14125  hashfundm  14628  hash2pr  14655  hash3tr  14677  hash3tpde  14679  cshf1  15003  cshweqrep  15014  limsupbnd2  15694  climrlim2  15758  climuni  15763  mulcn2  15807  serf0  15892  cvgcmp  16027  ntrivcvg  16110  smuval2  16696  dfgcd2  16763  lcmgcdlem  16825  lcmdvds  16827  lcmf  16852  qnumdencl  16959  infpnlem1  17132  ram0  17244  prmgaplem6  17278  prmgaplem7  17279  prmlem1  17329  prmlem2  17342  setsstruct  17398  catass  17910  inveq  17999  sscfn1  18042  catsubcat  18064  subccocl  18070  funcco  18096  initoeu2  18241  funcestrcsetclem8  18371  funcsetcestrclem8  18386  mgmpropd  18879  idressidex0  18910  idressid  18912  gsmsymgrfixlem1  19692  psgnran  19780  efgi  19984  efgi2  19990  cntzcmnss  20106  telgsumfzs  20254  dprddisj2  20306  rnghmsubcsetclem2  20935  funcrngcsetc  20943  rhmsubcsetclem2  20964  rhmsubcrngclem2  20970  funcringcsetc  20977  srhmsubc  20983  rhmsubclem4  20991  rnglidlmcl  21546  df2idl2crng  21628  prmirredlem  21833  psgnghm  21941  scmatghm  22903  cpmatacl  23089  pm2mpf1  23172  fvmptnn04if  23222  lmcls  23675  isfild  24232  flffbas  24369  cnpflf2  24374  qustgplem  24495  tngngp3  25030  reperflem  25193  nmhmcn  25496  iscau2  25653  iscmet3lem2  25668  ivthlem2  25828  ovolmge0  25853  itg2seq  26118  limciun  26269  dvres  26286  dveflem  26354  lhop1  26389  ftc1lem6  26416  mdegnn0cl  26444  aalioulem6  26721  lgsqrmod  27736  gausslemma2dlem3  27752  2sqreulem1  27830  2sqreunnlem1  27833  2sqreulem3  27837  pntlem3  27993  ltslpss  28351  axlowdimlem16  29592  axcontlem12  29610  umgrislfupgrlem  29757  uhgr2edg  29846  ushgredgedg  29867  ushgredgedgloop  29869  nbuhgr2vtx1edgb  29990  edgnbusgreu  30005  usgredgsscusgredg  30097  wlkdlem2  30319  pthdivtx  30369  upgrwlkdvdelem  30379  spthonepeq  30395  pthdlem1  30409  wwlksnprcl  30485  wlknewwlksn  30533  clwlkclwwlklem2a4  30645  clwlkclwwlklem2  30648  clwwlkwwlksb  30702  clwwlknun  30760  uhgr3cyclexlem  30839  eucrctshift  30901  frgrncvvdeqlem2  30958  frgrncvvdeqlem9  30965  numclwwlk1lem2foa  31012  numclwwlk1lem2f1  31015  ubthlem2  31530  shsvs  31982  mdsl2i  32981  mdsl2bi  32982  mdslmd1lem1  32984  atss  33005  chcv1  33014  chrelat2i  33024  atexch  33040  cdj3lem1  33093  disjxpin  33280  fpwrelmap  33421  nn0min  33508  sigaclci  34875  dya2iocuni  35026  omssubadd  35043  fnrelpredd  35845  onprcf1acwevdlem1  36086  srepdflem1  36126  subfacp1lem6  36158  fmlasuc  36359  satffunlem  36374  satffunlem1lem1  36375  satffunlem2lem1  36377  mthmblem  36553  dfon2lem6  36765  dfrdg4  36930  altopth2  36946  cgrtriv  36982  cgrextend  36988  lineext  37056  btwnconn1  37081  colinbtwnle  37098  trer  37319  elicc3  37320  poimirlem27  38833  poimirlem29  38835  poimir  38839  itg2addnc  38860  ftc1cnnc  38878  areacirclem1  38894  prnc  39267  ispridlc  39270  refressn  39731  lcvexchlem4  40360  lcvexchlem5  40361  lkrss2N  40492  cvrnbtwn  40594  hlrelat2  40726  atle  40759  lvolex3N  40861  lplnnlelln  40866  llncvrlpln2  40880  lvolnlelln  40907  lvolnlelpln  40908  lplncvrlvol2  40938  snatpsubN  41073  linepsubN  41075  pmodlem2  41170  linepsubclN  41274  dihatexv  42661  eldioph2b  44040  pell1234qrreccl  44127  islssfg2  44339  hbtlem2  44391  onexomgt  44504  cantnfresb  44587  clss2lem  44872  clsk1indlem3  45304  mnuop3d  45516  sspwtrALT2  46065  relpfrlem  46207  fcoresf1  48412  2reu3  48454  2reu8i  48457  elsetpreimafvbi  48746  iccpartres  48773  iccpartiltu  48777  icceuelpart  48791  sprsymrelfvlem  48845  prpair  48856  prproropf1olem4  48861  prprelb  48871  nprmmul2  48883  goldbachthlem2  48904  lighneallem4  48968  requad2  48994  sbgoldbwt  49148  sbgoldbst  49149  nnsum4primesoddALTV  49168  nnsum4primeseven  49171  nnsum4primesevenALTV  49172  bgoldbtbndlem2  49177  uhgrimisgrgric  49302  grtriprop  49312  isubgr3stgrlem4  49340  isubgr3stgrlem6  49342  uspgrlimlem4  49362  grlimedgclnbgr  49366  grlimprclnbgrvtx  49370  gpgedg2ov  49437  gpgedg2iv  49438  pgnbgreunbgrlem1  49484  pgnbgreunbgrlem2  49488  pgnbgreunbgrlem4  49490  pgnbgreunbgrlem5  49494  rhmsubcALTVlem4  49654  srhmsubcALTV  49695  lazsubcl  49739  ztprmneprm  49790  pgrpgt2nabl  49809  snlindsntor  49914  elbigo2  49995  itschlc0yqe  50203  itscnhlc0xyqsol  50208  itsclc0  50214  itsclquadeu  50220