Theorem adantld 491

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

Syntax hints:   → wi 4   ∧ wa 396

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 206  df-an 397

This theorem is referenced by:  im2anan9  620  jaoa  953  dedlema  1043  dedlemb  1044  prlem1  1052  dfsb1  2486  elneeldif  3902  unineq  4212  2nreu  4376  3elpr2eq  4839  tz7.7  6296  ordsssuc2  6358  fpropnf1  7149  nnsuc  7739  releldmdifi  7895  el2mpocsbcl  7934  poxp  7978  suppimacnv  7999  ressuppss  8008  onnseq  8184  tz7.49  8285  oaass  8401  omordi  8406  nnmordi  8471  eroprf  8613  xpdom2  8863  unfi  8964  infsupprpr  9272  inf3lem2  9396  trcl  9495  r1pwss  9551  cardaleph  9854  dfac2b  9895  axcc4  10204  acncc  10205  zorn2lem7  10267  iundom2g  10305  cfpwsdom  10349  grothomex  10594  ltexprlem2  10802  1re  10984  00id  11159  mulge0  11502  nn0ge2m1nn  12311  zle0orge1  12345  xrlttr  12883  xmullem2  13008  snunioo  13219  fzen  13282  eluzgtdifelfzo  13458  ssfzo12bi  13491  modirr  13671  hash2pr  14192  hash3tr  14213  cshf1  14532  cshweqrep  14543  limsupbnd2  15201  climrlim2  15265  climuni  15270  mulcn2  15314  serf0  15401  cvgcmp  15537  ntrivcvg  15618  smuval2  16198  dfgcd2  16263  lcmgcdlem  16320  lcmdvds  16322  lcmf  16347  qnumdencl  16452  infpnlem1  16620  ram0  16732  prmgaplem6  16766  prmgaplem7  16767  prmlem1  16818  prmlem2  16830  setsstruct  16886  catass  17404  inveq  17495  sscfn1  17538  catsubcat  17563  subccocl  17569  funcco  17595  initoeu2  17740  funcestrcsetclem8  17873  funcsetcestrclem8  17888  gsmsymgrfixlem1  19044  psgnran  19132  efgi  19334  efgi2  19340  cntzcmnss  19451  telgsumfzs  19599  dprddisj2  19651  prmirredlem  20703  psgnghm  20794  scmatghm  21691  cpmatacl  21874  pm2mpf1  21957  fvmptnn04if  22007  lmcls  22462  isfild  23018  flffbas  23155  cnpflf2  23160  qustgplem  23281  tngngp3  23829  reperflem  23990  nmhmcn  24292  iscau2  24450  iscmet3lem2  24465  ivthlem2  24625  ovolmge0  24650  itg2seq  24916  limciun  25067  dvres  25084  dveflem  25152  lhop1  25187  ftc1lem6  25214  mdegnn0cl  25245  aalioulem6  25506  lgsqrmod  26509  gausslemma2dlem3  26525  2sqreulem1  26603  2sqreunnlem1  26606  2sqreulem3  26610  pntlem3  26766  axlowdimlem16  27334  axcontlem12  27352  umgrislfupgrlem  27501  uhgr2edg  27584  ushgredgedg  27605  ushgredgedgloop  27607  nbuhgr2vtx1edgb  27728  edgnbusgreu  27743  usgredgsscusgredg  27835  wlkdlem2  28060  pthdivtx  28106  upgrwlkdvdelem  28113  spthonepeq  28129  pthdlem1  28143  wwlksnprcl  28213  wlknewwlksn  28261  clwlkclwwlklem2a4  28370  clwlkclwwlklem2  28373  clwwlkwwlksb  28427  clwwlknun  28485  uhgr3cyclexlem  28554  eucrctshift  28616  frgrncvvdeqlem2  28673  frgrncvvdeqlem9  28680  numclwwlk1lem2foa  28727  numclwwlk1lem2f1  28730  ubthlem2  29242  shsvs  29694  mdsl2i  30693  mdsl2bi  30694  mdslmd1lem1  30696  atss  30717  chcv1  30726  chrelat2i  30736  atexch  30752  cdj3lem1  30805  bian1d  30818  disjxpin  30936  fpwrelmap  31077  nn0min  31143  sigaclci  32109  dya2iocuni  32259  omssubadd  32276  fnrelpredd  33070  hashfundm  33083  umgr2cycllem  33111  subfacp1lem6  33156  fmlasuc  33357  satffunlem  33372  satffunlem1lem1  33373  satffunlem2lem1  33375  mthmblem  33551  dfon2lem6  33773  naddelim  33847  sltlpss  34096  dfrdg4  34262  altopth2  34277  cgrtriv  34313  cgrextend  34319  lineext  34387  btwnconn1  34412  colinbtwnle  34429  trer  34514  elicc3  34515  poimirlem27  35813  poimirlem29  35815  poimir  35819  itg2addnc  35840  ftc1cnnc  35858  areacirclem1  35874  prnc  36234  ispridlc  36237  lcvexchlem4  37058  lcvexchlem5  37059  lkrss2N  37190  cvrnbtwn  37292  hlrelat2  37424  atle  37457  lvolex3N  37559  lplnnlelln  37564  llncvrlpln2  37578  lvolnlelln  37605  lvolnlelpln  37606  lplncvrlvol2  37636  snatpsubN  37771  linepsubN  37773  pmodlem2  37868  linepsubclN  37972  dihatexv  39359  eldioph2b  40592  pell1234qrreccl  40683  islssfg2  40903  hbtlem2  40956  clss2lem  41226  clsk1indlem3  41660  mnuop3d  41896  sspwtrALT2  42450  fcoresf1  44574  2reu3  44613  2reu8i  44616  elsetpreimafvbi  44854  iccpartres  44881  iccpartiltu  44885  icceuelpart  44899  sprsymrelfvlem  44953  prpair  44964  prproropf1olem4  44969  prprelb  44979  goldbachthlem2  45009  lighneallem4  45073  requad2  45086  sbgoldbwt  45240  sbgoldbst  45241  nnsum4primesoddALTV  45260  nnsum4primeseven  45263  nnsum4primesevenALTV  45264  bgoldbtbndlem2  45269  mgmpropd  45340  rnghmsubcsetclem2  45545  funcrngcsetc  45567  rhmsubcsetclem2  45591  rhmsubcrngclem2  45597  funcringcsetc  45604  srhmsubc  45645  rhmsubclem4  45658  srhmsubcALTV  45663  rhmsubcALTVlem4  45676  ztprmneprm  45694  pgrpgt2nabl  45713  snlindsntor  45823  elbigo2  45909  eenglngeehlnm  46096  itschlc0yqe  46117  itscnhlc0xyqsol  46122  itsclc0  46128  itsclquadeu  46134