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  621  jaoa  958  dedlema  1046  dedlemb  1047  prlem1  1055  dfsb1  2486  elneeldif  3904  unineq  4229  2nreu  4385  3elpr2eq  4850  tz7.7  6343  ordsssuc2  6410  fpropnf1  7215  nnsuc  7828  releldmdifi  7991  el2mpocsbcl  8028  poxp  8071  suppimacnv  8117  ressuppss  8126  onnseq  8277  tz7.49  8377  oaass  8489  omordi  8494  nnmordi  8560  naddelim  8615  eroprf  8755  xpdom2  9003  unfi  9098  infsupprpr  9412  inf3lem2  9541  trcl  9640  r1pwss  9699  cardaleph  10002  dfac2b  10044  axcc4  10352  acncc  10353  zorn2lem7  10415  iundom2g  10453  cfpwsdom  10498  grothomex  10743  ltexprlem2  10951  1re  11135  00id  11312  mulge0  11659  nn0ge2m1nn  12498  zle0orge1  12532  xrlttr  13082  xmullem2  13208  snunioo  13422  fzen  13486  eluzgtdifelfzo  13673  ssfzo12bi  13707  modirr  13895  hashfundm  14395  hash2pr  14422  hash3tr  14444  hash3tpde  14446  cshf1  14763  cshweqrep  14774  limsupbnd2  15436  climrlim2  15500  climuni  15505  mulcn2  15549  serf0  15634  cvgcmp  15770  ntrivcvg  15853  smuval2  16442  dfgcd2  16506  lcmgcdlem  16566  lcmdvds  16568  lcmf  16593  qnumdencl  16700  infpnlem1  16872  ram0  16984  prmgaplem6  17018  prmgaplem7  17019  prmlem1  17069  prmlem2  17081  setsstruct  17137  catass  17643  inveq  17732  sscfn1  17775  catsubcat  17797  subccocl  17803  funcco  17829  initoeu2  17974  funcestrcsetclem8  18104  funcsetcestrclem8  18119  mgmpropd  18610  gsmsymgrfixlem1  19393  psgnran  19481  efgi  19685  efgi2  19691  cntzcmnss  19807  telgsumfzs  19955  dprddisj2  20007  rnghmsubcsetclem2  20600  funcrngcsetc  20608  rhmsubcsetclem2  20629  rhmsubcrngclem2  20635  funcringcsetc  20642  srhmsubc  20648  rhmsubclem4  20656  rnglidlmcl  21206  prmirredlem  21462  psgnghm  21570  scmatghm  22508  cpmatacl  22691  pm2mpf1  22774  fvmptnn04if  22824  lmcls  23277  isfild  23833  flffbas  23970  cnpflf2  23975  qustgplem  24096  tngngp3  24631  reperflem  24794  nmhmcn  25097  iscau2  25254  iscmet3lem2  25269  ivthlem2  25429  ovolmge0  25454  itg2seq  25719  limciun  25871  dvres  25888  dveflem  25956  lhop1  25991  ftc1lem6  26018  mdegnn0cl  26046  aalioulem6  26314  lgsqrmod  27329  gausslemma2dlem3  27345  2sqreulem1  27423  2sqreunnlem1  27426  2sqreulem3  27430  pntlem3  27586  ltslpss  27914  axlowdimlem16  29040  axcontlem12  29058  umgrislfupgrlem  29205  uhgr2edg  29291  ushgredgedg  29312  ushgredgedgloop  29314  nbuhgr2vtx1edgb  29435  edgnbusgreu  29450  usgredgsscusgredg  29543  wlkdlem2  29765  pthdivtx  29810  upgrwlkdvdelem  29819  spthonepeq  29835  pthdlem1  29849  wwlksnprcl  29922  wlknewwlksn  29970  clwlkclwwlklem2a4  30082  clwlkclwwlklem2  30085  clwwlkwwlksb  30139  clwwlknun  30197  uhgr3cyclexlem  30266  eucrctshift  30328  frgrncvvdeqlem2  30385  frgrncvvdeqlem9  30392  numclwwlk1lem2foa  30439  numclwwlk1lem2f1  30442  ubthlem2  30957  shsvs  31409  mdsl2i  32408  mdsl2bi  32409  mdslmd1lem1  32411  atss  32432  chcv1  32441  chrelat2i  32451  atexch  32467  cdj3lem1  32520  bian1dOLD  32541  disjxpin  32673  fpwrelmap  32821  nn0min  32909  sigaclci  34292  dya2iocuni  34443  omssubadd  34460  fnrelpredd  35250  umgr2cycllem  35338  subfacp1lem6  35383  fmlasuc  35584  satffunlem  35599  satffunlem1lem1  35600  satffunlem2lem1  35602  mthmblem  35778  dfon2lem6  35984  dfrdg4  36149  altopth2  36164  cgrtriv  36200  cgrextend  36206  lineext  36274  btwnconn1  36299  colinbtwnle  36316  trer  36514  elicc3  36515  poimirlem27  37982  poimirlem29  37984  poimir  37988  itg2addnc  38009  ftc1cnnc  38027  areacirclem1  38043  prnc  38402  ispridlc  38405  refressn  38868  lcvexchlem4  39497  lcvexchlem5  39498  lkrss2N  39629  cvrnbtwn  39731  hlrelat2  39863  atle  39896  lvolex3N  39998  lplnnlelln  40003  llncvrlpln2  40017  lvolnlelln  40044  lvolnlelpln  40045  lplncvrlvol2  40075  snatpsubN  40210  linepsubN  40212  pmodlem2  40307  linepsubclN  40411  dihatexv  41798  eldioph2b  43209  pell1234qrreccl  43300  islssfg2  43517  hbtlem2  43570  onexomgt  43687  cantnfresb  43770  clss2lem  44056  clsk1indlem3  44488  mnuop3d  44716  sspwtrALT2  45267  relpfrlem  45398  fcoresf1  47529  2reu3  47570  2reu8i  47573  elsetpreimafvbi  47863  iccpartres  47890  iccpartiltu  47894  icceuelpart  47908  sprsymrelfvlem  47962  prpair  47973  prproropf1olem4  47978  prprelb  47988  nprmmul2  48000  goldbachthlem2  48021  lighneallem4  48085  requad2  48111  sbgoldbwt  48265  sbgoldbst  48266  nnsum4primesoddALTV  48285  nnsum4primeseven  48288  nnsum4primesevenALTV  48289  bgoldbtbndlem2  48294  uhgrimisgrgric  48419  grtriprop  48429  isubgr3stgrlem4  48457  isubgr3stgrlem6  48459  uspgrlimlem4  48479  grlimedgclnbgr  48483  grlimprclnbgrvtx  48487  gpgedg2ov  48554  gpgedg2iv  48555  pgnbgreunbgrlem1  48601  pgnbgreunbgrlem2  48605  pgnbgreunbgrlem4  48607  pgnbgreunbgrlem5  48611  rhmsubcALTVlem4  48772  srhmsubcALTV  48813  ztprmneprm  48835  pgrpgt2nabl  48854  snlindsntor  48959  elbigo2  49040  eenglngeehlnm  49227  itschlc0yqe  49248  itscnhlc0xyqsol  49253  itsclc0  49259  itsclquadeu  49265