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

This theorem is referenced by:  im2anan9  619  jaoa  950  dedlema  1038  dedlemb  1039  prlem1  1047  dfsb1  2464  2eu3OLD  2710  elneeldif  3873  unineq  4174  2nreu  4307  3elpr2eq  4744  tz7.7  6092  ordsssuc2  6154  fpropnf1  6890  nnsuc  7453  releldmdifi  7600  el2mpocsbcl  7636  poxp  7675  suppimacnv  7692  ressuppss  7700  imacosuppOLD  7726  onnseq  7833  tz7.49  7932  oaass  8037  omordi  8042  nnmordi  8107  eroprf  8245  xpdom2  8459  infsupprpr  8814  inf3lem2  8938  trcl  9016  r1pwss  9059  cardaleph  9361  dfac2b  9402  axcc4  9707  acncc  9708  zorn2lem7  9770  iundom2g  9808  cfpwsdom  9852  grothomex  10097  ltexprlem2  10305  1re  10487  00id  10662  mulge0  11006  nn0ge2m1nn  11812  zle0orge1  11846  xrlttr  12383  xmullem2  12508  snunioo  12714  fzen  12774  eluzgtdifelfzo  12949  ssfzo12bi  12982  modirr  13160  hash2pr  13673  hash3tr  13694  cshf1  14008  cshweqrep  14019  limsupbnd2  14674  climrlim2  14738  climuni  14743  mulcn2  14786  serf0  14871  cvgcmp  15004  ntrivcvg  15086  smuval2  15664  dfgcd2  15723  lcmgcdlem  15779  lcmdvds  15781  lcmf  15806  qnumdencl  15908  infpnlem1  16075  ram0  16187  prmgaplem6  16221  prmgaplem7  16222  prmlem1  16270  prmlem2  16282  setsstruct  16352  catass  16786  inveq  16873  sscfn1  16916  catsubcat  16938  subccocl  16944  funcco  16970  initoeu2  17105  funcestrcsetclem8  17226  funcsetcestrclem8  17241  gsmsymgrfixlem1  18286  psgnran  18374  efgi  18572  efgi2  18578  cntzcmnss  18686  telgsumfzs  18826  dprddisj2  18878  prmirredlem  20322  psgnghm  20406  scmatghm  20826  cpmatacl  21008  pm2mpf1  21091  fvmptnn04if  21141  lmcls  21594  isfild  22150  flffbas  22287  cnpflf2  22292  qustgplem  22412  tngngp3  22948  reperflem  23109  nmhmcn  23407  iscau2  23563  iscmet3lem2  23578  ivthlem2  23736  ovolmge0  23761  itg2seq  24026  limciun  24175  dvres  24192  dveflem  24259  lhop1  24294  ftc1lem6  24321  mdegnn0cl  24348  aalioulem6  24609  lgsqrmod  25610  gausslemma2dlem3  25626  2sqreulem1  25704  2sqreunnlem1  25707  2sqreulem3  25711  pntlem3  25867  axlowdimlem16  26426  axcontlem12  26444  umgrislfupgrlem  26590  uhgr2edg  26673  ushgredgedg  26694  ushgredgedgloop  26696  nbuhgr2vtx1edgb  26817  edgnbusgreu  26832  usgredgsscusgredg  26924  wlkdlem2  27150  pthdivtx  27197  upgrwlkdvdelem  27204  spthonepeq  27220  pthdlem1  27234  wwlksnprcl  27304  wlknewwlksn  27352  clwlkclwwlklem2a4  27462  clwlkclwwlklem2  27465  clwwlkwwlksb  27520  clwwlknun  27578  uhgr3cyclexlem  27647  eucrctshift  27710  frgrncvvdeqlem2  27771  frgrncvvdeqlem9  27778  numclwwlk1lem2foa  27825  numclwwlk1lem2f1  27828  ubthlem2  28339  shsvs  28791  mdsl2i  29790  mdsl2bi  29791  mdslmd1lem1  29793  atss  29814  chcv1  29823  chrelat2i  29833  atexch  29849  cdj3lem1  29902  bian1d  29915  disjxpin  30028  fpwrelmap  30157  nn0min  30221  sigaclci  31008  dya2iocuni  31158  omssubadd  31175  hashfundm  31968  umgr2cycllem  31995  subfacp1lem6  32040  fmlasuc  32241  satffunlem  32256  satffunlem1lem1  32257  satffunlem2lem1  32259  mthmblem  32435  dfon2lem6  32641  dfrdg4  33021  altopth2  33036  cgrtriv  33072  cgrextend  33078  lineext  33146  btwnconn1  33171  colinbtwnle  33188  trer  33273  elicc3  33274  poimirlem27  34450  poimirlem29  34452  poimir  34456  itg2addnc  34477  ftc1cnnc  34497  areacirclem1  34513  prnc  34877  ispridlc  34880  lcvexchlem4  35704  lcvexchlem5  35705  lkrss2N  35836  cvrnbtwn  35938  hlrelat2  36070  atle  36103  lvolex3N  36205  lplnnlelln  36210  llncvrlpln2  36224  lvolnlelln  36251  lvolnlelpln  36252  lplncvrlvol2  36282  snatpsubN  36417  linepsubN  36419  pmodlem2  36514  linepsubclN  36618  dihatexv  38005  eldioph2b  38845  pell1234qrreccl  38936  islssfg2  39156  hbtlem2  39209  clss2lem  39456  clsk1indlem3  39878  mnuop3d  40104  sspwtrALT2  40696  2reu3  42825  2reu8i  42828  iccpartres  43060  iccpartiltu  43064  icceuelpart  43078  sprsymrelfvlem  43134  prpair  43145  prproropf1olem4  43150  prprelb  43160  goldbachthlem2  43190  lighneallem4  43257  requad2  43270  sbgoldbwt  43424  sbgoldbst  43425  nnsum4primesoddALTV  43444  nnsum4primeseven  43447  nnsum4primesevenALTV  43448  bgoldbtbndlem2  43453  mgmpropd  43524  rnghmsubcsetclem2  43725  funcrngcsetc  43747  rhmsubcsetclem2  43771  rhmsubcrngclem2  43777  funcringcsetc  43784  srhmsubc  43825  rhmsubclem4  43838  srhmsubcALTV  43843  rhmsubcALTVlem4  43856  ztprmneprm  43873  pgrpgt2nabl  43894  snlindsntor  44006  elbigo2  44093  eenglngeehlnm  44207  itschlc0yqe  44228  itscnhlc0xyqsol  44233  itsclc0  44239  itsclquadeu  44245