Theorem adantld 496

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  im2anan9  632  jaoa  970  dedlema  1061  dedlemb  1062  prlem1  1070  dfsb1  2515  elneeldif  3920  unineq  4241  2nreu  4409  3elpr2eq  4873  tz7.7  6390  ordsssuc2  6458  fpropnf1  7267  nnsuc  7882  releldmdifi  8044  el2mpocsbcl  8082  poxp  8126  suppimacnv  8172  ressuppss  8181  onnseq  8333  tz7.49  8434  oaass  8548  omordi  8553  nnmordi  8619  naddelim  8675  eroprf  8815  xpdom2  9063  unfi  9158  infsupprpr  9469  inf3lem2  9601  trcl  9700  r1pwss  9759  cardaleph  10085  dfac2b  10126  axcc4  10434  acncc  10435  zorn2lem7  10497  iundom2g  10535  cfpwsdom  10580  grothomex  10825  ltexprlem2  11033  1re  11219  00id  11396  mulge0  11743  nn0ge2m1nn  12585  zle0orge1  12619  xrlttr  13177  xmullem2  13303  snunioo  13517  fzen  13581  eluzgtdifelfzo  13769  ssfzo12bi  13803  modirr  13992  hashfundm  14493  hash2pr  14520  hash3tr  14542  hash3tpde  14544  cshf1  14867  cshweqrep  14878  limsupbnd2  15554  climrlim2  15618  climuni  15623  mulcn2  15667  serf0  15752  cvgcmp  15887  ntrivcvg  15970  smuval2  16558  dfgcd2  16622  lcmgcdlem  16682  lcmdvds  16684  lcmf  16709  qnumdencl  16816  infpnlem1  16988  ram0  17100  prmgaplem6  17134  prmgaplem7  17135  prmlem1  17185  prmlem2  17198  setsstruct  17254  catass  17760  inveq  17849  sscfn1  17892  catsubcat  17914  subccocl  17920  funcco  17946  initoeu2  18091  funcestrcsetclem8  18221  funcsetcestrclem8  18236  mgmpropd  18727  idressidex0  18753  idressid  18755  gsmsymgrfixlem1  19521  psgnran  19609  efgi  19813  efgi2  19819  cntzcmnss  19935  telgsumfzs  20083  dprddisj2  20135  rnghmsubcsetclem2  20761  funcrngcsetc  20769  rhmsubcsetclem2  20790  rhmsubcrngclem2  20796  funcringcsetc  20803  srhmsubc  20809  rhmsubclem4  20817  rnglidlmcl  21371  df2idl2crng  21451  prmirredlem  21652  psgnghm  21760  scmatghm  22720  cpmatacl  22903  pm2mpf1  22986  fvmptnn04if  23036  lmcls  23489  isfild  24046  flffbas  24183  cnpflf2  24188  qustgplem  24309  tngngp3  24844  reperflem  25007  nmhmcn  25310  iscau2  25467  iscmet3lem2  25482  ivthlem2  25642  ovolmge0  25667  itg2seq  25932  limciun  26084  dvres  26101  dveflem  26169  lhop1  26204  ftc1lem6  26231  mdegnn0cl  26259  aalioulem6  26531  lgsqrmod  27547  gausslemma2dlem3  27563  2sqreulem1  27641  2sqreunnlem1  27644  2sqreulem3  27648  pntlem3  27804  ltslpss  28132  axlowdimlem16  29338  axcontlem12  29356  umgrislfupgrlem  29503  uhgr2edg  29592  ushgredgedg  29613  ushgredgedgloop  29615  nbuhgr2vtx1edgb  29736  edgnbusgreu  29751  usgredgsscusgredg  29843  wlkdlem2  30065  pthdivtx  30115  upgrwlkdvdelem  30125  spthonepeq  30141  pthdlem1  30155  wwlksnprcl  30231  wlknewwlksn  30279  clwlkclwwlklem2a4  30391  clwlkclwwlklem2  30394  clwwlkwwlksb  30448  clwwlknun  30506  uhgr3cyclexlem  30579  eucrctshift  30641  frgrncvvdeqlem2  30698  frgrncvvdeqlem9  30705  numclwwlk1lem2foa  30752  numclwwlk1lem2f1  30755  ubthlem2  31270  shsvs  31722  mdsl2i  32721  mdsl2bi  32722  mdslmd1lem1  32724  atss  32745  chcv1  32754  chrelat2i  32764  atexch  32780  cdj3lem1  32833  disjxpin  32980  fpwrelmap  33124  nn0min  33211  sigaclci  34562  dya2iocuni  34714  omssubadd  34731  fnrelpredd  35516  subfacp1lem6  35690  fmlasuc  35891  satffunlem  35906  satffunlem1lem1  35907  satffunlem2lem1  35909  mthmblem  36085  dfon2lem6  36291  dfrdg4  36456  altopth2  36471  cgrtriv  36507  cgrextend  36513  lineext  36581  btwnconn1  36606  colinbtwnle  36623  trer  36860  elicc3  36861  poimirlem27  38331  poimirlem29  38333  poimir  38337  itg2addnc  38358  ftc1cnnc  38376  areacirclem1  38392  prnc  38751  ispridlc  38754  refressn  39215  lcvexchlem4  39844  lcvexchlem5  39845  lkrss2N  39976  cvrnbtwn  40078  hlrelat2  40210  atle  40243  lvolex3N  40345  lplnnlelln  40350  llncvrlpln2  40364  lvolnlelln  40391  lvolnlelpln  40392  lplncvrlvol2  40422  snatpsubN  40557  linepsubN  40559  pmodlem2  40654  linepsubclN  40758  dihatexv  42145  eldioph2b  43527  pell1234qrreccl  43614  islssfg2  43831  hbtlem2  43884  onexomgt  44001  cantnfresb  44084  clss2lem  44370  clsk1indlem3  44802  mnuop3d  45014  sspwtrALT2  45564  relpfrlem  45695  fcoresf1  47839  2reu3  47880  2reu8i  47883  elsetpreimafvbi  48173  iccpartres  48200  iccpartiltu  48204  icceuelpart  48218  sprsymrelfvlem  48272  prpair  48283  prproropf1olem4  48288  prprelb  48298  nprmmul2  48310  goldbachthlem2  48331  lighneallem4  48395  requad2  48421  sbgoldbwt  48575  sbgoldbst  48576  nnsum4primesoddALTV  48595  nnsum4primeseven  48598  nnsum4primesevenALTV  48599  bgoldbtbndlem2  48604  uhgrimisgrgric  48729  grtriprop  48739  isubgr3stgrlem4  48767  isubgr3stgrlem6  48769  uspgrlimlem4  48789  grlimedgclnbgr  48793  grlimprclnbgrvtx  48797  gpgedg2ov  48864  gpgedg2iv  48865  pgnbgreunbgrlem1  48911  pgnbgreunbgrlem2  48915  pgnbgreunbgrlem4  48917  pgnbgreunbgrlem5  48921  rhmsubcALTVlem4  49082  srhmsubcALTV  49123  ztprmneprm  49160  pgrpgt2nabl  49179  snlindsntor  49284  elbigo2  49365  eenglngeehlnm  49552  itschlc0yqe  49573  itscnhlc0xyqsol  49578  itsclc0  49584  itsclquadeu  49590