Theorem adantl 388

Description: Inference adding a conjunct to the left of an antecedent.

Hypothesis

Ref	Expression
adantl.1	⊢ (φ → ψ)

Assertion

Ref	Expression
adantl	⊢ ((χ ⋀ φ) → ψ)

Proof of Theorem adantl

Step	Hyp	Ref	Expression
1		adantl.1	. . 3 ⊢ (φ → ψ)
2	1	a1i 8	. 2 ⊢ (χ → (φ → ψ))
3	2	imp 350	1 ⊢ ((χ ⋀ φ) → ψ)

Syntax hints:   → wi 3   ⋀ wa 223

This theorem is referenced by:  adantll 392  ad2antlr 405  ad2antrl 406  ad2antll 407  jaao 427  sylan9 468  mpan9 470  sylan9bb 539  im2anan9 562  im2anan9r 563  bi2bian9 633  pm5.18 659  pm5.75 748  ccase2 756  prlem1 769  3ad2ant3 801  ax11v2 1214  ax11b 1219  sbcom 1257  sbal1 1345  ax11eq 1362  ax11el 1363  ax11inda 1370  euim 1420  euor2 1436  2exeu 1445  2eu5 1452  eqeqan12d 1488  sylan9eq 1525  vtoclegft 1853  eqvinc 1880  reu3 1928  sbcthdv 1944  sbccomglem 1985  sbccomg 1986  sbcralt 1987  csbcomg 2014  hbcsb1gd 2024  hbcsbgd 2025  sylan9ss 2072  elin 2204  sspr 2472  unissel 2523  intab 2556  copsex4g 2790  solin 2853  reuuni1 2878  alxfr 2892  ralxfrALT 2896  wefrc 2939  ordelon 2967  tz7.7 2969  ordunidif 3001  onint0 3003  onnmin 3011  onmindif 3056  onmindif2 3057  ordelsuc 3067  ordsucelsuc 3069  ordtri2or2 3074  ordsucun 3078  onsucuni2 3087  nlimsucg 3108  ordunisuc2 3111  limuni3 3119  tfi 3122  peano5 3149  findsg 3153  tfinds 3157  tfindsg 3158  ssnlim 3163  brinxp 3228  ideqg 3272  relssres 3388  relimasn 3421  soirri 3438  ssxpr 3471  xpexr2 3476  unixp0 3514  funssres 3548  funun 3550  fununi 3559  resfunexg 3575  cofunexg 3576  fco 3631  funssxp 3633  fssres2 3639  f1o2 3688  f1orescnv 3699  fnbrfvb 3748  fvelimab 3760  ssimaex 3763  dmfco 3768  fvco 3769  fvopab3ig 3773  fvimacnv 3800  fvimacnvALT 3804  dff2 3812  fopabco 3827  fopabcos 3828  fconst5 3843  iunexg 3857  f1ocnvfv1 3873  f1ocnvfv2 3874  isotr 3892  isotrALT 3893  isoini 3895  f1oiso 3899  tfrlem11 3916  tfr3 3921  rdglim2 3944  eloprabg 4002  oprssoprval 4029  f2ndres 4087  curry1 4091  oe0lem 4145  oe0 4154  oev2 4155  oasuc 4156  omsuc 4158  oesuc 4159  oalim 4160  omlim 4161  oecl 4165  oawordri 4177  oaord1 4178  oaword2 4180  oawordeulem 4181  oaordex 4185  oa00 4186  oalimcl 4187  oaass 4188  oarec 4189  omord 4192  omwordi 4195  omwordri 4196  omword1 4197  om00 4199  omlimcl 4202  odi 4203  oewordi 4211  oewordri 4212  oelim2 4215  nnarcl 4225  oaabs 4245  nneob 4248  omsmo 4250  ecoprass 4313  ecoprdi 4314  elmapg 4326  elpm 4329  fundmen 4418  pw2en 4435  sbthlem8 4443  sdomdomtr 4458  ensdomtr 4460  domsdomtr 4465  enen2 4467  domen1 4468  domen2 4469  fodomr 4472  mapenlem2 4479  mapxpen 4484  xpmapenlem5 4489  phplem2 4498  phplem4 4500  php2 4503  php3 4504  onomeneq 4507  onfin 4508  pssnn 4522  ssfi 4524  isfinite2 4532  unfilem1 4533  fodomfi 4549  iunfi 4552  pwfi 4554  suppr 4573  zfregfr 4584  inf3lem6 4601  dfom3 4613  r1ord3 4640  r1val1 4641  tz9.12lem1 4642  rankr1 4657  ranklim 4668  r1pwcl 4670  rankxplim 4695  rankxplim3 4697  rankxpsuc 4698  aceq3 4716  ac6lem 4737  kmlem9 4756  zorn2lem3 4773  zorn2lem4 4774  zorn2lem6 4776  zorn2lem7 4777  fodom 4781  fodomb 4783  brdom7disj 4787  brdom6disj 4788  unidom 4791  carden 4814  carddom 4819  sucdom 4825  unxpdomlem 4826  cardlim 4834  cardiun 4842  alephcard 4850  alephnbtwn 4851  alephnbtwn2 4852  alephord 4858  alephsucdom 4863  cardaleph 4868  alephsson 4877  alephfp 4883  alephval2 4885  cflim 4892  cfeq0 4897  axextnd 4926  axrepndlem1 4927  axrepndlem2 4928  axunnd 4931  axpowndlem2 4933  axpowndlem3 4934  axpowndlem4 4935  axpownd 4936  axregndlem2 4938  axregnd 4939  axinfndlem1 4940  axinfnd 4941  axacndlem4 4945  axacndlem5 4946  axacnd 4947  addasspi 5006  mulasspi 5008  distrpi 5009  addnidpi 5011  ltapi 5013  ltmpi 5014  ltaddpq 5062  ltexpq2 5064  halfpq 5065  ltbtwnpq 5067  prub 5081  genpnmax 5093  mulclprlem 5104  distrlem1pr 5110  distrlem2pr 5111  1idpr 5116  psslinpr 5118  prlem934b 5121  prlem934 5122  ltaddpr 5123  ltexprlem6 5130  ltexpri 5132  ltapr 5134  prlem936 5138  reclem3pr 5141  reclem4pr 5142  suplem2pr 5145  mulgt0sr 5197  suppsr3 5207  axcnre 5269  cnegextlem1 5328  cnegextlem3 5330  cnegext 5331  0cnALT 5333  subnegt 5377  subeq0t 5386  muladd11t 5405  negsubdit 5440  submul2t 5443  nncant 5452  addsub4t 5456  ltxrt 5478  ltxrltt 5483  letrt 5508  xrltnsymt 5533  xrlttrit 5535  xrlttrt 5536  xrletrt 5547  xrret 5552  xrre2t 5553  ltleaddt 5629  ltaddpost 5634  lenegcon2t 5642  subge0t 5657  recextlem1 5665  recext 5667  divdivdivt 5751  conjmult 5763  letrp1t 5782  lt2msq 5839  lerec2t 5847  lediv12it 5854  ledivp1t 5863  xrmax2 5868  xrmin1 5869  xrmin2 5870  peano2nn 5893  nn2get 5900  nnleltp1t 5911  nnaddm1clt 5915  halfaddsubt 5998  avglet 6001  sup2 6008  infm3 6011  infmsup 6025  xrsupsslem 6033  xrinfmsslem 6034  xrsupss 6035  xrinfmss 6036  xrub 6037  supxrre 6040  nn0addclt 6077  nn0ltp1let 6084  nn0ltlem1t 6086  elnnz1 6112  znegclt 6120  zltp1let 6138  zltlem1t 6141  gtndivt 6150  primet 6152  zeot 6156  zneo 6157  zneoOLD 6158  peano2uz2 6159  uzind 6163  uzindOLD 6166  uzwo4OLD 6168  flget 6190  ceilet 6205  qaddclt 6219  qmulclt 6221  qbtwnxr 6229  om2uzlt 6248  seq1rn2 6271  ser1recl 6281  ser1add 6289  shftval3t 6298  shftf 6301  2shft 6302  shftcan2t 6303  elioo3g 6330  elioc2t 6335  elico2t 6336  elicc2t 6337  ioossre 6341  uztrn 6373  eluzp1lt 6379  peano2uzr 6393  uzaddclt 6394  uzind4i 6399  uzwo 6400  uzwoOLD 6401  elfz2t 6417  eluzfzt 6422  elfzle3 6430  fznt 6438  fznn0sub2t 6444  fzaddelt 6445  fzsubelt 6446  fzoptht 6447  fzss2t 6449  fzelp1t 6453  elfzp1 6455  fzrevt 6456  fzrev2t 6457  fzrev2it 6458  fzrev3t 6459  fzneuzt 6463  fsequb 6468  fseqsupcl 6470  fseqsupub 6471  seqzeq 6500  seqzrn2 6501  expnnvalt 6517  expp1t 6519  expm1t 6528  expge0t 6536  expge1t 6538  mulexpt 6539  expaddt 6541  expword2it 6550  expmwordit 6551  exple1t 6552  sqlecant 6586  subsqt 6587  subsq2t 6588  bernneq 6597  expnbndt 6599  expnlbndt 6600  sqr11 6648  sqrmsq2 6651  sqr2irr 6674  crutOLD 6684  rimul 6690  replimt 6707  resubt 6756  imsubt 6759  cjsubt 6766  sqabsaddt 6798  sqabssubt 6799  absexpt 6818  seq1bnd 6862  seq1ublem 6863  cau3ir 6867  cvganz 6876  caubnd 6878  facnn2t 6891  facclt 6892  facdivt 6894  facwordit 6896  faclbnd 6897  faclbnd3 6899  faclbnd4lem1 6900  faclbnd4lem3 6902  faclbnd4lem4 6903  faclbnd6 6906  facavgt 6907  bcval3t 6913  bcval4t 6914  bccl2t 6924  permnnt 6926  sumex 6934  sumeq2 6938  serzfsum 6957  fsum1 6958  fsum1s 6962  fsump1s 6966  fsumsplit 6973  csbfsum 6980  fsumcom 6981  fsumrev 6982  fsumconst 6991  fsumcmpndx2 6995  serzsplit 7009  binomlem1 7019  binomlem2 7020  binomlem4 7022  binomlem5 7023  binom1p 7026  bcxmas 7029  2climnn 7055  2climnn0 7056  climshft 7057  climshft2 7059  iserzshft2 7060  climrecl 7063  climge0 7065  climaddlem3 7069  climmullem1 7073  climmullem3 7075  climmullem4 7076  climmullem5 7077  climmullem8 7080  climsub 7083  iserzmulc1 7089  climcmplem 7090  climsqueeze 7093  climsqueeze2 7094  clim2serz 7098  climsup 7108  climcau 7109  caucvglem5 7114  caucvglem6 7115  caucvg 7116  ser1cmp2lem 7129  ser1cmp2 7130  isumnul 7155  isumreclt 7162  reccnv 7170  infcvglem3 7175  expcnvlem6 7184  geoisum1c 7197  cvgratlem1ALT 7199  cvgratlem1 7202  cvgratlem4 7205  cvgratlem5 7206  fsum0diaglem1 7208  fsum0diaglem2 7209  fsum0diag2 7211  fsum0diag4 7213  elcncf 7217  cncffvrn 7225  mulc1cncf 7231  ivthlem6 7238  ivthlem7 7239  ivthlem6OLD 7247  ivthlem7OLD 7248  eftclt 7262  efseq0ex 7270  efaddlem2 7298  efaddlem5 7301  efaddlem9 7305  efaddlem14 7310  efne0t 7328  efsubt 7330  efexpt 7331  reeftclt 7333  eftlclt 7338  reeftlclt 7339  abspef01tlub 7353  reeff1o 7385  sinsubt 7414  cossubt 7415  demoivre 7443  acdc3lem 7445  acdc2lem1 7447  acdc2lem2 7448  acdc5lem1 7450  acdc5lem2 7451  acdclem 7453  acdcALT 7455  nn0ennn 7456  xpnnen 7458  znnenlem 7460  znnenlemOLD 7461  znnen 7462  infpnlem1 7466  ruclem24 7493  ruclem27 7496  ruclem28 7497  infxpidmlem4 7515  infxpidmlem5 7516  infxpidmlem7 7518  infxpidmlem8 7519  infxpidmlem9 7520  infunabs 7525  infcdaabs 7526  infdif 7528  infdif2 7529  infmap2lem2 7540  alephadd 7542  iunopnt 7559  eltopss 7563  istps2 7567  eltgt 7578  eltg2t 7579  tg2t 7581  tgclt 7584  eltg3t 7586  tgss2t 7597  basgen2t 7599  sn0top 7607  iscld 7629  ntrval2 7646  ntrss 7648  elcls 7664  neiss2 7676  neiint 7679  isneip 7680  neips 7687  islp2 7707  clslp 7708  cnpco 7729  iscncl 7730  cnsscnp 7732  sncld 7747  metreslem 7784  metxp 7796  blval 7799  bl2in 7805  opni 7826  opni3 7828  blssopn 7829  blnei 7841  metcnplem 7848  metcnpi 7852  metcnpi2 7853  metcnpi3 7854  metcnpi4 7855  metcni2 7857  metcnss 7860  metcnss2 7861  metdnsconst 7863  cncfmet 7867  ioo2bl 7874  tgioolem 7876  tgioo 7877  lmconst 7896  lmnn 7897  iscau3 7900  iscau4 7902  iscau5 7903  iscaunns 7906  caun0 7907  lmuni 7913  lmss 7915  lmfexlem2 7919  lmle 7922  metelcls 7927  xplmi 7935  xplm 7937  xpcn 7938  opr1cn 7940  bopcnlem2 7944  bopcnlem3 7945  fsumcnlem 7951  iscms2lem4 7954  lmcau 7958  cncms 7960  bcthlem2 7962  bcthlem7 7967  bcthlem9 7969  bcthlem14 7974  bcthlem16 7976  bcthlem18 7978  bcthlem20 7980  bcthlem21 7981  bcthlem26 7986  bcthlem28 7988  bcthlem31 7991  bcthlem33 7993  grpidinvlem2 8011  grpidinv 8014  grpideu 8015  grprcan 8025  grpinveu 8026  grpinvid1 8034  grpinvid2 8035  grplcan 8037  isgrp2i 8038  grpdivdiv 8049  grpmuldivass 8050  grppnpcan2 8054  grpnpncan 8056  abl4 8068  ablmuldiv 8071  abldivdiv4 8073  ablnnncan 8075  ablnnncan1 8077  subgopr 8082  subgabl 8087  vcdi 8135  vcdir 8136  vcass 8137  vcsubdir 8139  vcz 8153  nvex 8194  nvscom 8214  nvmdi 8234  nvsubadd 8239  cnnvm 8277  imsmetlem 8287  sqcn 8298  va1cnlem 8307  ipfval 8314  ipcl 8327  ip1cnilem6 8340  sspval 8344  sspmlem 8353  lnocoi 8380  nmoub3i 8396  0oo 8409  0lno 8410  nmlno0lem 8413  blocnilem 8423  cnph 8437  ipasslem1 8449  ipasslem2 8450  ipasslem4 8452  ipasslem5 8453  ipasslem11 8459  ipdi 8462  ipassr 8465  ipassr2 8466  ipsubdi 8468  ipblnfi 8475  ubthlem3 8490  ubthlem8 8495  ubthlem9 8496  ubthlem10 8497  minveclem17 8520  minveclem20 8523  minveclem22 8525  minveclem24 8527  minveclem25 8528  minveclem27 8530  minveclem30 8533  minveclem31 8534  htthlem5 8582  pstr 8609  pilem2 8626  efif1lem5 8684  shftefif1olem 8696  eff1i 8699  axgroth3 8734  grothinf 8736  hvmul0ort 8849  hvaddsubvalt 8857  hvsub4t 8861  hvpncant 8863  hvmulcant 8894  hvmulcan2t 8895  hvaddsub4t 8900  normpyct 8968  hlimcaui 9061  helch 9071  hhssnv 9089  occont 9115  ocorth 9119  occllem6 9133  occl 9136  projlem2 9142  projlem8 9148  projlem26 9166  pjtheu 9190  pjeq2t 9196  shscl 9236  shsel1t 9240  hsupss 9264  spanss 9273  orthin 9325  chsscon2t 9380  chpsscon2t 9383  chdmm3t 9405  chdmm4t 9406  chdmj3t 9409  chdmj4t 9410  h1de2b 9432  h1de2bOLD 9433  spansnss2t 9455  spanunsn 9459  h1datom 9461  osumlem7 9541  nonbool 9553  5oalem1 9556  5oalem2 9557  5oalem3 9558  5oalem5 9560  pjot 9573  pjsumt 9612  pjoi0t 9619  pjnorm2t 9629  hosubnegt 9690  honegsubdit 9693  hosub4t 9696  unopf1ot 9797  unopnormt 9798  nmlnop0ALT 9876  lnopm 9881  lnophs 9882  lnopco 9884  lnopeq0 9888  nmopunt 9895  nmcopexlem3 9909  nmcopexlem6 9912  nmcoplb 9914  nmophm 9917  lnopcon 9919  lnfnsub 9931  nmbdfnlb 9934  nmcfnexlem3 9938  nmcfnexlem6 9941  nmcfnlb 9943  lnfncon 9946  nlelsh 9949  nlelch 9950  riesz3 9951  riesz4 9952  riesz1t 9954  cnlnadjlem2 9957  cnlnadjlem6 9961  adjbdlnb 9973  nmopco 9984  adjco 9989  rnbra 9996  bra11 9997  cnvbravalt 9999  cnvbramult 10004  kbass4t 10008  kbass5t 10009  leoprf2t 10016  leoprft 10017  leopmulit 10022  leopnmidt 10027  pjbdln 10032  hmopidmch 10035  hmopidmpj 10036  pjadjco 10045  pjss1co 10047  pjss2co 10048  pjorthco 10053  pjscj 10054  pjssdif2 10058  pjhmopidm 10066  pjinvar 10075  pjclem4a 10082  pjclem4 10083  pjadj2co 10088  pj3s 10091  pj3cor1 10093  hstoct 10105  hstnmoct 10106  hstoht 10115  stcltr1 10157  cvcon3t 10167  cvnbtwnt 10169  mdbr3 10180  mdbr4 10181  dmdmdt 10183  dmdbr3 10188  dmdbr4 10189  dmdbr5 10191  mdsl0 10193  ssmd2 10195  mdslmd1lem2 10209  mdslmd2 10213  mdslmd3 10215  mdslmd4 10216  atcveq0 10231  superpos 10237  chjatom 10240  chrelat 10247  cvbr3 10250  atcv0eq 10262  atoml 10265  atcvatlem 10268  irredlem3 10275  atcvat3 10279  atcvat4 10280  atmd 10282  mdsymlem3 10288  mdsymlem4 10289  mdsymlem5 10290  sumdmdi 10298  sumdmdlem 10301  sumdmdlem2 10302  dmdbr6at 10306  cdjreu 10315  cdj1 10316  cdj3lem1 10317  cdj3lem2b 10320  cdj3 10324  nndivlub 10380  uninqs 10400  elo 10403  infi1 10405  fine 10406  sppfi 10435  cdrci 10440  oisbmj 10444  truni1 10445  cnrsfin 10455  cnrscoa 10456  mapdiscn 10457  cnvhmph 10473  hmphsyma 10474  hmphre 10476  hmphtr 10477  hmpher 10482  hmeogrp 10484  homcard 10485  qusp 10489  oefil2 10500  fgsb 10503  fgsb2 10508  cnfilca 10510  rcfpfillem3 10513  rcfpfillem4 10514  rcfpfil 10517  mslb1 10545  iintlem1 10548  iint 10550  1ded 10587  1cat 10608  cmpassoh 10645  homgrf 10646  ismonb 10652  ismonb1 10653  ismonb2 10654  imonclem 10655  ismonc 10656  cmpmon 10657  icmpmon 10659  idmon 10660  idfisf 10670

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7

This theorem depends on definitions:  df-bi 147  df-an 225

Copyright terms: Public domain