Theorem adantld 496

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  im2anan9  632  jaoa  970  dedlema  1061  dedlemb  1062  prlem1  1070  dfsb1  2510  elneeldif  4053  unineq  4233  2nreu  4401  3elpr2eq  4833  tz7.7  6388  ordsssuc2  6456  fpropnf1  7272  nnsuc  7896  releldmdifi  8057  el2mpocsbcl  8097  poxp  8143  suppimacnv  8195  ressuppss  8204  onnseq  8356  tz7.49  8459  oaass  8573  omordi  8578  nnmordi  8644  naddelim  8700  eroprf  8840  xpdom2  9095  unfi  9190  infsupprpr  9502  inf3lem2  9634  trcl  9733  r1pwss  9795  cardaleph  10172  dfac2b  10213  axcc4  10521  acncc  10522  zorn2lem7  10584  iundom2g  10628  cfpwsdom  10673  grothomex  10918  ltexprlem2  11126  1re  11312  00id  11489  mulge0  11838  nn0ge2m1nn  12680  zle0orge1  12714  xrlttr  13273  xmullem2  13399  snunioo  13613  fzen  13678  eluzgtdifelfzo  13866  ssfzo12bi  13900  modirr  14089  hashfundm  14591  hash2pr  14618  hash3tr  14640  hash3tpde  14642  cshf1  14966  cshweqrep  14977  limsupbnd2  15656  climrlim2  15720  climuni  15725  mulcn2  15769  serf0  15854  cvgcmp  15989  ntrivcvg  16072  smuval2  16658  dfgcd2  16725  lcmgcdlem  16787  lcmdvds  16789  lcmf  16814  qnumdencl  16921  infpnlem1  17094  ram0  17206  prmgaplem6  17240  prmgaplem7  17241  prmlem1  17291  prmlem2  17304  setsstruct  17360  catass  17866  inveq  17955  sscfn1  17998  catsubcat  18020  subccocl  18026  funcco  18052  initoeu2  18197  funcestrcsetclem8  18327  funcsetcestrclem8  18342  mgmpropd  18835  idressidex0  18866  idressid  18868  gsmsymgrfixlem1  19647  psgnran  19735  efgi  19939  efgi2  19945  cntzcmnss  20061  telgsumfzs  20209  dprddisj2  20261  rnghmsubcsetclem2  20890  funcrngcsetc  20898  rhmsubcsetclem2  20919  rhmsubcrngclem2  20925  funcringcsetc  20932  srhmsubc  20938  rhmsubclem4  20946  rnglidlmcl  21501  df2idl2crng  21583  prmirredlem  21784  psgnghm  21892  scmatghm  22854  cpmatacl  23040  pm2mpf1  23123  fvmptnn04if  23173  lmcls  23626  isfild  24183  flffbas  24320  cnpflf2  24325  qustgplem  24446  tngngp3  24981  reperflem  25144  nmhmcn  25447  iscau2  25604  iscmet3lem2  25619  ivthlem2  25779  ovolmge0  25804  itg2seq  26069  limciun  26220  dvres  26237  dveflem  26305  lhop1  26340  ftc1lem6  26367  mdegnn0cl  26395  aalioulem6  26670  lgsqrmod  27685  gausslemma2dlem3  27701  2sqreulem1  27779  2sqreunnlem1  27782  2sqreulem3  27786  pntlem3  27942  ltslpss  28300  axlowdimlem16  29541  axcontlem12  29559  umgrislfupgrlem  29706  uhgr2edg  29795  ushgredgedg  29816  ushgredgedgloop  29818  nbuhgr2vtx1edgb  29939  edgnbusgreu  29954  usgredgsscusgredg  30046  wlkdlem2  30268  pthdivtx  30318  upgrwlkdvdelem  30328  spthonepeq  30344  pthdlem1  30358  wwlksnprcl  30434  wlknewwlksn  30482  clwlkclwwlklem2a4  30594  clwlkclwwlklem2  30597  clwwlkwwlksb  30651  clwwlknun  30709  uhgr3cyclexlem  30788  eucrctshift  30850  frgrncvvdeqlem2  30907  frgrncvvdeqlem9  30914  numclwwlk1lem2foa  30961  numclwwlk1lem2f1  30964  ubthlem2  31479  shsvs  31931  mdsl2i  32930  mdsl2bi  32931  mdslmd1lem1  32933  atss  32954  chcv1  32963  chrelat2i  32973  atexch  32989  cdj3lem1  33042  disjxpin  33230  fpwrelmap  33372  nn0min  33459  sigaclci  34811  dya2iocuni  34962  omssubadd  34979  fnrelpredd  35773  onprcf1acwevdlem1  35965  srepdflem1  36005  subfacp1lem6  36037  fmlasuc  36238  satffunlem  36253  satffunlem1lem1  36254  satffunlem2lem1  36256  mthmblem  36432  dfon2lem6  36643  dfrdg4  36808  altopth2  36824  cgrtriv  36860  cgrextend  36866  lineext  36934  btwnconn1  36959  colinbtwnle  36976  trer  37197  elicc3  37198  poimirlem27  38659  poimirlem29  38661  poimir  38665  itg2addnc  38686  ftc1cnnc  38704  areacirclem1  38720  prnc  39095  ispridlc  39098  refressn  39559  lcvexchlem4  40188  lcvexchlem5  40189  lkrss2N  40320  cvrnbtwn  40422  hlrelat2  40554  atle  40587  lvolex3N  40689  lplnnlelln  40694  llncvrlpln2  40708  lvolnlelln  40735  lvolnlelpln  40736  lplncvrlvol2  40766  snatpsubN  40901  linepsubN  40903  pmodlem2  40998  linepsubclN  41102  dihatexv  42489  eldioph2b  43868  pell1234qrreccl  43955  islssfg2  44167  hbtlem2  44220  onexomgt  44337  cantnfresb  44420  clss2lem  44705  clsk1indlem3  45137  mnuop3d  45349  sspwtrALT2  45899  relpfrlem  46037  fcoresf1  48233  2reu3  48274  2reu8i  48277  elsetpreimafvbi  48567  iccpartres  48594  iccpartiltu  48598  icceuelpart  48612  sprsymrelfvlem  48666  prpair  48677  prproropf1olem4  48682  prprelb  48692  nprmmul2  48704  goldbachthlem2  48725  lighneallem4  48789  requad2  48815  sbgoldbwt  48969  sbgoldbst  48970  nnsum4primesoddALTV  48989  nnsum4primeseven  48992  nnsum4primesevenALTV  48993  bgoldbtbndlem2  48998  uhgrimisgrgric  49123  grtriprop  49133  isubgr3stgrlem4  49161  isubgr3stgrlem6  49163  uspgrlimlem4  49183  grlimedgclnbgr  49187  grlimprclnbgrvtx  49191  gpgedg2ov  49258  gpgedg2iv  49259  pgnbgreunbgrlem1  49305  pgnbgreunbgrlem2  49309  pgnbgreunbgrlem4  49311  pgnbgreunbgrlem5  49315  rhmsubcALTVlem4  49475  srhmsubcALTV  49516  ztprmneprm  49553  pgrpgt2nabl  49572  snlindsntor  49677  elbigo2  49758  itschlc0yqe  49966  itscnhlc0xyqsol  49971  itsclc0  49977  itsclquadeu  49983