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

This theorem is referenced by:  im2anan9  620  jaoa  957  dedlema  1045  dedlemb  1046  prlem1  1054  dfsb1  2479  elneeldif  3928  unineq  4251  2nreu  4407  3elpr2eq  4870  tz7.7  6358  ordsssuc2  6425  fpropnf1  7242  nnsuc  7860  releldmdifi  8024  el2mpocsbcl  8064  poxp  8107  suppimacnv  8153  ressuppss  8162  onnseq  8313  tz7.49  8413  oaass  8525  omordi  8530  nnmordi  8595  naddelim  8650  eroprf  8788  xpdom2  9036  unfi  9135  infsupprpr  9457  inf3lem2  9582  trcl  9681  r1pwss  9737  cardaleph  10042  dfac2b  10084  axcc4  10392  acncc  10393  zorn2lem7  10455  iundom2g  10493  cfpwsdom  10537  grothomex  10782  ltexprlem2  10990  1re  11174  00id  11349  mulge0  11696  nn0ge2m1nn  12512  zle0orge1  12546  xrlttr  13100  xmullem2  13225  snunioo  13439  fzen  13502  eluzgtdifelfzo  13688  ssfzo12bi  13722  modirr  13907  hashfundm  14407  hash2pr  14434  hash3tr  14456  hash3tpde  14458  cshf1  14775  cshweqrep  14786  limsupbnd2  15449  climrlim2  15513  climuni  15518  mulcn2  15562  serf0  15647  cvgcmp  15782  ntrivcvg  15863  smuval2  16452  dfgcd2  16516  lcmgcdlem  16576  lcmdvds  16578  lcmf  16603  qnumdencl  16709  infpnlem1  16881  ram0  16993  prmgaplem6  17027  prmgaplem7  17028  prmlem1  17078  prmlem2  17090  setsstruct  17146  catass  17647  inveq  17736  sscfn1  17779  catsubcat  17801  subccocl  17807  funcco  17833  initoeu2  17978  funcestrcsetclem8  18108  funcsetcestrclem8  18123  mgmpropd  18578  gsmsymgrfixlem1  19357  psgnran  19445  efgi  19649  efgi2  19655  cntzcmnss  19771  telgsumfzs  19919  dprddisj2  19971  rnghmsubcsetclem2  20541  funcrngcsetc  20549  rhmsubcsetclem2  20570  rhmsubcrngclem2  20576  funcringcsetc  20583  srhmsubc  20589  rhmsubclem4  20597  rnglidlmcl  21126  prmirredlem  21382  psgnghm  21489  scmatghm  22420  cpmatacl  22603  pm2mpf1  22686  fvmptnn04if  22736  lmcls  23189  isfild  23745  flffbas  23882  cnpflf2  23887  qustgplem  24008  tngngp3  24544  reperflem  24707  nmhmcn  25020  iscau2  25177  iscmet3lem2  25192  ivthlem2  25353  ovolmge0  25378  itg2seq  25643  limciun  25795  dvres  25812  dveflem  25883  lhop1  25919  ftc1lem6  25948  mdegnn0cl  25976  aalioulem6  26245  lgsqrmod  27263  gausslemma2dlem3  27279  2sqreulem1  27357  2sqreunnlem1  27360  2sqreulem3  27364  pntlem3  27520  sltlpss  27819  axlowdimlem16  28884  axcontlem12  28902  umgrislfupgrlem  29049  uhgr2edg  29135  ushgredgedg  29156  ushgredgedgloop  29158  nbuhgr2vtx1edgb  29279  edgnbusgreu  29294  usgredgsscusgredg  29387  wlkdlem2  29611  pthdivtx  29657  upgrwlkdvdelem  29666  spthonepeq  29682  pthdlem1  29696  wwlksnprcl  29769  wlknewwlksn  29817  clwlkclwwlklem2a4  29926  clwlkclwwlklem2  29929  clwwlkwwlksb  29983  clwwlknun  30041  uhgr3cyclexlem  30110  eucrctshift  30172  frgrncvvdeqlem2  30229  frgrncvvdeqlem9  30236  numclwwlk1lem2foa  30283  numclwwlk1lem2f1  30286  ubthlem2  30800  shsvs  31252  mdsl2i  32251  mdsl2bi  32252  mdslmd1lem1  32254  atss  32275  chcv1  32284  chrelat2i  32294  atexch  32310  cdj3lem1  32363  bian1dOLD  32386  disjxpin  32517  fpwrelmap  32656  nn0min  32745  sigaclci  34122  dya2iocuni  34274  omssubadd  34291  fnrelpredd  35079  umgr2cycllem  35127  subfacp1lem6  35172  fmlasuc  35373  satffunlem  35388  satffunlem1lem1  35389  satffunlem2lem1  35391  mthmblem  35567  dfon2lem6  35776  dfrdg4  35939  altopth2  35954  cgrtriv  35990  cgrextend  35996  lineext  36064  btwnconn1  36089  colinbtwnle  36106  trer  36304  elicc3  36305  poimirlem27  37641  poimirlem29  37643  poimir  37647  itg2addnc  37668  ftc1cnnc  37686  areacirclem1  37702  prnc  38061  ispridlc  38064  refressn  38434  lcvexchlem4  39030  lcvexchlem5  39031  lkrss2N  39162  cvrnbtwn  39264  hlrelat2  39397  atle  39430  lvolex3N  39532  lplnnlelln  39537  llncvrlpln2  39551  lvolnlelln  39578  lvolnlelpln  39579  lplncvrlvol2  39609  snatpsubN  39744  linepsubN  39746  pmodlem2  39841  linepsubclN  39945  dihatexv  41332  eldioph2b  42751  pell1234qrreccl  42842  islssfg2  43060  hbtlem2  43113  onexomgt  43230  cantnfresb  43313  clss2lem  43600  clsk1indlem3  44032  mnuop3d  44260  sspwtrALT2  44812  relpfrlem  44943  fcoresf1  47070  2reu3  47111  2reu8i  47114  elsetpreimafvbi  47392  iccpartres  47419  iccpartiltu  47423  icceuelpart  47437  sprsymrelfvlem  47491  prpair  47502  prproropf1olem4  47507  prprelb  47517  goldbachthlem2  47547  lighneallem4  47611  requad2  47624  sbgoldbwt  47778  sbgoldbst  47779  nnsum4primesoddALTV  47798  nnsum4primeseven  47801  nnsum4primesevenALTV  47802  bgoldbtbndlem2  47807  uhgrimisgrgric  47931  grtriprop  47940  isubgr3stgrlem4  47968  isubgr3stgrlem6  47970  uspgrlimlem4  47990  gpgedg2ov  48057  gpgedg2iv  48058  pgnbgreunbgrlem1  48103  pgnbgreunbgrlem2  48107  pgnbgreunbgrlem4  48109  pgnbgreunbgrlem5  48113  rhmsubcALTVlem4  48272  srhmsubcALTV  48313  ztprmneprm  48335  pgrpgt2nabl  48354  snlindsntor  48460  elbigo2  48541  eenglngeehlnm  48728  itschlc0yqe  48749  itscnhlc0xyqsol  48754  itsclc0  48760  itsclquadeu  48766