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  620  jaoa  957  dedlema  1045  dedlemb  1046  prlem1  1054  dfsb1  2485  elneeldif  3964  unineq  4287  2nreu  4443  3elpr2eq  4905  tz7.7  6409  ordsssuc2  6474  fpropnf1  7288  nnsuc  7906  releldmdifi  8071  el2mpocsbcl  8111  poxp  8154  suppimacnv  8200  ressuppss  8209  onnseq  8385  tz7.49  8486  oaass  8600  omordi  8605  nnmordi  8670  naddelim  8725  eroprf  8856  xpdom2  9108  unfi  9212  infsupprpr  9545  inf3lem2  9670  trcl  9769  r1pwss  9825  cardaleph  10130  dfac2b  10172  axcc4  10480  acncc  10481  zorn2lem7  10543  iundom2g  10581  cfpwsdom  10625  grothomex  10870  ltexprlem2  11078  1re  11262  00id  11437  mulge0  11782  nn0ge2m1nn  12598  zle0orge1  12632  xrlttr  13183  xmullem2  13308  snunioo  13519  fzen  13582  eluzgtdifelfzo  13767  ssfzo12bi  13801  modirr  13984  hashfundm  14482  hash2pr  14509  hash3tr  14531  hash3tpde  14533  cshf1  14849  cshweqrep  14860  limsupbnd2  15520  climrlim2  15584  climuni  15589  mulcn2  15633  serf0  15718  cvgcmp  15853  ntrivcvg  15934  smuval2  16520  dfgcd2  16584  lcmgcdlem  16644  lcmdvds  16646  lcmf  16671  qnumdencl  16777  infpnlem1  16949  ram0  17061  prmgaplem6  17095  prmgaplem7  17096  prmlem1  17146  prmlem2  17158  setsstruct  17214  catass  17730  inveq  17819  sscfn1  17862  catsubcat  17885  subccocl  17891  funcco  17917  initoeu2  18062  funcestrcsetclem8  18193  funcsetcestrclem8  18208  mgmpropd  18665  gsmsymgrfixlem1  19446  psgnran  19534  efgi  19738  efgi2  19744  cntzcmnss  19860  telgsumfzs  20008  dprddisj2  20060  rnghmsubcsetclem2  20633  funcrngcsetc  20641  rhmsubcsetclem2  20662  rhmsubcrngclem2  20668  funcringcsetc  20675  srhmsubc  20681  rhmsubclem4  20689  rnglidlmcl  21227  prmirredlem  21484  psgnghm  21599  scmatghm  22540  cpmatacl  22723  pm2mpf1  22806  fvmptnn04if  22856  lmcls  23311  isfild  23867  flffbas  24004  cnpflf2  24009  qustgplem  24130  tngngp3  24678  reperflem  24841  nmhmcn  25154  iscau2  25312  iscmet3lem2  25327  ivthlem2  25488  ovolmge0  25513  itg2seq  25778  limciun  25930  dvres  25947  dveflem  26018  lhop1  26054  ftc1lem6  26083  mdegnn0cl  26111  aalioulem6  26380  lgsqrmod  27397  gausslemma2dlem3  27413  2sqreulem1  27491  2sqreunnlem1  27494  2sqreulem3  27498  pntlem3  27654  sltlpss  27946  axlowdimlem16  28973  axcontlem12  28991  umgrislfupgrlem  29140  uhgr2edg  29226  ushgredgedg  29247  ushgredgedgloop  29249  nbuhgr2vtx1edgb  29370  edgnbusgreu  29385  usgredgsscusgredg  29478  wlkdlem2  29702  pthdivtx  29748  upgrwlkdvdelem  29757  spthonepeq  29773  pthdlem1  29787  wwlksnprcl  29860  wlknewwlksn  29908  clwlkclwwlklem2a4  30017  clwlkclwwlklem2  30020  clwwlkwwlksb  30074  clwwlknun  30132  uhgr3cyclexlem  30201  eucrctshift  30263  frgrncvvdeqlem2  30320  frgrncvvdeqlem9  30327  numclwwlk1lem2foa  30374  numclwwlk1lem2f1  30377  ubthlem2  30891  shsvs  31343  mdsl2i  32342  mdsl2bi  32343  mdslmd1lem1  32345  atss  32366  chcv1  32375  chrelat2i  32385  atexch  32401  cdj3lem1  32454  bian1dOLD  32477  disjxpin  32602  fpwrelmap  32745  nn0min  32823  sigaclci  34134  dya2iocuni  34286  omssubadd  34303  fnrelpredd  35104  umgr2cycllem  35146  subfacp1lem6  35191  fmlasuc  35392  satffunlem  35407  satffunlem1lem1  35408  satffunlem2lem1  35410  mthmblem  35586  dfon2lem6  35790  dfrdg4  35953  altopth2  35968  cgrtriv  36004  cgrextend  36010  lineext  36078  btwnconn1  36103  colinbtwnle  36120  trer  36318  elicc3  36319  poimirlem27  37655  poimirlem29  37657  poimir  37661  itg2addnc  37682  ftc1cnnc  37700  areacirclem1  37716  prnc  38075  ispridlc  38078  refressn  38445  lcvexchlem4  39039  lcvexchlem5  39040  lkrss2N  39171  cvrnbtwn  39273  hlrelat2  39406  atle  39439  lvolex3N  39541  lplnnlelln  39546  llncvrlpln2  39560  lvolnlelln  39587  lvolnlelpln  39588  lplncvrlvol2  39618  snatpsubN  39753  linepsubN  39755  pmodlem2  39850  linepsubclN  39954  dihatexv  41341  eldioph2b  42779  pell1234qrreccl  42870  islssfg2  43088  hbtlem2  43141  onexomgt  43258  cantnfresb  43342  clss2lem  43629  clsk1indlem3  44061  mnuop3d  44295  sspwtrALT2  44848  relpfrlem  44979  fcoresf1  47086  2reu3  47127  2reu8i  47130  elsetpreimafvbi  47383  iccpartres  47410  iccpartiltu  47414  icceuelpart  47428  sprsymrelfvlem  47482  prpair  47493  prproropf1olem4  47498  prprelb  47508  goldbachthlem2  47538  lighneallem4  47602  requad2  47615  sbgoldbwt  47769  sbgoldbst  47770  nnsum4primesoddALTV  47789  nnsum4primeseven  47792  nnsum4primesevenALTV  47793  bgoldbtbndlem2  47798  uhgrimisgrgric  47904  grtriprop  47913  isubgr3stgrlem4  47941  isubgr3stgrlem6  47943  uspgrlimlem4  47963  rhmsubcALTVlem4  48205  srhmsubcALTV  48246  ztprmneprm  48268  pgrpgt2nabl  48287  snlindsntor  48393  elbigo2  48478  eenglngeehlnm  48665  itschlc0yqe  48686  itscnhlc0xyqsol  48691  itsclc0  48697  itsclquadeu  48703