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  620  jaoa  957  dedlema  1045  dedlemb  1046  prlem1  1054  dfsb1  2484  elneeldif  3977  unineq  4294  2nreu  4450  3elpr2eq  4911  tz7.7  6412  ordsssuc2  6477  fpropnf1  7287  nnsuc  7905  releldmdifi  8069  el2mpocsbcl  8109  poxp  8152  suppimacnv  8198  ressuppss  8207  onnseq  8383  tz7.49  8484  oaass  8598  omordi  8603  nnmordi  8668  naddelim  8723  eroprf  8854  xpdom2  9106  unfi  9210  infsupprpr  9542  inf3lem2  9667  trcl  9766  r1pwss  9822  cardaleph  10127  dfac2b  10169  axcc4  10477  acncc  10478  zorn2lem7  10540  iundom2g  10578  cfpwsdom  10622  grothomex  10867  ltexprlem2  11075  1re  11259  00id  11434  mulge0  11779  nn0ge2m1nn  12594  zle0orge1  12628  xrlttr  13179  xmullem2  13304  snunioo  13515  fzen  13578  eluzgtdifelfzo  13763  ssfzo12bi  13797  modirr  13980  hashfundm  14478  hash2pr  14505  hash3tr  14527  hash3tpde  14529  cshf1  14845  cshweqrep  14856  limsupbnd2  15516  climrlim2  15580  climuni  15585  mulcn2  15629  serf0  15714  cvgcmp  15849  ntrivcvg  15930  smuval2  16516  dfgcd2  16580  lcmgcdlem  16640  lcmdvds  16642  lcmf  16667  qnumdencl  16773  infpnlem1  16944  ram0  17056  prmgaplem6  17090  prmgaplem7  17091  prmlem1  17142  prmlem2  17154  setsstruct  17210  catass  17731  inveq  17822  sscfn1  17865  catsubcat  17890  subccocl  17896  funcco  17922  initoeu2  18070  funcestrcsetclem8  18203  funcsetcestrclem8  18218  mgmpropd  18677  gsmsymgrfixlem1  19460  psgnran  19548  efgi  19752  efgi2  19758  cntzcmnss  19874  telgsumfzs  20022  dprddisj2  20074  rnghmsubcsetclem2  20649  funcrngcsetc  20657  rhmsubcsetclem2  20678  rhmsubcrngclem2  20684  funcringcsetc  20691  srhmsubc  20697  rhmsubclem4  20705  rnglidlmcl  21244  prmirredlem  21501  psgnghm  21616  scmatghm  22555  cpmatacl  22738  pm2mpf1  22821  fvmptnn04if  22871  lmcls  23326  isfild  23882  flffbas  24019  cnpflf2  24024  qustgplem  24145  tngngp3  24693  reperflem  24854  nmhmcn  25167  iscau2  25325  iscmet3lem2  25340  ivthlem2  25501  ovolmge0  25526  itg2seq  25792  limciun  25944  dvres  25961  dveflem  26032  lhop1  26068  ftc1lem6  26097  mdegnn0cl  26125  aalioulem6  26394  lgsqrmod  27411  gausslemma2dlem3  27427  2sqreulem1  27505  2sqreunnlem1  27508  2sqreulem3  27512  pntlem3  27668  sltlpss  27960  axlowdimlem16  28987  axcontlem12  29005  umgrislfupgrlem  29154  uhgr2edg  29240  ushgredgedg  29261  ushgredgedgloop  29263  nbuhgr2vtx1edgb  29384  edgnbusgreu  29399  usgredgsscusgredg  29492  wlkdlem2  29716  pthdivtx  29762  upgrwlkdvdelem  29769  spthonepeq  29785  pthdlem1  29799  wwlksnprcl  29869  wlknewwlksn  29917  clwlkclwwlklem2a4  30026  clwlkclwwlklem2  30029  clwwlkwwlksb  30083  clwwlknun  30141  uhgr3cyclexlem  30210  eucrctshift  30272  frgrncvvdeqlem2  30329  frgrncvvdeqlem9  30336  numclwwlk1lem2foa  30383  numclwwlk1lem2f1  30386  ubthlem2  30900  shsvs  31352  mdsl2i  32351  mdsl2bi  32352  mdslmd1lem1  32354  atss  32375  chcv1  32384  chrelat2i  32394  atexch  32410  cdj3lem1  32463  bian1dOLD  32485  disjxpin  32608  fpwrelmap  32751  nn0min  32827  sigaclci  34113  dya2iocuni  34265  omssubadd  34282  fnrelpredd  35082  umgr2cycllem  35125  subfacp1lem6  35170  fmlasuc  35371  satffunlem  35386  satffunlem1lem1  35387  satffunlem2lem1  35389  mthmblem  35565  dfon2lem6  35770  dfrdg4  35933  altopth2  35948  cgrtriv  35984  cgrextend  35990  lineext  36058  btwnconn1  36083  colinbtwnle  36100  trer  36299  elicc3  36300  poimirlem27  37634  poimirlem29  37636  poimir  37640  itg2addnc  37661  ftc1cnnc  37679  areacirclem1  37695  prnc  38054  ispridlc  38057  refressn  38425  lcvexchlem4  39019  lcvexchlem5  39020  lkrss2N  39151  cvrnbtwn  39253  hlrelat2  39386  atle  39419  lvolex3N  39521  lplnnlelln  39526  llncvrlpln2  39540  lvolnlelln  39567  lvolnlelpln  39568  lplncvrlvol2  39598  snatpsubN  39733  linepsubN  39735  pmodlem2  39830  linepsubclN  39934  dihatexv  41321  eldioph2b  42751  pell1234qrreccl  42842  islssfg2  43060  hbtlem2  43113  onexomgt  43230  cantnfresb  43314  clss2lem  43601  clsk1indlem3  44033  mnuop3d  44267  sspwtrALT2  44821  fcoresf1  47019  2reu3  47060  2reu8i  47063  elsetpreimafvbi  47316  iccpartres  47343  iccpartiltu  47347  icceuelpart  47361  sprsymrelfvlem  47415  prpair  47426  prproropf1olem4  47431  prprelb  47441  goldbachthlem2  47471  lighneallem4  47535  requad2  47548  sbgoldbwt  47702  sbgoldbst  47703  nnsum4primesoddALTV  47722  nnsum4primeseven  47725  nnsum4primesevenALTV  47726  bgoldbtbndlem2  47731  uhgrimisgrgric  47837  grtriprop  47846  isubgr3stgrlem4  47872  isubgr3stgrlem6  47874  uspgrlimlem4  47894  rhmsubcALTVlem4  48128  srhmsubcALTV  48169  ztprmneprm  48192  pgrpgt2nabl  48211  snlindsntor  48317  elbigo2  48402  eenglngeehlnm  48589  itschlc0yqe  48610  itscnhlc0xyqsol  48615  itsclc0  48621  itsclquadeu  48627