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  2485  elneeldif  3915  unineq  4240  2nreu  4396  3elpr2eq  4862  tz7.7  6343  ordsssuc2  6410  fpropnf1  7213  nnsuc  7826  releldmdifi  7989  el2mpocsbcl  8027  poxp  8070  suppimacnv  8116  ressuppss  8125  onnseq  8276  tz7.49  8376  oaass  8488  omordi  8493  nnmordi  8559  naddelim  8614  eroprf  8752  xpdom2  9000  unfi  9095  infsupprpr  9409  inf3lem2  9538  trcl  9637  r1pwss  9696  cardaleph  9999  dfac2b  10041  axcc4  10349  acncc  10350  zorn2lem7  10412  iundom2g  10450  cfpwsdom  10495  grothomex  10740  ltexprlem2  10948  1re  11132  00id  11308  mulge0  11655  nn0ge2m1nn  12471  zle0orge1  12505  xrlttr  13054  xmullem2  13180  snunioo  13394  fzen  13457  eluzgtdifelfzo  13643  ssfzo12bi  13677  modirr  13865  hashfundm  14365  hash2pr  14392  hash3tr  14414  hash3tpde  14416  cshf1  14733  cshweqrep  14744  limsupbnd2  15406  climrlim2  15470  climuni  15475  mulcn2  15519  serf0  15604  cvgcmp  15739  ntrivcvg  15820  smuval2  16409  dfgcd2  16473  lcmgcdlem  16533  lcmdvds  16535  lcmf  16560  qnumdencl  16666  infpnlem1  16838  ram0  16950  prmgaplem6  16984  prmgaplem7  16985  prmlem1  17035  prmlem2  17047  setsstruct  17103  catass  17609  inveq  17698  sscfn1  17741  catsubcat  17763  subccocl  17769  funcco  17795  initoeu2  17940  funcestrcsetclem8  18070  funcsetcestrclem8  18085  mgmpropd  18576  gsmsymgrfixlem1  19356  psgnran  19444  efgi  19648  efgi2  19654  cntzcmnss  19770  telgsumfzs  19918  dprddisj2  19970  rnghmsubcsetclem2  20565  funcrngcsetc  20573  rhmsubcsetclem2  20594  rhmsubcrngclem2  20600  funcringcsetc  20607  srhmsubc  20613  rhmsubclem4  20621  rnglidlmcl  21171  prmirredlem  21427  psgnghm  21535  scmatghm  22477  cpmatacl  22660  pm2mpf1  22743  fvmptnn04if  22793  lmcls  23246  isfild  23802  flffbas  23939  cnpflf2  23944  qustgplem  24065  tngngp3  24600  reperflem  24763  nmhmcn  25076  iscau2  25233  iscmet3lem2  25248  ivthlem2  25409  ovolmge0  25434  itg2seq  25699  limciun  25851  dvres  25868  dveflem  25939  lhop1  25975  ftc1lem6  26004  mdegnn0cl  26032  aalioulem6  26301  lgsqrmod  27319  gausslemma2dlem3  27335  2sqreulem1  27413  2sqreunnlem1  27416  2sqreulem3  27420  pntlem3  27576  ltslpss  27904  axlowdimlem16  29030  axcontlem12  29048  umgrislfupgrlem  29195  uhgr2edg  29281  ushgredgedg  29302  ushgredgedgloop  29304  nbuhgr2vtx1edgb  29425  edgnbusgreu  29440  usgredgsscusgredg  29533  wlkdlem2  29755  pthdivtx  29800  upgrwlkdvdelem  29809  spthonepeq  29825  pthdlem1  29839  wwlksnprcl  29912  wlknewwlksn  29960  clwlkclwwlklem2a4  30072  clwlkclwwlklem2  30075  clwwlkwwlksb  30129  clwwlknun  30187  uhgr3cyclexlem  30256  eucrctshift  30318  frgrncvvdeqlem2  30375  frgrncvvdeqlem9  30382  numclwwlk1lem2foa  30429  numclwwlk1lem2f1  30432  ubthlem2  30946  shsvs  31398  mdsl2i  32397  mdsl2bi  32398  mdslmd1lem1  32400  atss  32421  chcv1  32430  chrelat2i  32440  atexch  32456  cdj3lem1  32509  bian1dOLD  32531  disjxpin  32663  fpwrelmap  32812  nn0min  32901  sigaclci  34289  dya2iocuni  34440  omssubadd  34457  fnrelpredd  35247  umgr2cycllem  35334  subfacp1lem6  35379  fmlasuc  35580  satffunlem  35595  satffunlem1lem1  35596  satffunlem2lem1  35598  mthmblem  35774  dfon2lem6  35980  dfrdg4  36145  altopth2  36160  cgrtriv  36196  cgrextend  36202  lineext  36270  btwnconn1  36295  colinbtwnle  36312  trer  36510  elicc3  36511  poimirlem27  37848  poimirlem29  37850  poimir  37854  itg2addnc  37875  ftc1cnnc  37893  areacirclem1  37909  prnc  38268  ispridlc  38271  refressn  38706  lcvexchlem4  39297  lcvexchlem5  39298  lkrss2N  39429  cvrnbtwn  39531  hlrelat2  39663  atle  39696  lvolex3N  39798  lplnnlelln  39803  llncvrlpln2  39817  lvolnlelln  39844  lvolnlelpln  39845  lplncvrlvol2  39875  snatpsubN  40010  linepsubN  40012  pmodlem2  40107  linepsubclN  40211  dihatexv  41598  eldioph2b  43005  pell1234qrreccl  43096  islssfg2  43313  hbtlem2  43366  onexomgt  43483  cantnfresb  43566  clss2lem  43852  clsk1indlem3  44284  mnuop3d  44512  sspwtrALT2  45063  relpfrlem  45194  fcoresf1  47315  2reu3  47356  2reu8i  47359  elsetpreimafvbi  47637  iccpartres  47664  iccpartiltu  47668  icceuelpart  47682  sprsymrelfvlem  47736  prpair  47747  prproropf1olem4  47752  prprelb  47762  goldbachthlem2  47792  lighneallem4  47856  requad2  47869  sbgoldbwt  48023  sbgoldbst  48024  nnsum4primesoddALTV  48043  nnsum4primeseven  48046  nnsum4primesevenALTV  48047  bgoldbtbndlem2  48052  uhgrimisgrgric  48177  grtriprop  48187  isubgr3stgrlem4  48215  isubgr3stgrlem6  48217  uspgrlimlem4  48237  grlimedgclnbgr  48241  grlimprclnbgrvtx  48245  gpgedg2ov  48312  gpgedg2iv  48313  pgnbgreunbgrlem1  48359  pgnbgreunbgrlem2  48363  pgnbgreunbgrlem4  48365  pgnbgreunbgrlem5  48369  rhmsubcALTVlem4  48530  srhmsubcALTV  48571  ztprmneprm  48593  pgrpgt2nabl  48612  snlindsntor  48717  elbigo2  48798  eenglngeehlnm  48985  itschlc0yqe  49006  itscnhlc0xyqsol  49011  itsclc0  49017  itsclquadeu  49023