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

This theorem is referenced by:  im2anan9  619  jaoa  952  dedlema  1042  dedlemb  1043  prlem1  1051  dfsb1  2485  elneeldif  3897  unineq  4208  2nreu  4372  3elpr2eq  4835  tz7.7  6277  ordsssuc2  6339  fpropnf1  7121  nnsuc  7705  releldmdifi  7859  el2mpocsbcl  7896  poxp  7940  suppimacnv  7961  ressuppss  7970  onnseq  8146  tz7.49  8246  oaass  8354  omordi  8359  nnmordi  8424  eroprf  8562  xpdom2  8807  unfi  8917  infsupprpr  9193  inf3lem2  9317  trcl  9417  r1pwss  9473  cardaleph  9776  dfac2b  9817  axcc4  10126  acncc  10127  zorn2lem7  10189  iundom2g  10227  cfpwsdom  10271  grothomex  10516  ltexprlem2  10724  1re  10906  00id  11080  mulge0  11423  nn0ge2m1nn  12232  zle0orge1  12266  xrlttr  12803  xmullem2  12928  snunioo  13139  fzen  13202  eluzgtdifelfzo  13377  ssfzo12bi  13410  modirr  13590  hash2pr  14111  hash3tr  14132  cshf1  14451  cshweqrep  14462  limsupbnd2  15120  climrlim2  15184  climuni  15189  mulcn2  15233  serf0  15320  cvgcmp  15456  ntrivcvg  15537  smuval2  16117  dfgcd2  16182  lcmgcdlem  16239  lcmdvds  16241  lcmf  16266  qnumdencl  16371  infpnlem1  16539  ram0  16651  prmgaplem6  16685  prmgaplem7  16686  prmlem1  16737  prmlem2  16749  setsstruct  16805  catass  17312  inveq  17403  sscfn1  17446  catsubcat  17470  subccocl  17476  funcco  17502  initoeu2  17647  funcestrcsetclem8  17780  funcsetcestrclem8  17795  gsmsymgrfixlem1  18950  psgnran  19038  efgi  19240  efgi2  19246  cntzcmnss  19357  telgsumfzs  19505  dprddisj2  19557  prmirredlem  20606  psgnghm  20697  scmatghm  21590  cpmatacl  21773  pm2mpf1  21856  fvmptnn04if  21906  lmcls  22361  isfild  22917  flffbas  23054  cnpflf2  23059  qustgplem  23180  tngngp3  23726  reperflem  23887  nmhmcn  24189  iscau2  24346  iscmet3lem2  24361  ivthlem2  24521  ovolmge0  24546  itg2seq  24812  limciun  24963  dvres  24980  dveflem  25048  lhop1  25083  ftc1lem6  25110  mdegnn0cl  25141  aalioulem6  25402  lgsqrmod  26405  gausslemma2dlem3  26421  2sqreulem1  26499  2sqreunnlem1  26502  2sqreulem3  26506  pntlem3  26662  axlowdimlem16  27228  axcontlem12  27246  umgrislfupgrlem  27395  uhgr2edg  27478  ushgredgedg  27499  ushgredgedgloop  27501  nbuhgr2vtx1edgb  27622  edgnbusgreu  27637  usgredgsscusgredg  27729  wlkdlem2  27953  pthdivtx  27998  upgrwlkdvdelem  28005  spthonepeq  28021  pthdlem1  28035  wwlksnprcl  28105  wlknewwlksn  28153  clwlkclwwlklem2a4  28262  clwlkclwwlklem2  28265  clwwlkwwlksb  28319  clwwlknun  28377  uhgr3cyclexlem  28446  eucrctshift  28508  frgrncvvdeqlem2  28565  frgrncvvdeqlem9  28572  numclwwlk1lem2foa  28619  numclwwlk1lem2f1  28622  ubthlem2  29134  shsvs  29586  mdsl2i  30585  mdsl2bi  30586  mdslmd1lem1  30588  atss  30609  chcv1  30618  chrelat2i  30628  atexch  30644  cdj3lem1  30697  bian1d  30710  disjxpin  30828  fpwrelmap  30970  nn0min  31036  sigaclci  32000  dya2iocuni  32150  omssubadd  32167  fnrelpredd  32961  hashfundm  32974  umgr2cycllem  33002  subfacp1lem6  33047  fmlasuc  33248  satffunlem  33263  satffunlem1lem1  33264  satffunlem2lem1  33266  mthmblem  33442  dfon2lem6  33670  naddelim  33765  sltlpss  34014  dfrdg4  34180  altopth2  34195  cgrtriv  34231  cgrextend  34237  lineext  34305  btwnconn1  34330  colinbtwnle  34347  trer  34432  elicc3  34433  poimirlem27  35731  poimirlem29  35733  poimir  35737  itg2addnc  35758  ftc1cnnc  35776  areacirclem1  35792  prnc  36152  ispridlc  36155  lcvexchlem4  36978  lcvexchlem5  36979  lkrss2N  37110  cvrnbtwn  37212  hlrelat2  37344  atle  37377  lvolex3N  37479  lplnnlelln  37484  llncvrlpln2  37498  lvolnlelln  37525  lvolnlelpln  37526  lplncvrlvol2  37556  snatpsubN  37691  linepsubN  37693  pmodlem2  37788  linepsubclN  37892  dihatexv  39279  eldioph2b  40501  pell1234qrreccl  40592  islssfg2  40812  hbtlem2  40865  clss2lem  41108  clsk1indlem3  41542  mnuop3d  41778  sspwtrALT2  42332  fcoresf1  44450  2reu3  44489  2reu8i  44492  elsetpreimafvbi  44731  iccpartres  44758  iccpartiltu  44762  icceuelpart  44776  sprsymrelfvlem  44830  prpair  44841  prproropf1olem4  44846  prprelb  44856  goldbachthlem2  44886  lighneallem4  44950  requad2  44963  sbgoldbwt  45117  sbgoldbst  45118  nnsum4primesoddALTV  45137  nnsum4primeseven  45140  nnsum4primesevenALTV  45141  bgoldbtbndlem2  45146  mgmpropd  45217  rnghmsubcsetclem2  45422  funcrngcsetc  45444  rhmsubcsetclem2  45468  rhmsubcrngclem2  45474  funcringcsetc  45481  srhmsubc  45522  rhmsubclem4  45535  srhmsubcALTV  45540  rhmsubcALTVlem4  45553  ztprmneprm  45571  pgrpgt2nabl  45590  snlindsntor  45700  elbigo2  45786  eenglngeehlnm  45973  itschlc0yqe  45994  itscnhlc0xyqsol  45999  itsclc0  46005  itsclquadeu  46011