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  2481  elneeldif  3911  unineq  4233  2nreu  4389  3elpr2eq  4853  tz7.7  6327  ordsssuc2  6394  fpropnf1  7196  nnsuc  7809  releldmdifi  7972  el2mpocsbcl  8010  poxp  8053  suppimacnv  8099  ressuppss  8108  onnseq  8259  tz7.49  8359  oaass  8471  omordi  8476  nnmordi  8541  naddelim  8596  eroprf  8734  xpdom2  8980  unfi  9075  infsupprpr  9385  inf3lem2  9514  trcl  9613  r1pwss  9672  cardaleph  9975  dfac2b  10017  axcc4  10325  acncc  10326  zorn2lem7  10388  iundom2g  10426  cfpwsdom  10470  grothomex  10715  ltexprlem2  10923  1re  11107  00id  11283  mulge0  11630  nn0ge2m1nn  12446  zle0orge1  12480  xrlttr  13034  xmullem2  13159  snunioo  13373  fzen  13436  eluzgtdifelfzo  13622  ssfzo12bi  13656  modirr  13844  hashfundm  14344  hash2pr  14371  hash3tr  14393  hash3tpde  14395  cshf1  14712  cshweqrep  14723  limsupbnd2  15385  climrlim2  15449  climuni  15454  mulcn2  15498  serf0  15583  cvgcmp  15718  ntrivcvg  15799  smuval2  16388  dfgcd2  16452  lcmgcdlem  16512  lcmdvds  16514  lcmf  16539  qnumdencl  16645  infpnlem1  16817  ram0  16929  prmgaplem6  16963  prmgaplem7  16964  prmlem1  17014  prmlem2  17026  setsstruct  17082  catass  17587  inveq  17676  sscfn1  17719  catsubcat  17741  subccocl  17747  funcco  17773  initoeu2  17918  funcestrcsetclem8  18048  funcsetcestrclem8  18063  mgmpropd  18554  gsmsymgrfixlem1  19334  psgnran  19422  efgi  19626  efgi2  19632  cntzcmnss  19748  telgsumfzs  19896  dprddisj2  19948  rnghmsubcsetclem2  20542  funcrngcsetc  20550  rhmsubcsetclem2  20571  rhmsubcrngclem2  20577  funcringcsetc  20584  srhmsubc  20590  rhmsubclem4  20598  rnglidlmcl  21148  prmirredlem  21404  psgnghm  21512  scmatghm  22443  cpmatacl  22626  pm2mpf1  22709  fvmptnn04if  22759  lmcls  23212  isfild  23768  flffbas  23905  cnpflf2  23910  qustgplem  24031  tngngp3  24566  reperflem  24729  nmhmcn  25042  iscau2  25199  iscmet3lem2  25214  ivthlem2  25375  ovolmge0  25400  itg2seq  25665  limciun  25817  dvres  25834  dveflem  25905  lhop1  25941  ftc1lem6  25970  mdegnn0cl  25998  aalioulem6  26267  lgsqrmod  27285  gausslemma2dlem3  27301  2sqreulem1  27379  2sqreunnlem1  27382  2sqreulem3  27386  pntlem3  27542  sltlpss  27848  axlowdimlem16  28930  axcontlem12  28948  umgrislfupgrlem  29095  uhgr2edg  29181  ushgredgedg  29202  ushgredgedgloop  29204  nbuhgr2vtx1edgb  29325  edgnbusgreu  29340  usgredgsscusgredg  29433  wlkdlem2  29655  pthdivtx  29700  upgrwlkdvdelem  29709  spthonepeq  29725  pthdlem1  29739  wwlksnprcl  29812  wlknewwlksn  29860  clwlkclwwlklem2a4  29969  clwlkclwwlklem2  29972  clwwlkwwlksb  30026  clwwlknun  30084  uhgr3cyclexlem  30153  eucrctshift  30215  frgrncvvdeqlem2  30272  frgrncvvdeqlem9  30279  numclwwlk1lem2foa  30326  numclwwlk1lem2f1  30329  ubthlem2  30843  shsvs  31295  mdsl2i  32294  mdsl2bi  32295  mdslmd1lem1  32297  atss  32318  chcv1  32327  chrelat2i  32337  atexch  32353  cdj3lem1  32406  bian1dOLD  32428  disjxpin  32560  fpwrelmap  32708  nn0min  32795  sigaclci  34137  dya2iocuni  34288  omssubadd  34305  fnrelpredd  35094  umgr2cycllem  35176  subfacp1lem6  35221  fmlasuc  35422  satffunlem  35437  satffunlem1lem1  35438  satffunlem2lem1  35440  mthmblem  35616  dfon2lem6  35822  dfrdg4  35985  altopth2  36000  cgrtriv  36036  cgrextend  36042  lineext  36110  btwnconn1  36135  colinbtwnle  36152  trer  36350  elicc3  36351  poimirlem27  37687  poimirlem29  37689  poimir  37693  itg2addnc  37714  ftc1cnnc  37732  areacirclem1  37748  prnc  38107  ispridlc  38110  refressn  38480  lcvexchlem4  39076  lcvexchlem5  39077  lkrss2N  39208  cvrnbtwn  39310  hlrelat2  39442  atle  39475  lvolex3N  39577  lplnnlelln  39582  llncvrlpln2  39596  lvolnlelln  39623  lvolnlelpln  39624  lplncvrlvol2  39654  snatpsubN  39789  linepsubN  39791  pmodlem2  39886  linepsubclN  39990  dihatexv  41377  eldioph2b  42796  pell1234qrreccl  42887  islssfg2  43104  hbtlem2  43157  onexomgt  43274  cantnfresb  43357  clss2lem  43644  clsk1indlem3  44076  mnuop3d  44304  sspwtrALT2  44855  relpfrlem  44986  fcoresf1  47100  2reu3  47141  2reu8i  47144  elsetpreimafvbi  47422  iccpartres  47449  iccpartiltu  47453  icceuelpart  47467  sprsymrelfvlem  47521  prpair  47532  prproropf1olem4  47537  prprelb  47547  goldbachthlem2  47577  lighneallem4  47641  requad2  47654  sbgoldbwt  47808  sbgoldbst  47809  nnsum4primesoddALTV  47828  nnsum4primeseven  47831  nnsum4primesevenALTV  47832  bgoldbtbndlem2  47837  uhgrimisgrgric  47962  grtriprop  47972  isubgr3stgrlem4  48000  isubgr3stgrlem6  48002  uspgrlimlem4  48022  grlimedgclnbgr  48026  grlimprclnbgrvtx  48030  gpgedg2ov  48097  gpgedg2iv  48098  pgnbgreunbgrlem1  48144  pgnbgreunbgrlem2  48148  pgnbgreunbgrlem4  48150  pgnbgreunbgrlem5  48154  rhmsubcALTVlem4  48315  srhmsubcALTV  48356  ztprmneprm  48378  pgrpgt2nabl  48397  snlindsntor  48503  elbigo2  48584  eenglngeehlnm  48771  itschlc0yqe  48792  itscnhlc0xyqsol  48797  itsclc0  48803  itsclquadeu  48809