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  2479  elneeldif  3925  unineq  4247  2nreu  4403  3elpr2eq  4866  tz7.7  6346  ordsssuc2  6413  fpropnf1  7224  nnsuc  7840  releldmdifi  8003  el2mpocsbcl  8041  poxp  8084  suppimacnv  8130  ressuppss  8139  onnseq  8290  tz7.49  8390  oaass  8502  omordi  8507  nnmordi  8572  naddelim  8627  eroprf  8765  xpdom2  9013  unfi  9112  infsupprpr  9433  inf3lem2  9558  trcl  9657  r1pwss  9713  cardaleph  10018  dfac2b  10060  axcc4  10368  acncc  10369  zorn2lem7  10431  iundom2g  10469  cfpwsdom  10513  grothomex  10758  ltexprlem2  10966  1re  11150  00id  11325  mulge0  11672  nn0ge2m1nn  12488  zle0orge1  12522  xrlttr  13076  xmullem2  13201  snunioo  13415  fzen  13478  eluzgtdifelfzo  13664  ssfzo12bi  13698  modirr  13883  hashfundm  14383  hash2pr  14410  hash3tr  14432  hash3tpde  14434  cshf1  14751  cshweqrep  14762  limsupbnd2  15425  climrlim2  15489  climuni  15494  mulcn2  15538  serf0  15623  cvgcmp  15758  ntrivcvg  15839  smuval2  16428  dfgcd2  16492  lcmgcdlem  16552  lcmdvds  16554  lcmf  16579  qnumdencl  16685  infpnlem1  16857  ram0  16969  prmgaplem6  17003  prmgaplem7  17004  prmlem1  17054  prmlem2  17066  setsstruct  17122  catass  17623  inveq  17712  sscfn1  17755  catsubcat  17777  subccocl  17783  funcco  17809  initoeu2  17954  funcestrcsetclem8  18084  funcsetcestrclem8  18099  mgmpropd  18554  gsmsymgrfixlem1  19333  psgnran  19421  efgi  19625  efgi2  19631  cntzcmnss  19747  telgsumfzs  19895  dprddisj2  19947  rnghmsubcsetclem2  20517  funcrngcsetc  20525  rhmsubcsetclem2  20546  rhmsubcrngclem2  20552  funcringcsetc  20559  srhmsubc  20565  rhmsubclem4  20573  rnglidlmcl  21102  prmirredlem  21358  psgnghm  21465  scmatghm  22396  cpmatacl  22579  pm2mpf1  22662  fvmptnn04if  22712  lmcls  23165  isfild  23721  flffbas  23858  cnpflf2  23863  qustgplem  23984  tngngp3  24520  reperflem  24683  nmhmcn  24996  iscau2  25153  iscmet3lem2  25168  ivthlem2  25329  ovolmge0  25354  itg2seq  25619  limciun  25771  dvres  25788  dveflem  25859  lhop1  25895  ftc1lem6  25924  mdegnn0cl  25952  aalioulem6  26221  lgsqrmod  27239  gausslemma2dlem3  27255  2sqreulem1  27333  2sqreunnlem1  27336  2sqreulem3  27340  pntlem3  27496  sltlpss  27795  axlowdimlem16  28860  axcontlem12  28878  umgrislfupgrlem  29025  uhgr2edg  29111  ushgredgedg  29132  ushgredgedgloop  29134  nbuhgr2vtx1edgb  29255  edgnbusgreu  29270  usgredgsscusgredg  29363  wlkdlem2  29585  pthdivtx  29630  upgrwlkdvdelem  29639  spthonepeq  29655  pthdlem1  29669  wwlksnprcl  29742  wlknewwlksn  29790  clwlkclwwlklem2a4  29899  clwlkclwwlklem2  29902  clwwlkwwlksb  29956  clwwlknun  30014  uhgr3cyclexlem  30083  eucrctshift  30145  frgrncvvdeqlem2  30202  frgrncvvdeqlem9  30209  numclwwlk1lem2foa  30256  numclwwlk1lem2f1  30259  ubthlem2  30773  shsvs  31225  mdsl2i  32224  mdsl2bi  32225  mdslmd1lem1  32227  atss  32248  chcv1  32257  chrelat2i  32267  atexch  32283  cdj3lem1  32336  bian1dOLD  32359  disjxpin  32490  fpwrelmap  32629  nn0min  32718  sigaclci  34095  dya2iocuni  34247  omssubadd  34264  fnrelpredd  35052  umgr2cycllem  35100  subfacp1lem6  35145  fmlasuc  35346  satffunlem  35361  satffunlem1lem1  35362  satffunlem2lem1  35364  mthmblem  35540  dfon2lem6  35749  dfrdg4  35912  altopth2  35927  cgrtriv  35963  cgrextend  35969  lineext  36037  btwnconn1  36062  colinbtwnle  36079  trer  36277  elicc3  36278  poimirlem27  37614  poimirlem29  37616  poimir  37620  itg2addnc  37641  ftc1cnnc  37659  areacirclem1  37675  prnc  38034  ispridlc  38037  refressn  38407  lcvexchlem4  39003  lcvexchlem5  39004  lkrss2N  39135  cvrnbtwn  39237  hlrelat2  39370  atle  39403  lvolex3N  39505  lplnnlelln  39510  llncvrlpln2  39524  lvolnlelln  39551  lvolnlelpln  39552  lplncvrlvol2  39582  snatpsubN  39717  linepsubN  39719  pmodlem2  39814  linepsubclN  39918  dihatexv  41305  eldioph2b  42724  pell1234qrreccl  42815  islssfg2  43033  hbtlem2  43086  onexomgt  43203  cantnfresb  43286  clss2lem  43573  clsk1indlem3  44005  mnuop3d  44233  sspwtrALT2  44785  relpfrlem  44916  fcoresf1  47043  2reu3  47084  2reu8i  47087  elsetpreimafvbi  47365  iccpartres  47392  iccpartiltu  47396  icceuelpart  47410  sprsymrelfvlem  47464  prpair  47475  prproropf1olem4  47480  prprelb  47490  goldbachthlem2  47520  lighneallem4  47584  requad2  47597  sbgoldbwt  47751  sbgoldbst  47752  nnsum4primesoddALTV  47771  nnsum4primeseven  47774  nnsum4primesevenALTV  47775  bgoldbtbndlem2  47780  uhgrimisgrgric  47904  grtriprop  47913  isubgr3stgrlem4  47941  isubgr3stgrlem6  47943  uspgrlimlem4  47963  gpgedg2ov  48030  gpgedg2iv  48031  pgnbgreunbgrlem1  48076  pgnbgreunbgrlem2  48080  pgnbgreunbgrlem4  48082  pgnbgreunbgrlem5  48086  rhmsubcALTVlem4  48245  srhmsubcALTV  48286  ztprmneprm  48308  pgrpgt2nabl  48327  snlindsntor  48433  elbigo2  48514  eenglngeehlnm  48701  itschlc0yqe  48722  itscnhlc0xyqsol  48727  itsclc0  48733  itsclquadeu  48739