Theorem adantld 493

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

Syntax hints:   → wi 4   ∧ wa 398

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 209  df-an 399

This theorem is referenced by:  im2anan9  621  jaoa  952  dedlema  1040  dedlemb  1041  prlem1  1049  dfsb1  2510  elneeldif  3952  unineq  4256  2nreu  4395  3elpr2eq  4839  tz7.7  6219  ordsssuc2  6281  fpropnf1  7027  nnsuc  7599  releldmdifi  7746  el2mpocsbcl  7782  poxp  7824  suppimacnv  7843  ressuppss  7851  imacosuppOLD  7877  onnseq  7983  tz7.49  8083  oaass  8189  omordi  8194  nnmordi  8259  eroprf  8397  xpdom2  8614  infsupprpr  8970  inf3lem2  9094  trcl  9172  r1pwss  9215  cardaleph  9517  dfac2b  9558  axcc4  9863  acncc  9864  zorn2lem7  9926  iundom2g  9964  cfpwsdom  10008  grothomex  10253  ltexprlem2  10461  1re  10643  00id  10817  mulge0  11160  nn0ge2m1nn  11967  zle0orge1  12001  xrlttr  12536  xmullem2  12661  snunioo  12867  fzen  12927  eluzgtdifelfzo  13102  ssfzo12bi  13135  modirr  13313  hash2pr  13830  hash3tr  13851  cshf1  14174  cshweqrep  14185  limsupbnd2  14842  climrlim2  14906  climuni  14911  mulcn2  14954  serf0  15039  cvgcmp  15173  ntrivcvg  15255  smuval2  15833  dfgcd2  15896  lcmgcdlem  15952  lcmdvds  15954  lcmf  15979  qnumdencl  16081  infpnlem1  16248  ram0  16360  prmgaplem6  16394  prmgaplem7  16395  prmlem1  16443  prmlem2  16455  setsstruct  16525  catass  16959  inveq  17046  sscfn1  17089  catsubcat  17111  subccocl  17117  funcco  17143  initoeu2  17278  funcestrcsetclem8  17399  funcsetcestrclem8  17414  gsmsymgrfixlem1  18557  psgnran  18645  efgi  18847  efgi2  18853  cntzcmnss  18963  telgsumfzs  19111  dprddisj2  19163  prmirredlem  20642  psgnghm  20726  scmatghm  21144  cpmatacl  21326  pm2mpf1  21409  fvmptnn04if  21459  lmcls  21912  isfild  22468  flffbas  22605  cnpflf2  22610  qustgplem  22731  tngngp3  23267  reperflem  23428  nmhmcn  23726  iscau2  23882  iscmet3lem2  23897  ivthlem2  24055  ovolmge0  24080  itg2seq  24345  limciun  24494  dvres  24511  dveflem  24578  lhop1  24613  ftc1lem6  24640  mdegnn0cl  24667  aalioulem6  24928  lgsqrmod  25930  gausslemma2dlem3  25946  2sqreulem1  26024  2sqreunnlem1  26027  2sqreulem3  26031  pntlem3  26187  axlowdimlem16  26745  axcontlem12  26763  umgrislfupgrlem  26909  uhgr2edg  26992  ushgredgedg  27013  ushgredgedgloop  27015  nbuhgr2vtx1edgb  27136  edgnbusgreu  27151  usgredgsscusgredg  27243  wlkdlem2  27467  pthdivtx  27512  upgrwlkdvdelem  27519  spthonepeq  27535  pthdlem1  27549  wwlksnprcl  27619  wlknewwlksn  27667  clwlkclwwlklem2a4  27777  clwlkclwwlklem2  27780  clwwlkwwlksb  27835  clwwlknun  27893  uhgr3cyclexlem  27962  eucrctshift  28024  frgrncvvdeqlem2  28081  frgrncvvdeqlem9  28088  numclwwlk1lem2foa  28135  numclwwlk1lem2f1  28138  ubthlem2  28650  shsvs  29102  mdsl2i  30101  mdsl2bi  30102  mdslmd1lem1  30104  atss  30125  chcv1  30134  chrelat2i  30144  atexch  30160  cdj3lem1  30213  bian1d  30226  disjxpin  30340  fpwrelmap  30471  nn0min  30538  sigaclci  31393  dya2iocuni  31543  omssubadd  31560  hashfundm  32356  umgr2cycllem  32389  subfacp1lem6  32434  fmlasuc  32635  satffunlem  32650  satffunlem1lem1  32651  satffunlem2lem1  32653  mthmblem  32829  dfon2lem6  33035  dfrdg4  33414  altopth2  33429  cgrtriv  33465  cgrextend  33471  lineext  33539  btwnconn1  33564  colinbtwnle  33581  trer  33666  elicc3  33667  poimirlem27  34921  poimirlem29  34923  poimir  34927  itg2addnc  34948  ftc1cnnc  34968  areacirclem1  34984  prnc  35347  ispridlc  35350  lcvexchlem4  36175  lcvexchlem5  36176  lkrss2N  36307  cvrnbtwn  36409  hlrelat2  36541  atle  36574  lvolex3N  36676  lplnnlelln  36681  llncvrlpln2  36695  lvolnlelln  36722  lvolnlelpln  36723  lplncvrlvol2  36753  snatpsubN  36888  linepsubN  36890  pmodlem2  36985  linepsubclN  37089  dihatexv  38476  eldioph2b  39367  pell1234qrreccl  39458  islssfg2  39678  hbtlem2  39731  clss2lem  39978  clsk1indlem3  40400  mnuop3d  40614  sspwtrALT2  41164  2reu3  43316  2reu8i  43319  elsetpreimafvbi  43558  iccpartres  43585  iccpartiltu  43589  icceuelpart  43603  sprsymrelfvlem  43659  prpair  43670  prproropf1olem4  43675  prprelb  43685  goldbachthlem2  43715  lighneallem4  43782  requad2  43795  sbgoldbwt  43949  sbgoldbst  43950  nnsum4primesoddALTV  43969  nnsum4primeseven  43972  nnsum4primesevenALTV  43973  bgoldbtbndlem2  43978  mgmpropd  44049  rnghmsubcsetclem2  44254  funcrngcsetc  44276  rhmsubcsetclem2  44300  rhmsubcrngclem2  44306  funcringcsetc  44313  srhmsubc  44354  rhmsubclem4  44367  srhmsubcALTV  44372  rhmsubcALTVlem4  44385  ztprmneprm  44402  pgrpgt2nabl  44421  snlindsntor  44533  elbigo2  44619  eenglngeehlnm  44733  itschlc0yqe  44754  itscnhlc0xyqsol  44759  itsclc0  44765  itsclquadeu  44771