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  2512  elneeldif  3916  unineq  4237  2nreu  4405  3elpr2eq  4869  tz7.7  6387  ordsssuc2  6455  fpropnf1  7268  nnsuc  7884  releldmdifi  8046  el2mpocsbcl  8086  poxp  8130  suppimacnv  8176  ressuppss  8185  onnseq  8337  tz7.49  8438  oaass  8552  omordi  8557  nnmordi  8623  naddelim  8679  eroprf  8819  xpdom2  9074  unfi  9169  infsupprpr  9480  inf3lem2  9612  trcl  9711  r1pwss  9770  cardaleph  10096  dfac2b  10137  axcc4  10445  acncc  10446  zorn2lem7  10508  iundom2g  10552  cfpwsdom  10597  grothomex  10842  ltexprlem2  11050  1re  11236  00id  11413  mulge0  11760  nn0ge2m1nn  12602  zle0orge1  12636  xrlttr  13195  xmullem2  13321  snunioo  13535  fzen  13599  eluzgtdifelfzo  13787  ssfzo12bi  13821  modirr  14010  hashfundm  14511  hash2pr  14538  hash3tr  14560  hash3tpde  14562  cshf1  14885  cshweqrep  14896  limsupbnd2  15574  climrlim2  15638  climuni  15643  mulcn2  15687  serf0  15772  cvgcmp  15907  ntrivcvg  15990  smuval2  16578  dfgcd2  16642  lcmgcdlem  16702  lcmdvds  16704  lcmf  16729  qnumdencl  16836  infpnlem1  17008  ram0  17120  prmgaplem6  17154  prmgaplem7  17155  prmlem1  17205  prmlem2  17218  setsstruct  17274  catass  17780  inveq  17869  sscfn1  17912  catsubcat  17934  subccocl  17940  funcco  17966  initoeu2  18111  funcestrcsetclem8  18241  funcsetcestrclem8  18256  mgmpropd  18749  idressidex0  18779  idressid  18781  gsmsymgrfixlem1  19560  psgnran  19648  efgi  19852  efgi2  19858  cntzcmnss  19974  telgsumfzs  20122  dprddisj2  20174  rnghmsubcsetclem2  20800  funcrngcsetc  20808  rhmsubcsetclem2  20829  rhmsubcrngclem2  20835  funcringcsetc  20842  srhmsubc  20848  rhmsubclem4  20856  rnglidlmcl  21410  df2idl2crng  21490  prmirredlem  21691  psgnghm  21799  scmatghm  22761  cpmatacl  22947  pm2mpf1  23030  fvmptnn04if  23080  lmcls  23533  isfild  24090  flffbas  24227  cnpflf2  24232  qustgplem  24353  tngngp3  24888  reperflem  25051  nmhmcn  25354  iscau2  25511  iscmet3lem2  25526  ivthlem2  25686  ovolmge0  25711  itg2seq  25976  limciun  26128  dvres  26145  dveflem  26213  lhop1  26248  ftc1lem6  26275  mdegnn0cl  26303  aalioulem6  26580  lgsqrmod  27596  gausslemma2dlem3  27612  2sqreulem1  27690  2sqreunnlem1  27693  2sqreulem3  27697  pntlem3  27853  ltslpss  28181  axlowdimlem16  29422  axcontlem12  29440  umgrislfupgrlem  29587  uhgr2edg  29676  ushgredgedg  29697  ushgredgedgloop  29699  nbuhgr2vtx1edgb  29820  edgnbusgreu  29835  usgredgsscusgredg  29927  wlkdlem2  30149  pthdivtx  30199  upgrwlkdvdelem  30209  spthonepeq  30225  pthdlem1  30239  wwlksnprcl  30315  wlknewwlksn  30363  clwlkclwwlklem2a4  30475  clwlkclwwlklem2  30478  clwwlkwwlksb  30532  clwwlknun  30590  uhgr3cyclexlem  30669  eucrctshift  30731  frgrncvvdeqlem2  30788  frgrncvvdeqlem9  30795  numclwwlk1lem2foa  30842  numclwwlk1lem2f1  30845  ubthlem2  31360  shsvs  31812  mdsl2i  32811  mdsl2bi  32812  mdslmd1lem1  32814  atss  32835  chcv1  32844  chrelat2i  32854  atexch  32870  cdj3lem1  32923  disjxpin  33069  fpwrelmap  33212  nn0min  33299  sigaclci  34650  dya2iocuni  34802  omssubadd  34819  fnrelpredd  35604  subfacp1lem6  35772  fmlasuc  35973  satffunlem  35988  satffunlem1lem1  35989  satffunlem2lem1  35991  mthmblem  36167  dfon2lem6  36373  dfrdg4  36538  altopth2  36554  cgrtriv  36590  cgrextend  36596  lineext  36664  btwnconn1  36689  colinbtwnle  36706  trer  36943  elicc3  36944  poimirlem27  38404  poimirlem29  38406  poimir  38410  itg2addnc  38431  ftc1cnnc  38449  areacirclem1  38465  prnc  38825  ispridlc  38828  refressn  39289  lcvexchlem4  39918  lcvexchlem5  39919  lkrss2N  40050  cvrnbtwn  40152  hlrelat2  40284  atle  40317  lvolex3N  40419  lplnnlelln  40424  llncvrlpln2  40438  lvolnlelln  40465  lvolnlelpln  40466  lplncvrlvol2  40496  snatpsubN  40631  linepsubN  40633  pmodlem2  40728  linepsubclN  40832  dihatexv  42219  eldioph2b  43616  pell1234qrreccl  43703  islssfg2  43920  hbtlem2  43973  onexomgt  44090  cantnfresb  44173  clss2lem  44459  clsk1indlem3  44891  mnuop3d  45103  sspwtrALT2  45653  relpfrlem  45784  fcoresf1  47965  2reu3  48006  2reu8i  48009  elsetpreimafvbi  48299  iccpartres  48326  iccpartiltu  48330  icceuelpart  48344  sprsymrelfvlem  48398  prpair  48409  prproropf1olem4  48414  prprelb  48424  nprmmul2  48436  goldbachthlem2  48457  lighneallem4  48521  requad2  48547  sbgoldbwt  48701  sbgoldbst  48702  nnsum4primesoddALTV  48721  nnsum4primeseven  48724  nnsum4primesevenALTV  48725  bgoldbtbndlem2  48730  uhgrimisgrgric  48855  grtriprop  48865  isubgr3stgrlem4  48893  isubgr3stgrlem6  48895  uspgrlimlem4  48915  grlimedgclnbgr  48919  grlimprclnbgrvtx  48923  gpgedg2ov  48990  gpgedg2iv  48991  pgnbgreunbgrlem1  49037  pgnbgreunbgrlem2  49041  pgnbgreunbgrlem4  49043  pgnbgreunbgrlem5  49047  rhmsubcALTVlem4  49207  srhmsubcALTV  49248  ztprmneprm  49285  pgrpgt2nabl  49304  snlindsntor  49409  elbigo2  49490  eenglngeehlnm  49677  itschlc0yqe  49698  itscnhlc0xyqsol  49703  itsclc0  49709  itsclquadeu  49715