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  619  jaoa  956  dedlema  1046  dedlemb  1047  prlem1  1055  dfsb1  2489  elneeldif  3990  unineq  4307  2nreu  4467  3elpr2eq  4930  tz7.7  6421  ordsssuc2  6486  fpropnf1  7304  nnsuc  7921  releldmdifi  8086  el2mpocsbcl  8126  poxp  8169  suppimacnv  8215  ressuppss  8224  onnseq  8400  tz7.49  8501  oaass  8617  omordi  8622  nnmordi  8687  naddelim  8742  eroprf  8873  xpdom2  9133  unfi  9238  infsupprpr  9573  inf3lem2  9698  trcl  9797  r1pwss  9853  cardaleph  10158  dfac2b  10200  axcc4  10508  acncc  10509  zorn2lem7  10571  iundom2g  10609  cfpwsdom  10653  grothomex  10898  ltexprlem2  11106  1re  11290  00id  11465  mulge0  11808  nn0ge2m1nn  12622  zle0orge1  12656  xrlttr  13202  xmullem2  13327  snunioo  13538  fzen  13601  eluzgtdifelfzo  13778  ssfzo12bi  13811  modirr  13993  hashfundm  14491  hash2pr  14518  hash3tr  14540  hash3tpde  14542  cshf1  14858  cshweqrep  14869  limsupbnd2  15529  climrlim2  15593  climuni  15598  mulcn2  15642  serf0  15729  cvgcmp  15864  ntrivcvg  15945  smuval2  16528  dfgcd2  16593  lcmgcdlem  16653  lcmdvds  16655  lcmf  16680  qnumdencl  16786  infpnlem1  16957  ram0  17069  prmgaplem6  17103  prmgaplem7  17104  prmlem1  17155  prmlem2  17167  setsstruct  17223  catass  17744  inveq  17835  sscfn1  17878  catsubcat  17903  subccocl  17909  funcco  17935  initoeu2  18083  funcestrcsetclem8  18216  funcsetcestrclem8  18231  mgmpropd  18689  gsmsymgrfixlem1  19469  psgnran  19557  efgi  19761  efgi2  19767  cntzcmnss  19883  telgsumfzs  20031  dprddisj2  20083  rnghmsubcsetclem2  20654  funcrngcsetc  20662  rhmsubcsetclem2  20683  rhmsubcrngclem2  20689  funcringcsetc  20696  srhmsubc  20702  rhmsubclem4  20710  rnglidlmcl  21249  prmirredlem  21506  psgnghm  21621  scmatghm  22560  cpmatacl  22743  pm2mpf1  22826  fvmptnn04if  22876  lmcls  23331  isfild  23887  flffbas  24024  cnpflf2  24029  qustgplem  24150  tngngp3  24698  reperflem  24859  nmhmcn  25172  iscau2  25330  iscmet3lem2  25345  ivthlem2  25506  ovolmge0  25531  itg2seq  25797  limciun  25949  dvres  25966  dveflem  26037  lhop1  26073  ftc1lem6  26102  mdegnn0cl  26130  aalioulem6  26397  lgsqrmod  27414  gausslemma2dlem3  27430  2sqreulem1  27508  2sqreunnlem1  27511  2sqreulem3  27515  pntlem3  27671  sltlpss  27963  axlowdimlem16  28990  axcontlem12  29008  umgrislfupgrlem  29157  uhgr2edg  29243  ushgredgedg  29264  ushgredgedgloop  29266  nbuhgr2vtx1edgb  29387  edgnbusgreu  29402  usgredgsscusgredg  29495  wlkdlem2  29719  pthdivtx  29765  upgrwlkdvdelem  29772  spthonepeq  29788  pthdlem1  29802  wwlksnprcl  29872  wlknewwlksn  29920  clwlkclwwlklem2a4  30029  clwlkclwwlklem2  30032  clwwlkwwlksb  30086  clwwlknun  30144  uhgr3cyclexlem  30213  eucrctshift  30275  frgrncvvdeqlem2  30332  frgrncvvdeqlem9  30339  numclwwlk1lem2foa  30386  numclwwlk1lem2f1  30389  ubthlem2  30903  shsvs  31355  mdsl2i  32354  mdsl2bi  32355  mdslmd1lem1  32357  atss  32378  chcv1  32387  chrelat2i  32397  atexch  32413  cdj3lem1  32466  bian1dOLD  32485  disjxpin  32610  fpwrelmap  32747  nn0min  32824  sigaclci  34096  dya2iocuni  34248  omssubadd  34265  fnrelpredd  35065  umgr2cycllem  35108  subfacp1lem6  35153  fmlasuc  35354  satffunlem  35369  satffunlem1lem1  35370  satffunlem2lem1  35372  mthmblem  35548  dfon2lem6  35752  dfrdg4  35915  altopth2  35930  cgrtriv  35966  cgrextend  35972  lineext  36040  btwnconn1  36065  colinbtwnle  36082  trer  36282  elicc3  36283  poimirlem27  37607  poimirlem29  37609  poimir  37613  itg2addnc  37634  ftc1cnnc  37652  areacirclem1  37668  prnc  38027  ispridlc  38030  refressn  38399  lcvexchlem4  38993  lcvexchlem5  38994  lkrss2N  39125  cvrnbtwn  39227  hlrelat2  39360  atle  39393  lvolex3N  39495  lplnnlelln  39500  llncvrlpln2  39514  lvolnlelln  39541  lvolnlelpln  39542  lplncvrlvol2  39572  snatpsubN  39707  linepsubN  39709  pmodlem2  39804  linepsubclN  39908  dihatexv  41295  eldioph2b  42719  pell1234qrreccl  42810  islssfg2  43028  hbtlem2  43081  onexomgt  43202  cantnfresb  43286  clss2lem  43573  clsk1indlem3  44005  mnuop3d  44240  sspwtrALT2  44794  fcoresf1  46984  2reu3  47025  2reu8i  47028  elsetpreimafvbi  47265  iccpartres  47292  iccpartiltu  47296  icceuelpart  47310  sprsymrelfvlem  47364  prpair  47375  prproropf1olem4  47380  prprelb  47390  goldbachthlem2  47420  lighneallem4  47484  requad2  47497  sbgoldbwt  47651  sbgoldbst  47652  nnsum4primesoddALTV  47671  nnsum4primeseven  47674  nnsum4primesevenALTV  47675  bgoldbtbndlem2  47680  uhgrimisgrgric  47783  grtriprop  47792  uspgrlimlem4  47815  rhmsubcALTVlem4  48007  srhmsubcALTV  48048  ztprmneprm  48072  pgrpgt2nabl  48091  snlindsntor  48200  elbigo2  48286  eenglngeehlnm  48473  itschlc0yqe  48494  itscnhlc0xyqsol  48499  itsclc0  48505  itsclquadeu  48511