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  3917  unineq  4242  2nreu  4398  3elpr2eq  4864  tz7.7  6351  ordsssuc2  6418  fpropnf1  7223  nnsuc  7836  releldmdifi  7999  el2mpocsbcl  8037  poxp  8080  suppimacnv  8126  ressuppss  8135  onnseq  8286  tz7.49  8386  oaass  8498  omordi  8503  nnmordi  8569  naddelim  8624  eroprf  8764  xpdom2  9012  unfi  9107  infsupprpr  9421  inf3lem2  9550  trcl  9649  r1pwss  9708  cardaleph  10011  dfac2b  10053  axcc4  10361  acncc  10362  zorn2lem7  10424  iundom2g  10462  cfpwsdom  10507  grothomex  10752  ltexprlem2  10960  1re  11144  00id  11320  mulge0  11667  nn0ge2m1nn  12483  zle0orge1  12517  xrlttr  13066  xmullem2  13192  snunioo  13406  fzen  13469  eluzgtdifelfzo  13655  ssfzo12bi  13689  modirr  13877  hashfundm  14377  hash2pr  14404  hash3tr  14426  hash3tpde  14428  cshf1  14745  cshweqrep  14756  limsupbnd2  15418  climrlim2  15482  climuni  15487  mulcn2  15531  serf0  15616  cvgcmp  15751  ntrivcvg  15832  smuval2  16421  dfgcd2  16485  lcmgcdlem  16545  lcmdvds  16547  lcmf  16572  qnumdencl  16678  infpnlem1  16850  ram0  16962  prmgaplem6  16996  prmgaplem7  16997  prmlem1  17047  prmlem2  17059  setsstruct  17115  catass  17621  inveq  17710  sscfn1  17753  catsubcat  17775  subccocl  17781  funcco  17807  initoeu2  17952  funcestrcsetclem8  18082  funcsetcestrclem8  18097  mgmpropd  18588  gsmsymgrfixlem1  19368  psgnran  19456  efgi  19660  efgi2  19666  cntzcmnss  19782  telgsumfzs  19930  dprddisj2  19982  rnghmsubcsetclem2  20577  funcrngcsetc  20585  rhmsubcsetclem2  20606  rhmsubcrngclem2  20612  funcringcsetc  20619  srhmsubc  20625  rhmsubclem4  20633  rnglidlmcl  21183  prmirredlem  21439  psgnghm  21547  scmatghm  22489  cpmatacl  22672  pm2mpf1  22755  fvmptnn04if  22805  lmcls  23258  isfild  23814  flffbas  23951  cnpflf2  23956  qustgplem  24077  tngngp3  24612  reperflem  24775  nmhmcn  25088  iscau2  25245  iscmet3lem2  25260  ivthlem2  25421  ovolmge0  25446  itg2seq  25711  limciun  25863  dvres  25880  dveflem  25951  lhop1  25987  ftc1lem6  26016  mdegnn0cl  26044  aalioulem6  26313  lgsqrmod  27331  gausslemma2dlem3  27347  2sqreulem1  27425  2sqreunnlem1  27428  2sqreulem3  27432  pntlem3  27588  ltslpss  27916  axlowdimlem16  29042  axcontlem12  29060  umgrislfupgrlem  29207  uhgr2edg  29293  ushgredgedg  29314  ushgredgedgloop  29316  nbuhgr2vtx1edgb  29437  edgnbusgreu  29452  usgredgsscusgredg  29545  wlkdlem2  29767  pthdivtx  29812  upgrwlkdvdelem  29821  spthonepeq  29837  pthdlem1  29851  wwlksnprcl  29924  wlknewwlksn  29972  clwlkclwwlklem2a4  30084  clwlkclwwlklem2  30087  clwwlkwwlksb  30141  clwwlknun  30199  uhgr3cyclexlem  30268  eucrctshift  30330  frgrncvvdeqlem2  30387  frgrncvvdeqlem9  30394  numclwwlk1lem2foa  30441  numclwwlk1lem2f1  30444  ubthlem2  30959  shsvs  31411  mdsl2i  32410  mdsl2bi  32411  mdslmd1lem1  32413  atss  32434  chcv1  32443  chrelat2i  32453  atexch  32469  cdj3lem1  32522  bian1dOLD  32543  disjxpin  32675  fpwrelmap  32823  nn0min  32912  sigaclci  34310  dya2iocuni  34461  omssubadd  34478  fnrelpredd  35268  umgr2cycllem  35356  subfacp1lem6  35401  fmlasuc  35602  satffunlem  35617  satffunlem1lem1  35618  satffunlem2lem1  35620  mthmblem  35796  dfon2lem6  36002  dfrdg4  36167  altopth2  36182  cgrtriv  36218  cgrextend  36224  lineext  36292  btwnconn1  36317  colinbtwnle  36334  trer  36532  elicc3  36533  poimirlem27  37898  poimirlem29  37900  poimir  37904  itg2addnc  37925  ftc1cnnc  37943  areacirclem1  37959  prnc  38318  ispridlc  38321  refressn  38784  lcvexchlem4  39413  lcvexchlem5  39414  lkrss2N  39545  cvrnbtwn  39647  hlrelat2  39779  atle  39812  lvolex3N  39914  lplnnlelln  39919  llncvrlpln2  39933  lvolnlelln  39960  lvolnlelpln  39961  lplncvrlvol2  39991  snatpsubN  40126  linepsubN  40128  pmodlem2  40223  linepsubclN  40327  dihatexv  41714  eldioph2b  43120  pell1234qrreccl  43211  islssfg2  43428  hbtlem2  43481  onexomgt  43598  cantnfresb  43681  clss2lem  43967  clsk1indlem3  44399  mnuop3d  44627  sspwtrALT2  45178  relpfrlem  45309  fcoresf1  47429  2reu3  47470  2reu8i  47473  elsetpreimafvbi  47751  iccpartres  47778  iccpartiltu  47782  icceuelpart  47796  sprsymrelfvlem  47850  prpair  47861  prproropf1olem4  47866  prprelb  47876  goldbachthlem2  47906  lighneallem4  47970  requad2  47983  sbgoldbwt  48137  sbgoldbst  48138  nnsum4primesoddALTV  48157  nnsum4primeseven  48160  nnsum4primesevenALTV  48161  bgoldbtbndlem2  48166  uhgrimisgrgric  48291  grtriprop  48301  isubgr3stgrlem4  48329  isubgr3stgrlem6  48331  uspgrlimlem4  48351  grlimedgclnbgr  48355  grlimprclnbgrvtx  48359  gpgedg2ov  48426  gpgedg2iv  48427  pgnbgreunbgrlem1  48473  pgnbgreunbgrlem2  48477  pgnbgreunbgrlem4  48479  pgnbgreunbgrlem5  48483  rhmsubcALTVlem4  48644  srhmsubcALTV  48685  ztprmneprm  48707  pgrpgt2nabl  48726  snlindsntor  48831  elbigo2  48912  eenglngeehlnm  49099  itschlc0yqe  49120  itscnhlc0xyqsol  49125  itsclc0  49131  itsclquadeu  49137