Theorem adantld 495

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

Syntax hints:   → wi 4   ∧ wa 400

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 210  df-an 401

This theorem is referenced by:  im2anan9  631  jaoa  970  dedlema  1059  dedlemb  1060  prlem1  1068  dfsb1  2519  elneeldif  3927  unineq  4249  2nreu  4407  3elpr2eq  4872  tz7.7  6384  ordsssuc2  6452  fpropnf1  7263  nnsuc  7876  releldmdifi  8038  el2mpocsbcl  8076  poxp  8120  suppimacnv  8166  ressuppss  8175  onnseq  8327  tz7.49  8428  oaass  8542  omordi  8547  nnmordi  8613  naddelim  8669  eroprf  8809  xpdom2  9056  unfi  9151  infsupprpr  9462  inf3lem2  9594  trcl  9693  r1pwss  9752  cardaleph  10069  dfac2b  10110  axcc4  10419  acncc  10420  zorn2lem7  10482  iundom2g  10520  cfpwsdom  10565  grothomex  10810  ltexprlem2  11018  1re  11204  00id  11381  mulge0  11728  nn0ge2m1nn  12570  zle0orge1  12604  xrlttr  13161  xmullem2  13287  snunioo  13501  fzen  13565  eluzgtdifelfzo  13752  ssfzo12bi  13786  modirr  13974  hashfundm  14475  hash2pr  14502  hash3tr  14524  hash3tpde  14526  cshf1  14843  cshweqrep  14854  limsupbnd2  15530  climrlim2  15594  climuni  15599  mulcn2  15643  serf0  15728  cvgcmp  15864  ntrivcvg  15947  smuval2  16536  dfgcd2  16600  lcmgcdlem  16660  lcmdvds  16662  lcmf  16687  qnumdencl  16794  infpnlem1  16966  ram0  17078  prmgaplem6  17112  prmgaplem7  17113  prmlem1  17163  prmlem2  17176  setsstruct  17232  catass  17738  inveq  17827  sscfn1  17870  catsubcat  17892  subccocl  17898  funcco  17924  initoeu2  18069  funcestrcsetclem8  18199  funcsetcestrclem8  18214  mgmpropd  18705  gsmsymgrfixlem1  19493  psgnran  19581  efgi  19785  efgi2  19791  cntzcmnss  19907  telgsumfzs  20055  dprddisj2  20107  rnghmsubcsetclem2  20713  funcrngcsetc  20721  rhmsubcsetclem2  20742  rhmsubcrngclem2  20748  funcringcsetc  20755  srhmsubc  20761  rhmsubclem4  20769  rnglidlmcl  21315  df2idl2crng  21388  prmirredlem  21587  psgnghm  21695  scmatghm  22655  cpmatacl  22838  pm2mpf1  22921  fvmptnn04if  22971  lmcls  23424  isfild  23980  flffbas  24117  cnpflf2  24122  qustgplem  24243  tngngp3  24778  reperflem  24941  nmhmcn  25244  iscau2  25401  iscmet3lem2  25416  ivthlem2  25576  ovolmge0  25601  itg2seq  25866  limciun  26018  dvres  26035  dveflem  26103  lhop1  26138  ftc1lem6  26165  mdegnn0cl  26193  aalioulem6  26463  lgsqrmod  27478  gausslemma2dlem3  27494  2sqreulem1  27572  2sqreunnlem1  27575  2sqreulem3  27579  pntlem3  27735  ltslpss  28063  axlowdimlem16  29244  axcontlem12  29262  umgrislfupgrlem  29409  uhgr2edg  29495  ushgredgedg  29516  ushgredgedgloop  29518  nbuhgr2vtx1edgb  29639  edgnbusgreu  29654  usgredgsscusgredg  29746  wlkdlem2  29968  pthdivtx  30013  upgrwlkdvdelem  30022  spthonepeq  30038  pthdlem1  30052  wwlksnprcl  30125  wlknewwlksn  30173  clwlkclwwlklem2a4  30285  clwlkclwwlklem2  30288  clwwlkwwlksb  30342  clwwlknun  30400  uhgr3cyclexlem  30469  eucrctshift  30531  frgrncvvdeqlem2  30588  frgrncvvdeqlem9  30595  numclwwlk1lem2foa  30642  numclwwlk1lem2f1  30645  ubthlem2  31160  shsvs  31612  mdsl2i  32611  mdsl2bi  32612  mdslmd1lem1  32614  atss  32635  chcv1  32644  chrelat2i  32654  atexch  32670  cdj3lem1  32723  disjxpin  32870  fpwrelmap  33015  nn0min  33102  sigaclci  34463  dya2iocuni  34614  omssubadd  34631  fnrelpredd  35421  umgr2cycllem  35527  subfacp1lem6  35572  fmlasuc  35773  satffunlem  35788  satffunlem1lem1  35789  satffunlem2lem1  35791  mthmblem  35967  dfon2lem6  36173  dfrdg4  36338  altopth2  36353  cgrtriv  36389  cgrextend  36395  lineext  36463  btwnconn1  36488  colinbtwnle  36505  trer  36712  elicc3  36713  poimirlem27  38181  poimirlem29  38183  poimir  38187  itg2addnc  38208  ftc1cnnc  38226  areacirclem1  38242  prnc  38601  ispridlc  38604  refressn  39067  lcvexchlem4  39696  lcvexchlem5  39697  lkrss2N  39828  cvrnbtwn  39930  hlrelat2  40062  atle  40095  lvolex3N  40197  lplnnlelln  40202  llncvrlpln2  40216  lvolnlelln  40243  lvolnlelpln  40244  lplncvrlvol2  40274  snatpsubN  40409  linepsubN  40411  pmodlem2  40506  linepsubclN  40610  dihatexv  41997  eldioph2b  43381  pell1234qrreccl  43468  islssfg2  43685  hbtlem2  43738  onexomgt  43855  cantnfresb  43938  clss2lem  44224  clsk1indlem3  44656  mnuop3d  44868  sspwtrALT2  45418  relpfrlem  45549  fcoresf1  47690  2reu3  47731  2reu8i  47734  elsetpreimafvbi  48024  iccpartres  48051  iccpartiltu  48055  icceuelpart  48069  sprsymrelfvlem  48123  prpair  48134  prproropf1olem4  48139  prprelb  48149  nprmmul2  48161  goldbachthlem2  48182  lighneallem4  48246  requad2  48272  sbgoldbwt  48426  sbgoldbst  48427  nnsum4primesoddALTV  48446  nnsum4primeseven  48449  nnsum4primesevenALTV  48450  bgoldbtbndlem2  48455  uhgrimisgrgric  48580  grtriprop  48590  isubgr3stgrlem4  48618  isubgr3stgrlem6  48620  uspgrlimlem4  48640  grlimedgclnbgr  48644  grlimprclnbgrvtx  48648  gpgedg2ov  48715  gpgedg2iv  48716  pgnbgreunbgrlem1  48762  pgnbgreunbgrlem2  48766  pgnbgreunbgrlem4  48768  pgnbgreunbgrlem5  48772  rhmsubcALTVlem4  48933  srhmsubcALTV  48974  ztprmneprm  49007  pgrpgt2nabl  49026  snlindsntor  49131  elbigo2  49212  eenglngeehlnm  49399  itschlc0yqe  49420  itscnhlc0xyqsol  49425  itsclc0  49431  itsclquadeu  49437