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  954  dedlema  1044  dedlemb  1045  prlem1  1053  dfsb1  2479  elneeldif  3927  unineq  4242  2nreu  4406  3elpr2eq  4869  tz7.7  6348  ordsssuc2  6413  fpropnf1  7219  nnsuc  7825  releldmdifi  7982  el2mpocsbcl  8022  poxp  8065  suppimacnv  8110  ressuppss  8119  onnseq  8295  tz7.49  8396  oaass  8513  omordi  8518  nnmordi  8583  naddelim  8637  eroprf  8761  xpdom2  9018  unfi  9123  infsupprpr  9449  inf3lem2  9574  trcl  9673  r1pwss  9729  cardaleph  10034  dfac2b  10075  axcc4  10384  acncc  10385  zorn2lem7  10447  iundom2g  10485  cfpwsdom  10529  grothomex  10774  ltexprlem2  10982  1re  11164  00id  11339  mulge0  11682  nn0ge2m1nn  12491  zle0orge1  12525  xrlttr  13069  xmullem2  13194  snunioo  13405  fzen  13468  eluzgtdifelfzo  13644  ssfzo12bi  13677  modirr  13857  hashfundm  14352  hash2pr  14380  hash3tr  14401  cshf1  14710  cshweqrep  14721  limsupbnd2  15377  climrlim2  15441  climuni  15446  mulcn2  15490  serf0  15577  cvgcmp  15712  ntrivcvg  15793  smuval2  16373  dfgcd2  16438  lcmgcdlem  16493  lcmdvds  16495  lcmf  16520  qnumdencl  16625  infpnlem1  16793  ram0  16905  prmgaplem6  16939  prmgaplem7  16940  prmlem1  16991  prmlem2  17003  setsstruct  17059  catass  17580  inveq  17671  sscfn1  17714  catsubcat  17739  subccocl  17745  funcco  17771  initoeu2  17916  funcestrcsetclem8  18049  funcsetcestrclem8  18064  gsmsymgrfixlem1  19223  psgnran  19311  efgi  19515  efgi2  19521  cntzcmnss  19633  telgsumfzs  19780  dprddisj2  19832  prmirredlem  20930  psgnghm  21021  scmatghm  21919  cpmatacl  22102  pm2mpf1  22185  fvmptnn04if  22235  lmcls  22690  isfild  23246  flffbas  23383  cnpflf2  23388  qustgplem  23509  tngngp3  24057  reperflem  24218  nmhmcn  24520  iscau2  24678  iscmet3lem2  24693  ivthlem2  24853  ovolmge0  24878  itg2seq  25144  limciun  25295  dvres  25312  dveflem  25380  lhop1  25415  ftc1lem6  25442  mdegnn0cl  25473  aalioulem6  25734  lgsqrmod  26737  gausslemma2dlem3  26753  2sqreulem1  26831  2sqreunnlem1  26834  2sqreulem3  26838  pntlem3  26994  sltlpss  27279  axlowdimlem16  27969  axcontlem12  27987  umgrislfupgrlem  28136  uhgr2edg  28219  ushgredgedg  28240  ushgredgedgloop  28242  nbuhgr2vtx1edgb  28363  edgnbusgreu  28378  usgredgsscusgredg  28470  wlkdlem2  28694  pthdivtx  28740  upgrwlkdvdelem  28747  spthonepeq  28763  pthdlem1  28777  wwlksnprcl  28847  wlknewwlksn  28895  clwlkclwwlklem2a4  29004  clwlkclwwlklem2  29007  clwwlkwwlksb  29061  clwwlknun  29119  uhgr3cyclexlem  29188  eucrctshift  29250  frgrncvvdeqlem2  29307  frgrncvvdeqlem9  29314  numclwwlk1lem2foa  29361  numclwwlk1lem2f1  29364  ubthlem2  29876  shsvs  30328  mdsl2i  31327  mdsl2bi  31328  mdslmd1lem1  31330  atss  31351  chcv1  31360  chrelat2i  31370  atexch  31386  cdj3lem1  31439  bian1d  31452  disjxpin  31573  fpwrelmap  31718  nn0min  31786  sigaclci  32820  dya2iocuni  32972  omssubadd  32989  fnrelpredd  33782  umgr2cycllem  33821  subfacp1lem6  33866  fmlasuc  34067  satffunlem  34082  satffunlem1lem1  34083  satffunlem2lem1  34085  mthmblem  34261  dfon2lem6  34449  dfrdg4  34612  altopth2  34627  cgrtriv  34663  cgrextend  34669  lineext  34737  btwnconn1  34762  colinbtwnle  34779  trer  34864  elicc3  34865  poimirlem27  36178  poimirlem29  36180  poimir  36184  itg2addnc  36205  ftc1cnnc  36223  areacirclem1  36239  prnc  36599  ispridlc  36602  refressn  36978  lcvexchlem4  37572  lcvexchlem5  37573  lkrss2N  37704  cvrnbtwn  37806  hlrelat2  37939  atle  37972  lvolex3N  38074  lplnnlelln  38079  llncvrlpln2  38093  lvolnlelln  38120  lvolnlelpln  38121  lplncvrlvol2  38151  snatpsubN  38286  linepsubN  38288  pmodlem2  38383  linepsubclN  38487  dihatexv  39874  eldioph2b  41144  pell1234qrreccl  41235  islssfg2  41456  hbtlem2  41509  onexomgt  41633  cantnfresb  41717  clss2lem  42005  clsk1indlem3  42437  mnuop3d  42673  sspwtrALT2  43227  fcoresf1  45423  2reu3  45462  2reu8i  45465  elsetpreimafvbi  45703  iccpartres  45730  iccpartiltu  45734  icceuelpart  45748  sprsymrelfvlem  45802  prpair  45813  prproropf1olem4  45818  prprelb  45828  goldbachthlem2  45858  lighneallem4  45922  requad2  45935  sbgoldbwt  46089  sbgoldbst  46090  nnsum4primesoddALTV  46109  nnsum4primeseven  46112  nnsum4primesevenALTV  46113  bgoldbtbndlem2  46118  mgmpropd  46189  rnghmsubcsetclem2  46394  funcrngcsetc  46416  rhmsubcsetclem2  46440  rhmsubcrngclem2  46446  funcringcsetc  46453  srhmsubc  46494  rhmsubclem4  46507  srhmsubcALTV  46512  rhmsubcALTVlem4  46525  ztprmneprm  46543  pgrpgt2nabl  46562  snlindsntor  46672  elbigo2  46758  eenglngeehlnm  46945  itschlc0yqe  46966  itscnhlc0xyqsol  46971  itsclc0  46977  itsclquadeu  46983