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  2483  elneeldif  3912  unineq  4237  2nreu  4393  3elpr2eq  4859  tz7.7  6340  ordsssuc2  6407  fpropnf1  7210  nnsuc  7823  releldmdifi  7986  el2mpocsbcl  8024  poxp  8067  suppimacnv  8113  ressuppss  8122  onnseq  8273  tz7.49  8373  oaass  8485  omordi  8490  nnmordi  8555  naddelim  8610  eroprf  8748  xpdom2  8996  unfi  9091  infsupprpr  9401  inf3lem2  9530  trcl  9629  r1pwss  9688  cardaleph  9991  dfac2b  10033  axcc4  10341  acncc  10342  zorn2lem7  10404  iundom2g  10442  cfpwsdom  10486  grothomex  10731  ltexprlem2  10939  1re  11123  00id  11299  mulge0  11646  nn0ge2m1nn  12462  zle0orge1  12496  xrlttr  13045  xmullem2  13171  snunioo  13385  fzen  13448  eluzgtdifelfzo  13634  ssfzo12bi  13668  modirr  13856  hashfundm  14356  hash2pr  14383  hash3tr  14405  hash3tpde  14407  cshf1  14724  cshweqrep  14735  limsupbnd2  15397  climrlim2  15461  climuni  15466  mulcn2  15510  serf0  15595  cvgcmp  15730  ntrivcvg  15811  smuval2  16400  dfgcd2  16464  lcmgcdlem  16524  lcmdvds  16526  lcmf  16551  qnumdencl  16657  infpnlem1  16829  ram0  16941  prmgaplem6  16975  prmgaplem7  16976  prmlem1  17026  prmlem2  17038  setsstruct  17094  catass  17600  inveq  17689  sscfn1  17732  catsubcat  17754  subccocl  17760  funcco  17786  initoeu2  17931  funcestrcsetclem8  18061  funcsetcestrclem8  18076  mgmpropd  18567  gsmsymgrfixlem1  19347  psgnran  19435  efgi  19639  efgi2  19645  cntzcmnss  19761  telgsumfzs  19909  dprddisj2  19961  rnghmsubcsetclem2  20556  funcrngcsetc  20564  rhmsubcsetclem2  20585  rhmsubcrngclem2  20591  funcringcsetc  20598  srhmsubc  20604  rhmsubclem4  20612  rnglidlmcl  21162  prmirredlem  21418  psgnghm  21526  scmatghm  22468  cpmatacl  22651  pm2mpf1  22734  fvmptnn04if  22784  lmcls  23237  isfild  23793  flffbas  23930  cnpflf2  23935  qustgplem  24056  tngngp3  24591  reperflem  24754  nmhmcn  25067  iscau2  25224  iscmet3lem2  25239  ivthlem2  25400  ovolmge0  25425  itg2seq  25690  limciun  25842  dvres  25859  dveflem  25930  lhop1  25966  ftc1lem6  25995  mdegnn0cl  26023  aalioulem6  26292  lgsqrmod  27310  gausslemma2dlem3  27326  2sqreulem1  27404  2sqreunnlem1  27407  2sqreulem3  27411  pntlem3  27567  sltlpss  27873  axlowdimlem16  28956  axcontlem12  28974  umgrislfupgrlem  29121  uhgr2edg  29207  ushgredgedg  29228  ushgredgedgloop  29230  nbuhgr2vtx1edgb  29351  edgnbusgreu  29366  usgredgsscusgredg  29459  wlkdlem2  29681  pthdivtx  29726  upgrwlkdvdelem  29735  spthonepeq  29751  pthdlem1  29765  wwlksnprcl  29838  wlknewwlksn  29886  clwlkclwwlklem2a4  29998  clwlkclwwlklem2  30001  clwwlkwwlksb  30055  clwwlknun  30113  uhgr3cyclexlem  30182  eucrctshift  30244  frgrncvvdeqlem2  30301  frgrncvvdeqlem9  30308  numclwwlk1lem2foa  30355  numclwwlk1lem2f1  30358  ubthlem2  30872  shsvs  31324  mdsl2i  32323  mdsl2bi  32324  mdslmd1lem1  32326  atss  32347  chcv1  32356  chrelat2i  32366  atexch  32382  cdj3lem1  32435  bian1dOLD  32457  disjxpin  32589  fpwrelmap  32740  nn0min  32829  sigaclci  34217  dya2iocuni  34368  omssubadd  34385  fnrelpredd  35174  umgr2cycllem  35256  subfacp1lem6  35301  fmlasuc  35502  satffunlem  35517  satffunlem1lem1  35518  satffunlem2lem1  35520  mthmblem  35696  dfon2lem6  35902  dfrdg4  36067  altopth2  36082  cgrtriv  36118  cgrextend  36124  lineext  36192  btwnconn1  36217  colinbtwnle  36234  trer  36432  elicc3  36433  poimirlem27  37760  poimirlem29  37762  poimir  37766  itg2addnc  37787  ftc1cnnc  37805  areacirclem1  37821  prnc  38180  ispridlc  38183  refressn  38618  lcvexchlem4  39209  lcvexchlem5  39210  lkrss2N  39341  cvrnbtwn  39443  hlrelat2  39575  atle  39608  lvolex3N  39710  lplnnlelln  39715  llncvrlpln2  39729  lvolnlelln  39756  lvolnlelpln  39757  lplncvrlvol2  39787  snatpsubN  39922  linepsubN  39924  pmodlem2  40019  linepsubclN  40123  dihatexv  41510  eldioph2b  42920  pell1234qrreccl  43011  islssfg2  43228  hbtlem2  43281  onexomgt  43398  cantnfresb  43481  clss2lem  43768  clsk1indlem3  44200  mnuop3d  44428  sspwtrALT2  44979  relpfrlem  45110  fcoresf1  47231  2reu3  47272  2reu8i  47275  elsetpreimafvbi  47553  iccpartres  47580  iccpartiltu  47584  icceuelpart  47598  sprsymrelfvlem  47652  prpair  47663  prproropf1olem4  47668  prprelb  47678  goldbachthlem2  47708  lighneallem4  47772  requad2  47785  sbgoldbwt  47939  sbgoldbst  47940  nnsum4primesoddALTV  47959  nnsum4primeseven  47962  nnsum4primesevenALTV  47963  bgoldbtbndlem2  47968  uhgrimisgrgric  48093  grtriprop  48103  isubgr3stgrlem4  48131  isubgr3stgrlem6  48133  uspgrlimlem4  48153  grlimedgclnbgr  48157  grlimprclnbgrvtx  48161  gpgedg2ov  48228  gpgedg2iv  48229  pgnbgreunbgrlem1  48275  pgnbgreunbgrlem2  48279  pgnbgreunbgrlem4  48281  pgnbgreunbgrlem5  48285  rhmsubcALTVlem4  48446  srhmsubcALTV  48487  ztprmneprm  48509  pgrpgt2nabl  48528  snlindsntor  48633  elbigo2  48714  eenglngeehlnm  48901  itschlc0yqe  48922  itscnhlc0xyqsol  48927  itsclc0  48933  itsclquadeu  48939