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  2486  elneeldif  3945  unineq  4268  2nreu  4424  3elpr2eq  4887  tz7.7  6383  ordsssuc2  6450  fpropnf1  7265  nnsuc  7884  releldmdifi  8049  el2mpocsbcl  8089  poxp  8132  suppimacnv  8178  ressuppss  8187  onnseq  8363  tz7.49  8464  oaass  8578  omordi  8583  nnmordi  8648  naddelim  8703  eroprf  8834  xpdom2  9086  unfi  9190  infsupprpr  9523  inf3lem2  9648  trcl  9747  r1pwss  9803  cardaleph  10108  dfac2b  10150  axcc4  10458  acncc  10459  zorn2lem7  10521  iundom2g  10559  cfpwsdom  10603  grothomex  10848  ltexprlem2  11056  1re  11240  00id  11415  mulge0  11760  nn0ge2m1nn  12576  zle0orge1  12610  xrlttr  13161  xmullem2  13286  snunioo  13500  fzen  13563  eluzgtdifelfzo  13748  ssfzo12bi  13782  modirr  13965  hashfundm  14465  hash2pr  14492  hash3tr  14514  hash3tpde  14516  cshf1  14833  cshweqrep  14844  limsupbnd2  15504  climrlim2  15568  climuni  15573  mulcn2  15617  serf0  15702  cvgcmp  15837  ntrivcvg  15918  smuval2  16506  dfgcd2  16570  lcmgcdlem  16630  lcmdvds  16632  lcmf  16657  qnumdencl  16763  infpnlem1  16935  ram0  17047  prmgaplem6  17081  prmgaplem7  17082  prmlem1  17132  prmlem2  17144  setsstruct  17200  catass  17703  inveq  17792  sscfn1  17835  catsubcat  17857  subccocl  17863  funcco  17889  initoeu2  18034  funcestrcsetclem8  18164  funcsetcestrclem8  18179  mgmpropd  18634  gsmsymgrfixlem1  19413  psgnran  19501  efgi  19705  efgi2  19711  cntzcmnss  19827  telgsumfzs  19975  dprddisj2  20027  rnghmsubcsetclem2  20597  funcrngcsetc  20605  rhmsubcsetclem2  20626  rhmsubcrngclem2  20632  funcringcsetc  20639  srhmsubc  20645  rhmsubclem4  20653  rnglidlmcl  21182  prmirredlem  21438  psgnghm  21545  scmatghm  22476  cpmatacl  22659  pm2mpf1  22742  fvmptnn04if  22792  lmcls  23245  isfild  23801  flffbas  23938  cnpflf2  23943  qustgplem  24064  tngngp3  24600  reperflem  24763  nmhmcn  25076  iscau2  25234  iscmet3lem2  25249  ivthlem2  25410  ovolmge0  25435  itg2seq  25700  limciun  25852  dvres  25869  dveflem  25940  lhop1  25976  ftc1lem6  26005  mdegnn0cl  26033  aalioulem6  26302  lgsqrmod  27320  gausslemma2dlem3  27336  2sqreulem1  27414  2sqreunnlem1  27417  2sqreulem3  27421  pntlem3  27577  sltlpss  27876  axlowdimlem16  28941  axcontlem12  28959  umgrislfupgrlem  29106  uhgr2edg  29192  ushgredgedg  29213  ushgredgedgloop  29215  nbuhgr2vtx1edgb  29336  edgnbusgreu  29351  usgredgsscusgredg  29444  wlkdlem2  29668  pthdivtx  29714  upgrwlkdvdelem  29723  spthonepeq  29739  pthdlem1  29753  wwlksnprcl  29826  wlknewwlksn  29874  clwlkclwwlklem2a4  29983  clwlkclwwlklem2  29986  clwwlkwwlksb  30040  clwwlknun  30098  uhgr3cyclexlem  30167  eucrctshift  30229  frgrncvvdeqlem2  30286  frgrncvvdeqlem9  30293  numclwwlk1lem2foa  30340  numclwwlk1lem2f1  30343  ubthlem2  30857  shsvs  31309  mdsl2i  32308  mdsl2bi  32309  mdslmd1lem1  32311  atss  32332  chcv1  32341  chrelat2i  32351  atexch  32367  cdj3lem1  32420  bian1dOLD  32443  disjxpin  32574  fpwrelmap  32715  nn0min  32804  sigaclci  34168  dya2iocuni  34320  omssubadd  34337  fnrelpredd  35125  umgr2cycllem  35167  subfacp1lem6  35212  fmlasuc  35413  satffunlem  35428  satffunlem1lem1  35429  satffunlem2lem1  35431  mthmblem  35607  dfon2lem6  35811  dfrdg4  35974  altopth2  35989  cgrtriv  36025  cgrextend  36031  lineext  36099  btwnconn1  36124  colinbtwnle  36141  trer  36339  elicc3  36340  poimirlem27  37676  poimirlem29  37678  poimir  37682  itg2addnc  37703  ftc1cnnc  37721  areacirclem1  37737  prnc  38096  ispridlc  38099  refressn  38466  lcvexchlem4  39060  lcvexchlem5  39061  lkrss2N  39192  cvrnbtwn  39294  hlrelat2  39427  atle  39460  lvolex3N  39562  lplnnlelln  39567  llncvrlpln2  39581  lvolnlelln  39608  lvolnlelpln  39609  lplncvrlvol2  39639  snatpsubN  39774  linepsubN  39776  pmodlem2  39871  linepsubclN  39975  dihatexv  41362  eldioph2b  42761  pell1234qrreccl  42852  islssfg2  43070  hbtlem2  43123  onexomgt  43240  cantnfresb  43323  clss2lem  43610  clsk1indlem3  44042  mnuop3d  44270  sspwtrALT2  44822  relpfrlem  44953  fcoresf1  47078  2reu3  47119  2reu8i  47122  elsetpreimafvbi  47385  iccpartres  47412  iccpartiltu  47416  icceuelpart  47430  sprsymrelfvlem  47484  prpair  47495  prproropf1olem4  47500  prprelb  47510  goldbachthlem2  47540  lighneallem4  47604  requad2  47617  sbgoldbwt  47771  sbgoldbst  47772  nnsum4primesoddALTV  47791  nnsum4primeseven  47794  nnsum4primesevenALTV  47795  bgoldbtbndlem2  47800  uhgrimisgrgric  47924  grtriprop  47933  isubgr3stgrlem4  47961  isubgr3stgrlem6  47963  uspgrlimlem4  47983  rhmsubcALTVlem4  48239  srhmsubcALTV  48280  ztprmneprm  48302  pgrpgt2nabl  48321  snlindsntor  48427  elbigo2  48512  eenglngeehlnm  48699  itschlc0yqe  48720  itscnhlc0xyqsol  48725  itsclc0  48731  itsclquadeu  48737