Theorem adantld 490

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

Syntax hints:   → wi 4   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  im2anan9  621  jaoa  958  dedlema  1046  dedlemb  1047  prlem1  1055  dfsb1  2485  elneeldif  3903  unineq  4228  2nreu  4384  3elpr2eq  4849  tz7.7  6349  ordsssuc2  6416  fpropnf1  7222  nnsuc  7835  releldmdifi  7998  el2mpocsbcl  8035  poxp  8078  suppimacnv  8124  ressuppss  8133  onnseq  8284  tz7.49  8384  oaass  8496  omordi  8501  nnmordi  8567  naddelim  8622  eroprf  8762  xpdom2  9010  unfi  9105  infsupprpr  9419  inf3lem2  9550  trcl  9649  r1pwss  9708  cardaleph  10011  dfac2b  10053  axcc4  10361  acncc  10362  zorn2lem7  10424  iundom2g  10462  cfpwsdom  10507  grothomex  10752  ltexprlem2  10960  1re  11144  00id  11321  mulge0  11668  nn0ge2m1nn  12507  zle0orge1  12541  xrlttr  13091  xmullem2  13217  snunioo  13431  fzen  13495  eluzgtdifelfzo  13682  ssfzo12bi  13716  modirr  13904  hashfundm  14404  hash2pr  14431  hash3tr  14453  hash3tpde  14455  cshf1  14772  cshweqrep  14783  limsupbnd2  15445  climrlim2  15509  climuni  15514  mulcn2  15558  serf0  15643  cvgcmp  15779  ntrivcvg  15862  smuval2  16451  dfgcd2  16515  lcmgcdlem  16575  lcmdvds  16577  lcmf  16602  qnumdencl  16709  infpnlem1  16881  ram0  16993  prmgaplem6  17027  prmgaplem7  17028  prmlem1  17078  prmlem2  17090  setsstruct  17146  catass  17652  inveq  17741  sscfn1  17784  catsubcat  17806  subccocl  17812  funcco  17838  initoeu2  17983  funcestrcsetclem8  18113  funcsetcestrclem8  18128  mgmpropd  18619  gsmsymgrfixlem1  19402  psgnran  19490  efgi  19694  efgi2  19700  cntzcmnss  19816  telgsumfzs  19964  dprddisj2  20016  rnghmsubcsetclem2  20609  funcrngcsetc  20617  rhmsubcsetclem2  20638  rhmsubcrngclem2  20644  funcringcsetc  20651  srhmsubc  20657  rhmsubclem4  20665  rnglidlmcl  21214  prmirredlem  21452  psgnghm  21560  scmatghm  22498  cpmatacl  22681  pm2mpf1  22764  fvmptnn04if  22814  lmcls  23267  isfild  23823  flffbas  23960  cnpflf2  23965  qustgplem  24086  tngngp3  24621  reperflem  24784  nmhmcn  25087  iscau2  25244  iscmet3lem2  25259  ivthlem2  25419  ovolmge0  25444  itg2seq  25709  limciun  25861  dvres  25878  dveflem  25946  lhop1  25981  ftc1lem6  26008  mdegnn0cl  26036  aalioulem6  26303  lgsqrmod  27315  gausslemma2dlem3  27331  2sqreulem1  27409  2sqreunnlem1  27412  2sqreulem3  27416  pntlem3  27572  ltslpss  27900  axlowdimlem16  29026  axcontlem12  29044  umgrislfupgrlem  29191  uhgr2edg  29277  ushgredgedg  29298  ushgredgedgloop  29300  nbuhgr2vtx1edgb  29421  edgnbusgreu  29436  usgredgsscusgredg  29528  wlkdlem2  29750  pthdivtx  29795  upgrwlkdvdelem  29804  spthonepeq  29820  pthdlem1  29834  wwlksnprcl  29907  wlknewwlksn  29955  clwlkclwwlklem2a4  30067  clwlkclwwlklem2  30070  clwwlkwwlksb  30124  clwwlknun  30182  uhgr3cyclexlem  30251  eucrctshift  30313  frgrncvvdeqlem2  30370  frgrncvvdeqlem9  30377  numclwwlk1lem2foa  30424  numclwwlk1lem2f1  30427  ubthlem2  30942  shsvs  31394  mdsl2i  32393  mdsl2bi  32394  mdslmd1lem1  32396  atss  32417  chcv1  32426  chrelat2i  32436  atexch  32452  cdj3lem1  32505  bian1dOLD  32526  disjxpin  32658  fpwrelmap  32806  nn0min  32894  sigaclci  34276  dya2iocuni  34427  omssubadd  34444  fnrelpredd  35234  umgr2cycllem  35322  subfacp1lem6  35367  fmlasuc  35568  satffunlem  35583  satffunlem1lem1  35584  satffunlem2lem1  35586  mthmblem  35762  dfon2lem6  35968  dfrdg4  36133  altopth2  36148  cgrtriv  36184  cgrextend  36190  lineext  36258  btwnconn1  36283  colinbtwnle  36300  trer  36498  elicc3  36499  poimirlem27  37968  poimirlem29  37970  poimir  37974  itg2addnc  37995  ftc1cnnc  38013  areacirclem1  38029  prnc  38388  ispridlc  38391  refressn  38854  lcvexchlem4  39483  lcvexchlem5  39484  lkrss2N  39615  cvrnbtwn  39717  hlrelat2  39849  atle  39882  lvolex3N  39984  lplnnlelln  39989  llncvrlpln2  40003  lvolnlelln  40030  lvolnlelpln  40031  lplncvrlvol2  40061  snatpsubN  40196  linepsubN  40198  pmodlem2  40293  linepsubclN  40397  dihatexv  41784  eldioph2b  43195  pell1234qrreccl  43282  islssfg2  43499  hbtlem2  43552  onexomgt  43669  cantnfresb  43752  clss2lem  44038  clsk1indlem3  44470  mnuop3d  44698  sspwtrALT2  45249  relpfrlem  45380  fcoresf1  47517  2reu3  47558  2reu8i  47561  elsetpreimafvbi  47851  iccpartres  47878  iccpartiltu  47882  icceuelpart  47896  sprsymrelfvlem  47950  prpair  47961  prproropf1olem4  47966  prprelb  47976  nprmmul2  47988  goldbachthlem2  48009  lighneallem4  48073  requad2  48099  sbgoldbwt  48253  sbgoldbst  48254  nnsum4primesoddALTV  48273  nnsum4primeseven  48276  nnsum4primesevenALTV  48277  bgoldbtbndlem2  48282  uhgrimisgrgric  48407  grtriprop  48417  isubgr3stgrlem4  48445  isubgr3stgrlem6  48447  uspgrlimlem4  48467  grlimedgclnbgr  48471  grlimprclnbgrvtx  48475  gpgedg2ov  48542  gpgedg2iv  48543  pgnbgreunbgrlem1  48589  pgnbgreunbgrlem2  48593  pgnbgreunbgrlem4  48595  pgnbgreunbgrlem5  48599  rhmsubcALTVlem4  48760  srhmsubcALTV  48801  ztprmneprm  48823  pgrpgt2nabl  48842  snlindsntor  48947  elbigo2  49028  eenglngeehlnm  49215  itschlc0yqe  49236  itscnhlc0xyqsol  49241  itsclc0  49247  itsclquadeu  49253