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  1061  dedlemb  1062  prlem1  1070  dfsb1  2513  elneeldif  3919  unineq  4241  2nreu  4409  3elpr2eq  4871  tz7.7  6386  ordsssuc2  6454  fpropnf1  7265  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  10418  acncc  10419  zorn2lem7  10481  iundom2g  10519  cfpwsdom  10564  grothomex  10809  ltexprlem2  11017  1re  11203  00id  11380  mulge0  11727  nn0ge2m1nn  12569  zle0orge1  12603  xrlttr  13160  xmullem2  13286  snunioo  13500  fzen  13564  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  16535  dfgcd2  16599  lcmgcdlem  16659  lcmdvds  16661  lcmf  16686  qnumdencl  16793  infpnlem1  16965  ram0  17077  prmgaplem6  17111  prmgaplem7  17112  prmlem1  17162  prmlem2  17175  setsstruct  17231  catass  17737  inveq  17826  sscfn1  17869  catsubcat  17891  subccocl  17897  funcco  17923  initoeu2  18068  funcestrcsetclem8  18198  funcsetcestrclem8  18213  mgmpropd  18704  gsmsymgrfixlem1  19492  psgnran  19580  efgi  19784  efgi2  19790  cntzcmnss  19906  telgsumfzs  20054  dprddisj2  20106  rnghmsubcsetclem2  20731  funcrngcsetc  20739  rhmsubcsetclem2  20760  rhmsubcrngclem2  20766  funcringcsetc  20773  srhmsubc  20779  rhmsubclem4  20787  rnglidlmcl  21341  df2idl2crng  21421  prmirredlem  21622  psgnghm  21730  scmatghm  22690  cpmatacl  22873  pm2mpf1  22956  fvmptnn04if  23006  lmcls  23459  isfild  24015  flffbas  24152  cnpflf2  24157  qustgplem  24278  tngngp3  24813  reperflem  24976  nmhmcn  25279  iscau2  25436  iscmet3lem2  25451  ivthlem2  25611  ovolmge0  25636  itg2seq  25901  limciun  26053  dvres  26070  dveflem  26138  lhop1  26173  ftc1lem6  26200  mdegnn0cl  26228  aalioulem6  26500  lgsqrmod  27516  gausslemma2dlem3  27532  2sqreulem1  27610  2sqreunnlem1  27613  2sqreulem3  27617  pntlem3  27773  ltslpss  28101  axlowdimlem16  29307  axcontlem12  29325  umgrislfupgrlem  29472  uhgr2edg  29558  ushgredgedg  29579  ushgredgedgloop  29581  nbuhgr2vtx1edgb  29702  edgnbusgreu  29717  usgredgsscusgredg  29809  wlkdlem2  30031  pthdivtx  30076  upgrwlkdvdelem  30085  spthonepeq  30101  pthdlem1  30115  wwlksnprcl  30188  wlknewwlksn  30236  clwlkclwwlklem2a4  30348  clwlkclwwlklem2  30351  clwwlkwwlksb  30405  clwwlknun  30463  uhgr3cyclexlem  30532  eucrctshift  30594  frgrncvvdeqlem2  30651  frgrncvvdeqlem9  30658  numclwwlk1lem2foa  30705  numclwwlk1lem2f1  30708  ubthlem2  31223  shsvs  31675  mdsl2i  32674  mdsl2bi  32675  mdslmd1lem1  32677  atss  32698  chcv1  32707  chrelat2i  32717  atexch  32733  cdj3lem1  32786  disjxpin  32933  fpwrelmap  33078  nn0min  33165  sigaclci  34522  dya2iocuni  34673  omssubadd  34690  fnrelpredd  35482  umgr2cycllem  35632  subfacp1lem6  35677  fmlasuc  35878  satffunlem  35893  satffunlem1lem1  35894  satffunlem2lem1  35896  mthmblem  36072  dfon2lem6  36278  dfrdg4  36443  altopth2  36458  cgrtriv  36494  cgrextend  36500  lineext  36568  btwnconn1  36593  colinbtwnle  36610  trer  36827  elicc3  36828  poimirlem27  38298  poimirlem29  38300  poimir  38304  itg2addnc  38325  ftc1cnnc  38343  areacirclem1  38359  prnc  38718  ispridlc  38721  refressn  39182  lcvexchlem4  39811  lcvexchlem5  39812  lkrss2N  39943  cvrnbtwn  40045  hlrelat2  40177  atle  40210  lvolex3N  40312  lplnnlelln  40317  llncvrlpln2  40331  lvolnlelln  40358  lvolnlelpln  40359  lplncvrlvol2  40389  snatpsubN  40524  linepsubN  40526  pmodlem2  40621  linepsubclN  40725  dihatexv  42112  eldioph2b  43494  pell1234qrreccl  43581  islssfg2  43798  hbtlem2  43851  onexomgt  43968  cantnfresb  44051  clss2lem  44337  clsk1indlem3  44769  mnuop3d  44981  sspwtrALT2  45531  relpfrlem  45662  fcoresf1  47806  2reu3  47847  2reu8i  47850  elsetpreimafvbi  48140  iccpartres  48167  iccpartiltu  48171  icceuelpart  48185  sprsymrelfvlem  48239  prpair  48250  prproropf1olem4  48255  prprelb  48265  nprmmul2  48277  goldbachthlem2  48298  lighneallem4  48362  requad2  48388  sbgoldbwt  48542  sbgoldbst  48543  nnsum4primesoddALTV  48562  nnsum4primeseven  48565  nnsum4primesevenALTV  48566  bgoldbtbndlem2  48571  uhgrimisgrgric  48696  grtriprop  48706  isubgr3stgrlem4  48734  isubgr3stgrlem6  48736  uspgrlimlem4  48756  grlimedgclnbgr  48760  grlimprclnbgrvtx  48764  gpgedg2ov  48831  gpgedg2iv  48832  pgnbgreunbgrlem1  48878  pgnbgreunbgrlem2  48882  pgnbgreunbgrlem4  48884  pgnbgreunbgrlem5  48888  rhmsubcALTVlem4  49049  srhmsubcALTV  49090  ztprmneprm  49127  pgrpgt2nabl  49146  snlindsntor  49251  elbigo2  49332  eenglngeehlnm  49519  itschlc0yqe  49540  itscnhlc0xyqsol  49545  itsclc0  49551  itsclquadeu  49557