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  2506  2eu3OLD  2736  elneeldif  3949  unineq  4253  2nreu  4392  3elpr2eq  4830  tz7.7  6211  ordsssuc2  6273  fpropnf1  7019  nnsuc  7591  releldmdifi  7738  el2mpocsbcl  7774  poxp  7816  suppimacnv  7835  ressuppss  7843  imacosuppOLD  7869  onnseq  7975  tz7.49  8075  oaass  8181  omordi  8186  nnmordi  8251  eroprf  8389  xpdom2  8606  infsupprpr  8962  inf3lem2  9086  trcl  9164  r1pwss  9207  cardaleph  9509  dfac2b  9550  axcc4  9855  acncc  9856  zorn2lem7  9918  iundom2g  9956  cfpwsdom  10000  grothomex  10245  ltexprlem2  10453  1re  10635  00id  10809  mulge0  11152  nn0ge2m1nn  11958  zle0orge1  11992  xrlttr  12527  xmullem2  12652  snunioo  12858  fzen  12918  eluzgtdifelfzo  13093  ssfzo12bi  13126  modirr  13304  hash2pr  13821  hash3tr  13842  cshf1  14166  cshweqrep  14177  limsupbnd2  14834  climrlim2  14898  climuni  14903  mulcn2  14946  serf0  15031  cvgcmp  15165  ntrivcvg  15247  smuval2  15825  dfgcd2  15888  lcmgcdlem  15944  lcmdvds  15946  lcmf  15971  qnumdencl  16073  infpnlem1  16240  ram0  16352  prmgaplem6  16386  prmgaplem7  16387  prmlem1  16435  prmlem2  16447  setsstruct  16517  catass  16951  inveq  17038  sscfn1  17081  catsubcat  17103  subccocl  17109  funcco  17135  initoeu2  17270  funcestrcsetclem8  17391  funcsetcestrclem8  17406  gsmsymgrfixlem1  18549  psgnran  18637  efgi  18839  efgi2  18845  cntzcmnss  18955  telgsumfzs  19103  dprddisj2  19155  prmirredlem  20634  psgnghm  20718  scmatghm  21136  cpmatacl  21318  pm2mpf1  21401  fvmptnn04if  21451  lmcls  21904  isfild  22460  flffbas  22597  cnpflf2  22602  qustgplem  22723  tngngp3  23259  reperflem  23420  nmhmcn  23718  iscau2  23874  iscmet3lem2  23889  ivthlem2  24047  ovolmge0  24072  itg2seq  24337  limciun  24486  dvres  24503  dveflem  24570  lhop1  24605  ftc1lem6  24632  mdegnn0cl  24659  aalioulem6  24920  lgsqrmod  25922  gausslemma2dlem3  25938  2sqreulem1  26016  2sqreunnlem1  26019  2sqreulem3  26023  pntlem3  26179  axlowdimlem16  26737  axcontlem12  26755  umgrislfupgrlem  26901  uhgr2edg  26984  ushgredgedg  27005  ushgredgedgloop  27007  nbuhgr2vtx1edgb  27128  edgnbusgreu  27143  usgredgsscusgredg  27235  wlkdlem2  27459  pthdivtx  27504  upgrwlkdvdelem  27511  spthonepeq  27527  pthdlem1  27541  wwlksnprcl  27611  wlknewwlksn  27659  clwlkclwwlklem2a4  27769  clwlkclwwlklem2  27772  clwwlkwwlksb  27827  clwwlknun  27885  uhgr3cyclexlem  27954  eucrctshift  28016  frgrncvvdeqlem2  28073  frgrncvvdeqlem9  28080  numclwwlk1lem2foa  28127  numclwwlk1lem2f1  28130  ubthlem2  28642  shsvs  29094  mdsl2i  30093  mdsl2bi  30094  mdslmd1lem1  30096  atss  30117  chcv1  30126  chrelat2i  30136  atexch  30152  cdj3lem1  30205  bian1d  30218  disjxpin  30332  fpwrelmap  30463  nn0min  30531  sigaclci  31386  dya2iocuni  31536  omssubadd  31553  hashfundm  32349  umgr2cycllem  32382  subfacp1lem6  32427  fmlasuc  32628  satffunlem  32643  satffunlem1lem1  32644  satffunlem2lem1  32646  mthmblem  32822  dfon2lem6  33028  dfrdg4  33407  altopth2  33422  cgrtriv  33458  cgrextend  33464  lineext  33532  btwnconn1  33557  colinbtwnle  33574  trer  33659  elicc3  33660  poimirlem27  34913  poimirlem29  34915  poimir  34919  itg2addnc  34940  ftc1cnnc  34960  areacirclem1  34976  prnc  35339  ispridlc  35342  lcvexchlem4  36167  lcvexchlem5  36168  lkrss2N  36299  cvrnbtwn  36401  hlrelat2  36533  atle  36566  lvolex3N  36668  lplnnlelln  36673  llncvrlpln2  36687  lvolnlelln  36714  lvolnlelpln  36715  lplncvrlvol2  36745  snatpsubN  36880  linepsubN  36882  pmodlem2  36977  linepsubclN  37081  dihatexv  38468  eldioph2b  39353  pell1234qrreccl  39444  islssfg2  39664  hbtlem2  39717  clss2lem  39964  clsk1indlem3  40386  mnuop3d  40600  sspwtrALT2  41150  2reu3  43303  2reu8i  43306  elsetpreimafvbi  43545  iccpartres  43572  iccpartiltu  43576  icceuelpart  43590  sprsymrelfvlem  43646  prpair  43657  prproropf1olem4  43662  prprelb  43672  goldbachthlem2  43702  lighneallem4  43769  requad2  43782  sbgoldbwt  43936  sbgoldbst  43937  nnsum4primesoddALTV  43956  nnsum4primeseven  43959  nnsum4primesevenALTV  43960  bgoldbtbndlem2  43965  mgmpropd  44036  rnghmsubcsetclem2  44241  funcrngcsetc  44263  rhmsubcsetclem2  44287  rhmsubcrngclem2  44293  funcringcsetc  44300  srhmsubc  44341  rhmsubclem4  44354  srhmsubcALTV  44359  rhmsubcALTVlem4  44372  ztprmneprm  44389  pgrpgt2nabl  44408  snlindsntor  44520  elbigo2  44606  eenglngeehlnm  44720  itschlc0yqe  44741  itscnhlc0xyqsol  44746  itsclc0  44752  itsclquadeu  44758