Theorem adantld 489

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

Syntax hints:   → wi 4   ∧ wa 394

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 395

This theorem is referenced by:  im2anan9  618  jaoa  953  dedlema  1043  dedlemb  1044  prlem1  1052  dfsb1  2475  elneeldif  3963  unineq  4280  2nreu  4445  3elpr2eq  4911  tz7.7  6400  ordsssuc2  6465  fpropnf1  7283  nnsuc  7894  releldmdifi  8055  el2mpocsbcl  8096  poxp  8139  suppimacnv  8185  ressuppss  8194  onnseq  8371  tz7.49  8472  oaass  8588  omordi  8593  nnmordi  8658  naddelim  8713  eroprf  8840  xpdom2  9098  unfi  9203  infsupprpr  9535  inf3lem2  9660  trcl  9759  r1pwss  9815  cardaleph  10120  dfac2b  10161  axcc4  10470  acncc  10471  zorn2lem7  10533  iundom2g  10571  cfpwsdom  10615  grothomex  10860  ltexprlem2  11068  1re  11252  00id  11427  mulge0  11770  nn0ge2m1nn  12579  zle0orge1  12613  xrlttr  13159  xmullem2  13284  snunioo  13495  fzen  13558  eluzgtdifelfzo  13734  ssfzo12bi  13767  modirr  13947  hashfundm  14441  hash2pr  14470  hash3tr  14491  cshf1  14800  cshweqrep  14811  limsupbnd2  15467  climrlim2  15531  climuni  15536  mulcn2  15580  serf0  15667  cvgcmp  15802  ntrivcvg  15883  smuval2  16464  dfgcd2  16529  lcmgcdlem  16584  lcmdvds  16586  lcmf  16611  qnumdencl  16718  infpnlem1  16886  ram0  16998  prmgaplem6  17032  prmgaplem7  17033  prmlem1  17084  prmlem2  17096  setsstruct  17152  catass  17673  inveq  17764  sscfn1  17807  catsubcat  17832  subccocl  17838  funcco  17864  initoeu2  18012  funcestrcsetclem8  18145  funcsetcestrclem8  18160  mgmpropd  18618  gsmsymgrfixlem1  19389  psgnran  19477  efgi  19681  efgi2  19687  cntzcmnss  19803  telgsumfzs  19951  dprddisj2  20003  rnghmsubcsetclem2  20572  funcrngcsetc  20580  rhmsubcsetclem2  20601  rhmsubcrngclem2  20607  funcringcsetc  20614  srhmsubc  20620  rhmsubclem4  20628  rnglidlmcl  21119  prmirredlem  21405  psgnghm  21519  scmatghm  22455  cpmatacl  22638  pm2mpf1  22721  fvmptnn04if  22771  lmcls  23226  isfild  23782  flffbas  23919  cnpflf2  23924  qustgplem  24045  tngngp3  24593  reperflem  24754  nmhmcn  25067  iscau2  25225  iscmet3lem2  25240  ivthlem2  25401  ovolmge0  25426  itg2seq  25692  limciun  25843  dvres  25860  dveflem  25931  lhop1  25967  ftc1lem6  25996  mdegnn0cl  26027  aalioulem6  26292  lgsqrmod  27305  gausslemma2dlem3  27321  2sqreulem1  27399  2sqreunnlem1  27402  2sqreulem3  27406  pntlem3  27562  sltlpss  27853  axlowdimlem16  28788  axcontlem12  28806  umgrislfupgrlem  28955  uhgr2edg  29041  ushgredgedg  29062  ushgredgedgloop  29064  nbuhgr2vtx1edgb  29185  edgnbusgreu  29200  usgredgsscusgredg  29293  wlkdlem2  29517  pthdivtx  29563  upgrwlkdvdelem  29570  spthonepeq  29586  pthdlem1  29600  wwlksnprcl  29670  wlknewwlksn  29718  clwlkclwwlklem2a4  29827  clwlkclwwlklem2  29830  clwwlkwwlksb  29884  clwwlknun  29942  uhgr3cyclexlem  30011  eucrctshift  30073  frgrncvvdeqlem2  30130  frgrncvvdeqlem9  30137  numclwwlk1lem2foa  30184  numclwwlk1lem2f1  30187  ubthlem2  30701  shsvs  31153  mdsl2i  32152  mdsl2bi  32153  mdslmd1lem1  32155  atss  32176  chcv1  32185  chrelat2i  32195  atexch  32211  cdj3lem1  32264  bian1d  32277  disjxpin  32399  fpwrelmap  32536  nn0min  32604  sigaclci  33784  dya2iocuni  33936  omssubadd  33953  fnrelpredd  34745  umgr2cycllem  34783  subfacp1lem6  34828  fmlasuc  35029  satffunlem  35044  satffunlem1lem1  35045  satffunlem2lem1  35047  mthmblem  35223  dfon2lem6  35417  dfrdg4  35580  altopth2  35595  cgrtriv  35631  cgrextend  35637  lineext  35705  btwnconn1  35730  colinbtwnle  35747  trer  35833  elicc3  35834  poimirlem27  37153  poimirlem29  37155  poimir  37159  itg2addnc  37180  ftc1cnnc  37198  areacirclem1  37214  prnc  37573  ispridlc  37576  refressn  37947  lcvexchlem4  38541  lcvexchlem5  38542  lkrss2N  38673  cvrnbtwn  38775  hlrelat2  38908  atle  38941  lvolex3N  39043  lplnnlelln  39048  llncvrlpln2  39062  lvolnlelln  39089  lvolnlelpln  39090  lplncvrlvol2  39120  snatpsubN  39255  linepsubN  39257  pmodlem2  39352  linepsubclN  39456  dihatexv  40843  eldioph2b  42214  pell1234qrreccl  42305  islssfg2  42526  hbtlem2  42579  onexomgt  42700  cantnfresb  42784  clss2lem  43072  clsk1indlem3  43504  mnuop3d  43739  sspwtrALT2  44293  fcoresf1  46480  2reu3  46519  2reu8i  46522  elsetpreimafvbi  46760  iccpartres  46787  iccpartiltu  46791  icceuelpart  46805  sprsymrelfvlem  46859  prpair  46870  prproropf1olem4  46875  prprelb  46885  goldbachthlem2  46915  lighneallem4  46979  requad2  46992  sbgoldbwt  47146  sbgoldbst  47147  nnsum4primesoddALTV  47166  nnsum4primeseven  47169  nnsum4primesevenALTV  47170  bgoldbtbndlem2  47175  gricer  47268  rhmsubcALTVlem4  47424  srhmsubcALTV  47465  ztprmneprm  47489  pgrpgt2nabl  47508  snlindsntor  47617  elbigo2  47703  eenglngeehlnm  47890  itschlc0yqe  47911  itscnhlc0xyqsol  47916  itsclc0  47922  itsclquadeu  47928