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  3917  unineq  4239  2nreu  4395  3elpr2eq  4857  tz7.7  6333  ordsssuc2  6400  fpropnf1  7204  nnsuc  7817  releldmdifi  7980  el2mpocsbcl  8018  poxp  8061  suppimacnv  8107  ressuppss  8116  onnseq  8267  tz7.49  8367  oaass  8479  omordi  8484  nnmordi  8549  naddelim  8604  eroprf  8742  xpdom2  8989  unfi  9085  infsupprpr  9396  inf3lem2  9525  trcl  9624  r1pwss  9680  cardaleph  9983  dfac2b  10025  axcc4  10333  acncc  10334  zorn2lem7  10396  iundom2g  10434  cfpwsdom  10478  grothomex  10723  ltexprlem2  10931  1re  11115  00id  11291  mulge0  11638  nn0ge2m1nn  12454  zle0orge1  12488  xrlttr  13042  xmullem2  13167  snunioo  13381  fzen  13444  eluzgtdifelfzo  13630  ssfzo12bi  13664  modirr  13849  hashfundm  14349  hash2pr  14376  hash3tr  14398  hash3tpde  14400  cshf1  14716  cshweqrep  14727  limsupbnd2  15390  climrlim2  15454  climuni  15459  mulcn2  15503  serf0  15588  cvgcmp  15723  ntrivcvg  15804  smuval2  16393  dfgcd2  16457  lcmgcdlem  16517  lcmdvds  16519  lcmf  16544  qnumdencl  16650  infpnlem1  16822  ram0  16934  prmgaplem6  16968  prmgaplem7  16969  prmlem1  17019  prmlem2  17031  setsstruct  17087  catass  17592  inveq  17681  sscfn1  17724  catsubcat  17746  subccocl  17752  funcco  17778  initoeu2  17923  funcestrcsetclem8  18053  funcsetcestrclem8  18068  mgmpropd  18525  gsmsymgrfixlem1  19306  psgnran  19394  efgi  19598  efgi2  19604  cntzcmnss  19720  telgsumfzs  19868  dprddisj2  19920  rnghmsubcsetclem2  20517  funcrngcsetc  20525  rhmsubcsetclem2  20546  rhmsubcrngclem2  20552  funcringcsetc  20559  srhmsubc  20565  rhmsubclem4  20573  rnglidlmcl  21123  prmirredlem  21379  psgnghm  21487  scmatghm  22418  cpmatacl  22601  pm2mpf1  22684  fvmptnn04if  22734  lmcls  23187  isfild  23743  flffbas  23880  cnpflf2  23885  qustgplem  24006  tngngp3  24542  reperflem  24705  nmhmcn  25018  iscau2  25175  iscmet3lem2  25190  ivthlem2  25351  ovolmge0  25376  itg2seq  25641  limciun  25793  dvres  25810  dveflem  25881  lhop1  25917  ftc1lem6  25946  mdegnn0cl  25974  aalioulem6  26243  lgsqrmod  27261  gausslemma2dlem3  27277  2sqreulem1  27355  2sqreunnlem1  27358  2sqreulem3  27362  pntlem3  27518  sltlpss  27824  axlowdimlem16  28906  axcontlem12  28924  umgrislfupgrlem  29071  uhgr2edg  29157  ushgredgedg  29178  ushgredgedgloop  29180  nbuhgr2vtx1edgb  29301  edgnbusgreu  29316  usgredgsscusgredg  29409  wlkdlem2  29631  pthdivtx  29676  upgrwlkdvdelem  29685  spthonepeq  29701  pthdlem1  29715  wwlksnprcl  29788  wlknewwlksn  29836  clwlkclwwlklem2a4  29945  clwlkclwwlklem2  29948  clwwlkwwlksb  30002  clwwlknun  30060  uhgr3cyclexlem  30129  eucrctshift  30191  frgrncvvdeqlem2  30248  frgrncvvdeqlem9  30255  numclwwlk1lem2foa  30302  numclwwlk1lem2f1  30305  ubthlem2  30819  shsvs  31271  mdsl2i  32270  mdsl2bi  32271  mdslmd1lem1  32273  atss  32294  chcv1  32303  chrelat2i  32313  atexch  32329  cdj3lem1  32382  bian1dOLD  32405  disjxpin  32537  fpwrelmap  32685  nn0min  32774  sigaclci  34115  dya2iocuni  34267  omssubadd  34284  fnrelpredd  35072  umgr2cycllem  35133  subfacp1lem6  35178  fmlasuc  35379  satffunlem  35394  satffunlem1lem1  35395  satffunlem2lem1  35397  mthmblem  35573  dfon2lem6  35782  dfrdg4  35945  altopth2  35960  cgrtriv  35996  cgrextend  36002  lineext  36070  btwnconn1  36095  colinbtwnle  36112  trer  36310  elicc3  36311  poimirlem27  37647  poimirlem29  37649  poimir  37653  itg2addnc  37674  ftc1cnnc  37692  areacirclem1  37708  prnc  38067  ispridlc  38070  refressn  38440  lcvexchlem4  39036  lcvexchlem5  39037  lkrss2N  39168  cvrnbtwn  39270  hlrelat2  39402  atle  39435  lvolex3N  39537  lplnnlelln  39542  llncvrlpln2  39556  lvolnlelln  39583  lvolnlelpln  39584  lplncvrlvol2  39614  snatpsubN  39749  linepsubN  39751  pmodlem2  39846  linepsubclN  39950  dihatexv  41337  eldioph2b  42756  pell1234qrreccl  42847  islssfg2  43064  hbtlem2  43117  onexomgt  43234  cantnfresb  43317  clss2lem  43604  clsk1indlem3  44036  mnuop3d  44264  sspwtrALT2  44816  relpfrlem  44947  fcoresf1  47073  2reu3  47114  2reu8i  47117  elsetpreimafvbi  47395  iccpartres  47422  iccpartiltu  47426  icceuelpart  47440  sprsymrelfvlem  47494  prpair  47505  prproropf1olem4  47510  prprelb  47520  goldbachthlem2  47550  lighneallem4  47614  requad2  47627  sbgoldbwt  47781  sbgoldbst  47782  nnsum4primesoddALTV  47801  nnsum4primeseven  47804  nnsum4primesevenALTV  47805  bgoldbtbndlem2  47810  uhgrimisgrgric  47935  grtriprop  47945  isubgr3stgrlem4  47973  isubgr3stgrlem6  47975  uspgrlimlem4  47995  grlimedgclnbgr  47999  grlimprclnbgrvtx  48003  gpgedg2ov  48070  gpgedg2iv  48071  pgnbgreunbgrlem1  48117  pgnbgreunbgrlem2  48121  pgnbgreunbgrlem4  48123  pgnbgreunbgrlem5  48127  rhmsubcALTVlem4  48288  srhmsubcALTV  48329  ztprmneprm  48351  pgrpgt2nabl  48370  snlindsntor  48476  elbigo2  48557  eenglngeehlnm  48744  itschlc0yqe  48765  itscnhlc0xyqsol  48770  itsclc0  48776  itsclquadeu  48782