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  2511  elneeldif  3913  unineq  4234  2nreu  4402  3elpr2eq  4866  tz7.7  6387  ordsssuc2  6455  fpropnf1  7269  nnsuc  7893  releldmdifi  8054  el2mpocsbcl  8094  poxp  8138  suppimacnv  8184  ressuppss  8193  onnseq  8345  tz7.49  8448  oaass  8562  omordi  8567  nnmordi  8633  naddelim  8689  eroprf  8829  xpdom2  9084  unfi  9179  infsupprpr  9491  inf3lem2  9623  trcl  9722  r1pwss  9784  cardaleph  10161  dfac2b  10202  axcc4  10510  acncc  10511  zorn2lem7  10573  iundom2g  10617  cfpwsdom  10662  grothomex  10907  ltexprlem2  11115  1re  11301  00id  11478  mulge0  11827  nn0ge2m1nn  12669  zle0orge1  12703  xrlttr  13262  xmullem2  13388  snunioo  13602  fzen  13667  eluzgtdifelfzo  13855  ssfzo12bi  13889  modirr  14078  hashfundm  14580  hash2pr  14607  hash3tr  14629  hash3tpde  14631  cshf1  14954  cshweqrep  14965  limsupbnd2  15643  climrlim2  15707  climuni  15712  mulcn2  15756  serf0  15841  cvgcmp  15976  ntrivcvg  16059  smuval2  16645  dfgcd2  16712  lcmgcdlem  16774  lcmdvds  16776  lcmf  16801  qnumdencl  16908  infpnlem1  17081  ram0  17193  prmgaplem6  17227  prmgaplem7  17228  prmlem1  17278  prmlem2  17291  setsstruct  17347  catass  17853  inveq  17942  sscfn1  17985  catsubcat  18007  subccocl  18013  funcco  18039  initoeu2  18184  funcestrcsetclem8  18314  funcsetcestrclem8  18329  mgmpropd  18822  idressidex0  18853  idressid  18855  gsmsymgrfixlem1  19634  psgnran  19722  efgi  19926  efgi2  19932  cntzcmnss  20048  telgsumfzs  20196  dprddisj2  20248  rnghmsubcsetclem2  20877  funcrngcsetc  20885  rhmsubcsetclem2  20906  rhmsubcrngclem2  20912  funcringcsetc  20919  srhmsubc  20925  rhmsubclem4  20933  rnglidlmcl  21488  df2idl2crng  21570  prmirredlem  21771  psgnghm  21879  scmatghm  22841  cpmatacl  23027  pm2mpf1  23110  fvmptnn04if  23160  lmcls  23613  isfild  24170  flffbas  24307  cnpflf2  24312  qustgplem  24433  tngngp3  24968  reperflem  25131  nmhmcn  25434  iscau2  25591  iscmet3lem2  25606  ivthlem2  25766  ovolmge0  25791  itg2seq  26056  limciun  26207  dvres  26224  dveflem  26292  lhop1  26327  ftc1lem6  26354  mdegnn0cl  26382  aalioulem6  26657  lgsqrmod  27672  gausslemma2dlem3  27688  2sqreulem1  27766  2sqreunnlem1  27769  2sqreulem3  27773  pntlem3  27929  ltslpss  28287  axlowdimlem16  29528  axcontlem12  29546  umgrislfupgrlem  29693  uhgr2edg  29782  ushgredgedg  29803  ushgredgedgloop  29805  nbuhgr2vtx1edgb  29926  edgnbusgreu  29941  usgredgsscusgredg  30033  wlkdlem2  30255  pthdivtx  30305  upgrwlkdvdelem  30315  spthonepeq  30331  pthdlem1  30345  wwlksnprcl  30421  wlknewwlksn  30469  clwlkclwwlklem2a4  30581  clwlkclwwlklem2  30584  clwwlkwwlksb  30638  clwwlknun  30696  uhgr3cyclexlem  30775  eucrctshift  30837  frgrncvvdeqlem2  30894  frgrncvvdeqlem9  30901  numclwwlk1lem2foa  30948  numclwwlk1lem2f1  30951  ubthlem2  31466  shsvs  31918  mdsl2i  32917  mdsl2bi  32918  mdslmd1lem1  32920  atss  32941  chcv1  32950  chrelat2i  32960  atexch  32976  cdj3lem1  33029  disjxpin  33175  fpwrelmap  33318  nn0min  33405  sigaclci  34757  dya2iocuni  34908  omssubadd  34925  fnrelpredd  35709  subfacp1lem6  35929  fmlasuc  36130  satffunlem  36145  satffunlem1lem1  36146  satffunlem2lem1  36148  mthmblem  36324  dfon2lem6  36530  dfrdg4  36695  altopth2  36711  cgrtriv  36747  cgrextend  36753  lineext  36821  btwnconn1  36846  colinbtwnle  36863  trer  37084  elicc3  37085  poimirlem27  38545  poimirlem29  38547  poimir  38551  itg2addnc  38572  ftc1cnnc  38590  areacirclem1  38606  prnc  38981  ispridlc  38984  refressn  39445  lcvexchlem4  40074  lcvexchlem5  40075  lkrss2N  40206  cvrnbtwn  40308  hlrelat2  40440  atle  40473  lvolex3N  40575  lplnnlelln  40580  llncvrlpln2  40594  lvolnlelln  40621  lvolnlelpln  40622  lplncvrlvol2  40652  snatpsubN  40787  linepsubN  40789  pmodlem2  40884  linepsubclN  40988  dihatexv  42375  eldioph2b  43753  pell1234qrreccl  43840  islssfg2  44057  hbtlem2  44110  onexomgt  44227  cantnfresb  44310  clss2lem  44596  clsk1indlem3  45028  mnuop3d  45240  sspwtrALT2  45790  relpfrlem  45921  fcoresf1  48108  2reu3  48149  2reu8i  48152  elsetpreimafvbi  48442  iccpartres  48469  iccpartiltu  48473  icceuelpart  48487  sprsymrelfvlem  48541  prpair  48552  prproropf1olem4  48557  prprelb  48567  nprmmul2  48579  goldbachthlem2  48600  lighneallem4  48664  requad2  48690  sbgoldbwt  48844  sbgoldbst  48845  nnsum4primesoddALTV  48864  nnsum4primeseven  48867  nnsum4primesevenALTV  48868  bgoldbtbndlem2  48873  uhgrimisgrgric  48998  grtriprop  49008  isubgr3stgrlem4  49036  isubgr3stgrlem6  49038  uspgrlimlem4  49058  grlimedgclnbgr  49062  grlimprclnbgrvtx  49066  gpgedg2ov  49133  gpgedg2iv  49134  pgnbgreunbgrlem1  49180  pgnbgreunbgrlem2  49184  pgnbgreunbgrlem4  49186  pgnbgreunbgrlem5  49190  rhmsubcALTVlem4  49350  srhmsubcALTV  49391  ztprmneprm  49428  pgrpgt2nabl  49447  snlindsntor  49552  elbigo2  49633  eenglngeehlnm  49820  itschlc0yqe  49841  itscnhlc0xyqsol  49846  itsclc0  49852  itsclquadeu  49858