Theorem adantld 494

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

Syntax hints:   → wi 4   ∧ wa 399

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 209  df-an 400

This theorem is referenced by:  im2anan9  629  jaoa  968  dedlema  1056  dedlemb  1057  prlem1  1065  dfsb1  2511  elneeldif  3916  unineq  4238  2nreu  4395  3elpr2eq  4861  tz7.7  6367  ordsssuc2  6434  fpropnf1  7246  nnsuc  7859  releldmdifi  8021  el2mpocsbcl  8058  poxp  8102  suppimacnv  8148  ressuppss  8157  onnseq  8309  tz7.49  8410  oaass  8524  omordi  8529  nnmordi  8595  naddelim  8651  eroprf  8791  xpdom2  9038  unfi  9133  infsupprpr  9446  inf3lem2  9578  trcl  9677  r1pwss  9736  cardaleph  10039  dfac2b  10081  axcc4  10390  acncc  10391  zorn2lem7  10453  iundom2g  10491  cfpwsdom  10536  grothomex  10781  ltexprlem2  10989  1re  11175  00id  11352  mulge0  11699  nn0ge2m1nn  12545  zle0orge1  12579  xrlttr  13136  xmullem2  13262  snunioo  13476  fzen  13540  eluzgtdifelfzo  13727  ssfzo12bi  13761  modirr  13949  hashfundm  14449  hash2pr  14476  hash3tr  14498  hash3tpde  14500  cshf1  14817  cshweqrep  14828  limsupbnd2  15501  climrlim2  15565  climuni  15570  mulcn2  15614  serf0  15699  cvgcmp  15835  ntrivcvg  15918  smuval2  16507  dfgcd2  16571  lcmgcdlem  16631  lcmdvds  16633  lcmf  16658  qnumdencl  16765  infpnlem1  16937  ram0  17049  prmgaplem6  17083  prmgaplem7  17084  prmlem1  17134  prmlem2  17147  setsstruct  17203  catass  17709  inveq  17798  sscfn1  17841  catsubcat  17863  subccocl  17869  funcco  17895  initoeu2  18040  funcestrcsetclem8  18170  funcsetcestrclem8  18185  mgmpropd  18676  gsmsymgrfixlem1  19458  psgnran  19546  efgi  19750  efgi2  19756  cntzcmnss  19872  telgsumfzs  20020  dprddisj2  20072  rnghmsubcsetclem2  20669  funcrngcsetc  20677  rhmsubcsetclem2  20698  rhmsubcrngclem2  20704  funcringcsetc  20711  srhmsubc  20717  rhmsubclem4  20725  rnglidlmcl  21274  prmirredlem  21512  psgnghm  21620  scmatghm  22581  cpmatacl  22764  pm2mpf1  22847  fvmptnn04if  22897  lmcls  23350  isfild  23906  flffbas  24043  cnpflf2  24048  qustgplem  24169  tngngp3  24704  reperflem  24867  nmhmcn  25170  iscau2  25327  iscmet3lem2  25342  ivthlem2  25502  ovolmge0  25527  itg2seq  25792  limciun  25944  dvres  25961  dveflem  26029  lhop1  26064  ftc1lem6  26091  mdegnn0cl  26119  aalioulem6  26389  lgsqrmod  27404  gausslemma2dlem3  27420  2sqreulem1  27498  2sqreunnlem1  27501  2sqreulem3  27505  pntlem3  27661  ltslpss  27989  axlowdimlem16  29115  axcontlem12  29133  umgrislfupgrlem  29280  uhgr2edg  29366  ushgredgedg  29387  ushgredgedgloop  29389  nbuhgr2vtx1edgb  29510  edgnbusgreu  29525  usgredgsscusgredg  29617  wlkdlem2  29839  pthdivtx  29884  upgrwlkdvdelem  29893  spthonepeq  29909  pthdlem1  29923  wwlksnprcl  29996  wlknewwlksn  30044  clwlkclwwlklem2a4  30156  clwlkclwwlklem2  30159  clwwlkwwlksb  30213  clwwlknun  30271  uhgr3cyclexlem  30340  eucrctshift  30402  frgrncvvdeqlem2  30459  frgrncvvdeqlem9  30466  numclwwlk1lem2foa  30513  numclwwlk1lem2f1  30516  ubthlem2  31031  shsvs  31483  mdsl2i  32482  mdsl2bi  32483  mdslmd1lem1  32485  atss  32506  chcv1  32515  chrelat2i  32525  atexch  32541  cdj3lem1  32594  bian1dOLD  32615  disjxpin  32748  fpwrelmap  32896  nn0min  32984  sigaclci  34390  dya2iocuni  34541  omssubadd  34558  fnrelpredd  35348  umgr2cycllem  35451  subfacp1lem6  35496  fmlasuc  35697  satffunlem  35712  satffunlem1lem1  35713  satffunlem2lem1  35715  mthmblem  35891  dfon2lem6  36097  dfrdg4  36262  altopth2  36277  cgrtriv  36313  cgrextend  36319  lineext  36387  btwnconn1  36412  colinbtwnle  36429  trer  36637  elicc3  36638  poimirlem27  38107  poimirlem29  38109  poimir  38113  itg2addnc  38134  ftc1cnnc  38152  areacirclem1  38168  prnc  38527  ispridlc  38530  refressn  38993  lcvexchlem4  39622  lcvexchlem5  39623  lkrss2N  39754  cvrnbtwn  39856  hlrelat2  39988  atle  40021  lvolex3N  40123  lplnnlelln  40128  llncvrlpln2  40142  lvolnlelln  40169  lvolnlelpln  40170  lplncvrlvol2  40200  snatpsubN  40335  linepsubN  40337  pmodlem2  40432  linepsubclN  40536  dihatexv  41923  eldioph2b  43305  pell1234qrreccl  43392  islssfg2  43609  hbtlem2  43662  onexomgt  43779  cantnfresb  43862  clss2lem  44148  clsk1indlem3  44580  mnuop3d  44808  sspwtrALT2  45359  relpfrlem  45490  fcoresf1  47624  2reu3  47665  2reu8i  47668  elsetpreimafvbi  47958  iccpartres  47985  iccpartiltu  47989  icceuelpart  48003  sprsymrelfvlem  48057  prpair  48068  prproropf1olem4  48073  prprelb  48083  nprmmul2  48095  goldbachthlem2  48116  lighneallem4  48180  requad2  48206  sbgoldbwt  48360  sbgoldbst  48361  nnsum4primesoddALTV  48380  nnsum4primeseven  48383  nnsum4primesevenALTV  48384  bgoldbtbndlem2  48389  uhgrimisgrgric  48514  grtriprop  48524  isubgr3stgrlem4  48552  isubgr3stgrlem6  48554  uspgrlimlem4  48574  grlimedgclnbgr  48578  grlimprclnbgrvtx  48582  gpgedg2ov  48649  gpgedg2iv  48650  pgnbgreunbgrlem1  48696  pgnbgreunbgrlem2  48700  pgnbgreunbgrlem4  48702  pgnbgreunbgrlem5  48706  rhmsubcALTVlem4  48867  srhmsubcALTV  48908  ztprmneprm  48930  pgrpgt2nabl  48949  snlindsntor  49054  elbigo2  49135  eenglngeehlnm  49322  itschlc0yqe  49343  itscnhlc0xyqsol  49348  itsclc0  49354  itsclquadeu  49360