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

This theorem is referenced by:  im2anan9  620  jaoa  953  dedlema  1043  dedlemb  1044  prlem1  1052  dfsb1  2487  elneeldif  3906  unineq  4217  2nreu  4381  3elpr2eq  4844  tz7.7  6291  ordsssuc2  6353  fpropnf1  7137  nnsuc  7724  releldmdifi  7879  el2mpocsbcl  7916  poxp  7960  suppimacnv  7981  ressuppss  7990  onnseq  8166  tz7.49  8267  oaass  8377  omordi  8382  nnmordi  8447  eroprf  8587  xpdom2  8836  unfi  8937  infsupprpr  9241  inf3lem2  9365  trcl  9486  r1pwss  9543  cardaleph  9846  dfac2b  9887  axcc4  10196  acncc  10197  zorn2lem7  10259  iundom2g  10297  cfpwsdom  10341  grothomex  10586  ltexprlem2  10794  1re  10976  00id  11150  mulge0  11493  nn0ge2m1nn  12302  zle0orge1  12336  xrlttr  12873  xmullem2  12998  snunioo  13209  fzen  13272  eluzgtdifelfzo  13447  ssfzo12bi  13480  modirr  13660  hash2pr  14181  hash3tr  14202  cshf1  14521  cshweqrep  14532  limsupbnd2  15190  climrlim2  15254  climuni  15259  mulcn2  15303  serf0  15390  cvgcmp  15526  ntrivcvg  15607  smuval2  16187  dfgcd2  16252  lcmgcdlem  16309  lcmdvds  16311  lcmf  16336  qnumdencl  16441  infpnlem1  16609  ram0  16721  prmgaplem6  16755  prmgaplem7  16756  prmlem1  16807  prmlem2  16819  setsstruct  16875  catass  17393  inveq  17484  sscfn1  17527  catsubcat  17552  subccocl  17558  funcco  17584  initoeu2  17729  funcestrcsetclem8  17862  funcsetcestrclem8  17877  gsmsymgrfixlem1  19033  psgnran  19121  efgi  19323  efgi2  19329  cntzcmnss  19440  telgsumfzs  19588  dprddisj2  19640  prmirredlem  20692  psgnghm  20783  scmatghm  21680  cpmatacl  21863  pm2mpf1  21946  fvmptnn04if  21996  lmcls  22451  isfild  23007  flffbas  23144  cnpflf2  23149  qustgplem  23270  tngngp3  23818  reperflem  23979  nmhmcn  24281  iscau2  24439  iscmet3lem2  24454  ivthlem2  24614  ovolmge0  24639  itg2seq  24905  limciun  25056  dvres  25073  dveflem  25141  lhop1  25176  ftc1lem6  25203  mdegnn0cl  25234  aalioulem6  25495  lgsqrmod  26498  gausslemma2dlem3  26514  2sqreulem1  26592  2sqreunnlem1  26595  2sqreulem3  26599  pntlem3  26755  axlowdimlem16  27323  axcontlem12  27341  umgrislfupgrlem  27490  uhgr2edg  27573  ushgredgedg  27594  ushgredgedgloop  27596  nbuhgr2vtx1edgb  27717  edgnbusgreu  27732  usgredgsscusgredg  27824  wlkdlem2  28048  pthdivtx  28093  upgrwlkdvdelem  28100  spthonepeq  28116  pthdlem1  28130  wwlksnprcl  28200  wlknewwlksn  28248  clwlkclwwlklem2a4  28357  clwlkclwwlklem2  28360  clwwlkwwlksb  28414  clwwlknun  28472  uhgr3cyclexlem  28541  eucrctshift  28603  frgrncvvdeqlem2  28660  frgrncvvdeqlem9  28667  numclwwlk1lem2foa  28714  numclwwlk1lem2f1  28717  ubthlem2  29229  shsvs  29681  mdsl2i  30680  mdsl2bi  30681  mdslmd1lem1  30683  atss  30704  chcv1  30713  chrelat2i  30723  atexch  30739  cdj3lem1  30792  bian1d  30805  disjxpin  30923  fpwrelmap  31064  nn0min  31130  sigaclci  32096  dya2iocuni  32246  omssubadd  32263  fnrelpredd  33057  hashfundm  33070  umgr2cycllem  33098  subfacp1lem6  33143  fmlasuc  33344  satffunlem  33359  satffunlem1lem1  33360  satffunlem2lem1  33362  mthmblem  33538  dfon2lem6  33760  naddelim  33834  sltlpss  34083  dfrdg4  34249  altopth2  34264  cgrtriv  34300  cgrextend  34306  lineext  34374  btwnconn1  34399  colinbtwnle  34416  trer  34501  elicc3  34502  poimirlem27  35800  poimirlem29  35802  poimir  35806  itg2addnc  35827  ftc1cnnc  35845  areacirclem1  35861  prnc  36221  ispridlc  36224  lcvexchlem4  37047  lcvexchlem5  37048  lkrss2N  37179  cvrnbtwn  37281  hlrelat2  37413  atle  37446  lvolex3N  37548  lplnnlelln  37553  llncvrlpln2  37567  lvolnlelln  37594  lvolnlelpln  37595  lplncvrlvol2  37625  snatpsubN  37760  linepsubN  37762  pmodlem2  37857  linepsubclN  37961  dihatexv  39348  eldioph2b  40582  pell1234qrreccl  40673  islssfg2  40893  hbtlem2  40946  clss2lem  41189  clsk1indlem3  41623  mnuop3d  41859  sspwtrALT2  42413  fcoresf1  44531  2reu3  44570  2reu8i  44573  elsetpreimafvbi  44812  iccpartres  44839  iccpartiltu  44843  icceuelpart  44857  sprsymrelfvlem  44911  prpair  44922  prproropf1olem4  44927  prprelb  44937  goldbachthlem2  44967  lighneallem4  45031  requad2  45044  sbgoldbwt  45198  sbgoldbst  45199  nnsum4primesoddALTV  45218  nnsum4primeseven  45221  nnsum4primesevenALTV  45222  bgoldbtbndlem2  45227  mgmpropd  45298  rnghmsubcsetclem2  45503  funcrngcsetc  45525  rhmsubcsetclem2  45549  rhmsubcrngclem2  45555  funcringcsetc  45562  srhmsubc  45603  rhmsubclem4  45616  srhmsubcALTV  45621  rhmsubcALTVlem4  45634  ztprmneprm  45652  pgrpgt2nabl  45671  snlindsntor  45781  elbigo2  45867  eenglngeehlnm  46054  itschlc0yqe  46075  itscnhlc0xyqsol  46080  itsclc0  46086  itsclquadeu  46092