Theorem adantld 491

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

Syntax hints:   → wi 4   ∧ wa 396

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 208  df-an 397

This theorem is referenced by:  im2anan9  626  jaoa  963  dedlema  1051  dedlemb  1052  prlem1  1060  dfsb1  2489  elneeldif  3897  unineq  4216  2nreu  4372  3elpr2eq  4837  tz7.7  6336  ordsssuc2  6403  fpropnf1  7211  nnsuc  7824  releldmdifi  7987  el2mpocsbcl  8024  poxp  8068  suppimacnv  8114  ressuppss  8123  onnseq  8274  tz7.49  8374  oaass  8486  omordi  8491  nnmordi  8557  naddelim  8612  eroprf  8752  xpdom2  9000  unfi  9095  infsupprpr  9409  inf3lem2  9541  trcl  9640  r1pwss  9699  cardaleph  10002  dfac2b  10044  axcc4  10352  acncc  10353  zorn2lem7  10415  iundom2g  10453  cfpwsdom  10498  grothomex  10743  ltexprlem2  10951  1re  11135  00id  11312  mulge0  11659  nn0ge2m1nn  12498  zle0orge1  12532  xrlttr  13082  xmullem2  13208  snunioo  13422  fzen  13486  eluzgtdifelfzo  13673  ssfzo12bi  13707  modirr  13895  hashfundm  14395  hash2pr  14422  hash3tr  14444  hash3tpde  14446  cshf1  14763  cshweqrep  14774  limsupbnd2  15436  climrlim2  15500  climuni  15505  mulcn2  15549  serf0  15634  cvgcmp  15770  ntrivcvg  15853  smuval2  16442  dfgcd2  16506  lcmgcdlem  16566  lcmdvds  16568  lcmf  16593  qnumdencl  16700  infpnlem1  16872  ram0  16984  prmgaplem6  17018  prmgaplem7  17019  prmlem1  17069  prmlem2  17081  setsstruct  17137  catass  17643  inveq  17732  sscfn1  17775  catsubcat  17797  subccocl  17803  funcco  17829  initoeu2  17974  funcestrcsetclem8  18104  funcsetcestrclem8  18119  mgmpropd  18610  gsmsymgrfixlem1  19393  psgnran  19481  efgi  19685  efgi2  19691  cntzcmnss  19807  telgsumfzs  19955  dprddisj2  20007  rnghmsubcsetclem2  20604  funcrngcsetc  20612  rhmsubcsetclem2  20633  rhmsubcrngclem2  20639  funcringcsetc  20646  srhmsubc  20652  rhmsubclem4  20660  rnglidlmcl  21209  prmirredlem  21447  psgnghm  21555  scmatghm  22516  cpmatacl  22699  pm2mpf1  22782  fvmptnn04if  22832  lmcls  23285  isfild  23841  flffbas  23978  cnpflf2  23983  qustgplem  24104  tngngp3  24639  reperflem  24802  nmhmcn  25105  iscau2  25262  iscmet3lem2  25277  ivthlem2  25437  ovolmge0  25462  itg2seq  25727  limciun  25879  dvres  25896  dveflem  25964  lhop1  25999  ftc1lem6  26026  mdegnn0cl  26054  aalioulem6  26321  lgsqrmod  27333  gausslemma2dlem3  27349  2sqreulem1  27427  2sqreunnlem1  27430  2sqreulem3  27434  pntlem3  27590  ltslpss  27918  axlowdimlem16  29044  axcontlem12  29062  umgrislfupgrlem  29209  uhgr2edg  29295  ushgredgedg  29316  ushgredgedgloop  29318  nbuhgr2vtx1edgb  29439  edgnbusgreu  29454  usgredgsscusgredg  29546  wlkdlem2  29768  pthdivtx  29813  upgrwlkdvdelem  29822  spthonepeq  29838  pthdlem1  29852  wwlksnprcl  29925  wlknewwlksn  29973  clwlkclwwlklem2a4  30085  clwlkclwwlklem2  30088  clwwlkwwlksb  30142  clwwlknun  30200  uhgr3cyclexlem  30269  eucrctshift  30331  frgrncvvdeqlem2  30388  frgrncvvdeqlem9  30395  numclwwlk1lem2foa  30442  numclwwlk1lem2f1  30445  ubthlem2  30960  shsvs  31412  mdsl2i  32411  mdsl2bi  32412  mdslmd1lem1  32414  atss  32435  chcv1  32444  chrelat2i  32454  atexch  32470  cdj3lem1  32523  bian1dOLD  32544  disjxpin  32677  fpwrelmap  32825  nn0min  32913  sigaclci  34316  dya2iocuni  34467  omssubadd  34484  fnrelpredd  35272  umgr2cycllem  35368  subfacp1lem6  35413  fmlasuc  35614  satffunlem  35629  satffunlem1lem1  35630  satffunlem2lem1  35632  mthmblem  35808  dfon2lem6  36014  dfrdg4  36179  altopth2  36194  cgrtriv  36230  cgrextend  36236  lineext  36304  btwnconn1  36329  colinbtwnle  36346  trer  36544  elicc3  36545  poimirlem27  38014  poimirlem29  38016  poimir  38020  itg2addnc  38041  ftc1cnnc  38059  areacirclem1  38075  prnc  38434  ispridlc  38437  refressn  38900  lcvexchlem4  39529  lcvexchlem5  39530  lkrss2N  39661  cvrnbtwn  39763  hlrelat2  39895  atle  39928  lvolex3N  40030  lplnnlelln  40035  llncvrlpln2  40049  lvolnlelln  40076  lvolnlelpln  40077  lplncvrlvol2  40107  snatpsubN  40242  linepsubN  40244  pmodlem2  40339  linepsubclN  40443  dihatexv  41830  eldioph2b  43212  pell1234qrreccl  43299  islssfg2  43516  hbtlem2  43569  onexomgt  43686  cantnfresb  43769  clss2lem  44055  clsk1indlem3  44487  mnuop3d  44715  sspwtrALT2  45266  relpfrlem  45397  fcoresf1  47532  2reu3  47573  2reu8i  47576  elsetpreimafvbi  47866  iccpartres  47893  iccpartiltu  47897  icceuelpart  47911  sprsymrelfvlem  47965  prpair  47976  prproropf1olem4  47981  prprelb  47991  nprmmul2  48003  goldbachthlem2  48024  lighneallem4  48088  requad2  48114  sbgoldbwt  48268  sbgoldbst  48269  nnsum4primesoddALTV  48288  nnsum4primeseven  48291  nnsum4primesevenALTV  48292  bgoldbtbndlem2  48297  uhgrimisgrgric  48422  grtriprop  48432  isubgr3stgrlem4  48460  isubgr3stgrlem6  48462  uspgrlimlem4  48482  grlimedgclnbgr  48486  grlimprclnbgrvtx  48490  gpgedg2ov  48557  gpgedg2iv  48558  pgnbgreunbgrlem1  48604  pgnbgreunbgrlem2  48608  pgnbgreunbgrlem4  48610  pgnbgreunbgrlem5  48614  rhmsubcALTVlem4  48775  srhmsubcALTV  48816  ztprmneprm  48838  pgrpgt2nabl  48857  snlindsntor  48962  elbigo2  49043  eenglngeehlnm  49230  itschlc0yqe  49251  itscnhlc0xyqsol  49256  itsclc0  49262  itsclquadeu  49268