Theorem adantld 482

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

Syntax hints:   → wi 4   ∧ wa 383

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 196  df-an 385

This theorem is referenced by:  jaoa  531  dedlema  993  dedlemb  994  prlem1  997  19.40bOLD  1805  2eu3  2543  unineq  3836  tz7.7  5666  ordsssuc2  5731  nnsuc  6974  el2mpt2csbcl  7137  poxp  7176  suppimacnv  7193  ressuppss  7201  imacosupp  7222  onnseq  7328  tz7.49  7427  oaass  7528  omordi  7533  nnmordi  7598  eroprf  7732  xpdom2  7940  inf3lem2  8409  trcl  8487  r1pwss  8530  cardaleph  8795  dfac2  8836  axcc4  9144  acncc  9145  zorn2lem7  9207  iundom2g  9241  cfpwsdom  9285  grothomex  9530  ltexprlem2  9738  1re  9918  00id  10090  mulge0  10425  nn0ge2m1nn  11237  xrlttr  11849  xmullem2  11967  snunioo  12169  fzen  12229  eluzgtdifelfzo  12397  ssfzo12bi  12429  modirr  12603  hash2pr  13108  hash3tr  13127  cshf1  13407  cshweqrep  13418  limsupbnd2  14062  climrlim2  14126  climuni  14131  mulcn2  14174  serf0  14259  cvgcmp  14389  ntrivcvg  14468  smuval2  15042  dfgcd2  15101  lcmgcdlem  15157  lcmdvds  15159  lcmf  15184  qnumdencl  15285  infpnlem1  15452  ram0  15564  prmgaplem6  15598  prmgaplem7  15599  prmlem1  15652  prmlem2  15665  catass  16170  inveq  16257  sscfn1  16300  catsubcat  16322  subccocl  16328  funcco  16354  initoeu2  16489  funcestrcsetclem8  16610  funcsetcestrclem8  16625  gsmsymgrfixlem1  17670  psgnran  17758  efgi  17955  efgi2  17961  cntzcmnss  18069  telgsumfzs  18209  dprddisj2  18261  prmirredlem  19660  psgnghm  19745  scmatghm  20158  cpmatacl  20340  pm2mpf1  20423  fvmptnn04if  20473  lmcls  20916  isfild  21472  flffbas  21609  cnpflf2  21614  qustgplem  21734  tngngp3  22270  reperflem  22429  nmhmcn  22728  iscau2  22883  iscmet3lem2  22898  ivthlem2  23028  ovolmge0  23052  itg2seq  23315  limciun  23464  dveflem  23546  lhop1  23581  ftc1lem6  23608  mdegnn0cl  23635  aalioulem6  23896  lgsqrmod  24877  gausslemma2dlem3  24893  pntlem3  25098  axlowdimlem16  25637  axcontlem12  25655  umgrislfupgrlem  25788  usgraedgprv  25905  usgra2wlkspthlem2  26148  usgrcyclnl2  26169  nvnencycllem  26171  wlkv0  26288  clwlkisclwwlklem2a4  26312  clwlkisclwwlklem1  26315  2spontn0vne  26414  usg2spthonot0  26416  iseupa  26492  frgra3vlem1  26527  ubthlem2  27111  shsvs  27566  mdsl2i  28565  mdsl2bi  28566  mdslmd1lem1  28568  atss  28589  chcv1  28598  chrelat2i  28608  atexch  28624  cdj3lem1  28677  bian1d  28690  disjxpin  28783  fpwrelmap  28896  nn0min  28954  sigaclci  29522  dya2iocuni  29672  omssubadd  29689  subfacp1lem6  30421  mthmblem  30731  dfon2lem6  30937  dfrdg4  31228  altopth2  31243  cgrtriv  31279  cgrextend  31285  lineext  31353  btwnconn1  31378  colinbtwnle  31395  trer  31480  elicc3  31481  poimirlem27  32606  poimirlem29  32608  poimir  32612  itg2addnc  32634  ftc1cnnc  32654  areacirclem1  32670  prnc  33036  ispridlc  33039  lcvexchlem4  33342  lcvexchlem5  33343  lkrss2N  33474  cvrnbtwn  33576  hlrelat2  33707  atle  33740  lvolex3N  33842  lplnnlelln  33847  llncvrlpln2  33861  lvolnlelln  33888  lvolnlelpln  33889  lplncvrlvol2  33919  snatpsubN  34054  linepsubN  34056  pmodlem2  34151  linepsubclN  34255  dihatexv  35645  eldioph2b  36344  pell1234qrreccl  36436  islssfg2  36659  hbtlem2  36713  clss2lem  36937  clsk1indlem3  37361  sspwtrALT2  38080  2reu3  39837  iccpartres  39956  iccpartiltu  39960  icceuelpart  39974  goldbachthlem2  39996  lighneallem4  40065  bgoldbwt  40199  bgoldbst  40200  nnsum4primesoddALTV  40213  nnsum4primeseven  40216  nnsum4primesevenALTV  40217  bgoldbtbndlem2  40222  fpropnf1  40337  uhgr2edg  40435  ushgredgedga  40456  ushgredgedgaloop  40458  nbuhgr2vtx1edgb  40574  edgnbusgreu  40595  usgredgsscusgredg  40675  1wlkdlem2  40892  pthdivtx  40935  upgrwlkdvdelem  40942  spthonepeq-av  40958  pthdlem1  40972  wlknewwlksn  41084  clwlkclwwlklem2a4  41206  clwlkclwwlklem2  41209  clwwlksnun  41281  uhgr3cyclexlem  41348  eucrctshift  41411  fusgr2wsp2nb  41498  2wspmdisj  41501  av-extwwlkfablem2  41510  mgmpropd  41565  rnghmsubcsetclem2  41768  funcrngcsetc  41790  rhmsubcsetclem2  41814  rhmsubcrngclem2  41820  funcringcsetc  41827  srhmsubc  41868  rhmsubclem4  41881  srhmsubcALTV  41887  rhmsubcALTVlem4  41900  ztprmneprm  41918  pgrpgt2nabl  41941  snlindsntor  42054  elbigo2  42144