Theorem adantl 388

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

Hypothesis

Ref	Expression
adantl.1	|- (ph -> ps)

Assertion

Ref	Expression
adantl	|- ((ch /\ ph) -> ps)

Proof of Theorem adantl

Step	Hyp	Ref	Expression
1		adantl.1	. . 3 |- (ph -> ps)
2	1	a1i 8	. 2 |- (ch -> (ph -> ps))
3	2	imp 350	1 |- ((ch /\ ph) -> ps)

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 540  im2anan9 563  im2anan9r 564  bi2bian9 634  pm5.18 660  pm5.75 749  ccase2 757  prlem1 770  3ad2ant3 802  ax11v2 1215  ax11b 1220  sbcom 1258  sbal1 1346  ax11eq 1363  ax11el 1364  ax11inda 1371  euim 1421  euor2 1437  2exeu 1446  2eu5 1453  eqeqan12d 1490  sylan9eq 1527  vtoclegft 1856  eqvinc 1883  reu3 1931  sbcthdv 1947  sbccomglem 1988  sbccomg 1989  sbcralt 1990  csbcomg 2017  hbcsb1gd 2027  hbcsbgd 2028  sylan9ss 2075  elin 2207  sspr 2475  unissel 2527  intab 2560  copsex4g 2794  solin 2857  reuuni1 2882  alxfr 2896  ralxfrALT 2900  wefrc 2943  ordelon 2971  tz7.7 2973  ordunidif 3005  onint0 3007  onnmin 3015  onmindif 3060  onmindif2 3061  ordelsuc 3071  ordsucelsuc 3073  ordtri2or2 3078  ordsucun 3082  onsucuni2 3091  nlimsucg 3112  ordunisuc2 3115  limuni3 3123  tfi 3126  peano5 3153  findsg 3157  tfinds 3161  tfindsg 3162  ssnlim 3167  brinxp 3232  ideqg 3276  relssres 3392  relimasn 3425  soirri 3442  ssxpr 3475  xpexr2 3480  unixp0 3518  funssres 3552  funun 3554  fununi 3563  resfunexg 3579  cofunexg 3580  fco 3636  funssxp 3638  fssres2 3644  f1o2 3693  f1orescnv 3704  fnbrfvb 3753  fvelimab 3765  ssimaex 3768  dmfco 3773  fvco 3774  fvopab3ig 3778  fvimacnv 3805  fvimacnvALT 3809  dff2 3817  fopabco 3832  fopabcos 3833  fconst5 3848  iunexg 3862  f1ocnvfv1 3878  f1ocnvfv2 3879  isotr 3897  isotrALT 3898  isoini 3900  f1oiso 3904  tfrlem11 3921  tfr3 3926  rdglim2 3949  eloprabg 4007  oprssoprval 4034  f2ndres 4094  curry1 4098  oe0lem 4152  oe0 4161  oev2 4162  oasuc 4163  omsuc 4165  oesuc 4166  oalim 4167  omlim 4168  oecl 4172  oawordri 4184  oaord1 4185  oaword2 4187  oawordeulem 4188  oaordex 4192  oa00 4193  oalimcl 4194  oaass 4195  oarec 4196  omord 4199  omwordi 4202  omwordri 4203  omword1 4204  om00 4206  omlimcl 4209  odi 4210  oewordi 4218  oewordri 4219  oelim2 4222  nnarcl 4232  oaabs 4252  nneob 4255  omsmo 4257  ecoprass 4320  ecoprdi 4321  elmapg 4333  elpm 4336  fundmen 4428  pw2en 4446  sbthlem8 4454  sdomdomtr 4469  ensdomtr 4471  domsdomtr 4476  enen2 4478  domen1 4479  domen2 4480  fodomr 4483  mapenlem2 4490  mapxpen 4495  xpmapenlem5 4500  phplem2 4509  phplem4 4511  php2 4514  php3 4515  php3OLD 4516  onomeneq 4519  onfinOLD 4520  pssnn 4534  ssfi 4537  ssfiOLD 4538  isfinite2OLD 4546  unfilem1 4548  fodomfiOLD 4566  iunfiOLD 4569  pwfiOLD 4571  suppr 4590  zfregfr 4601  inf3lem6 4618  dfom3 4630  r1ord3 4657  r1val1 4658  tz9.12lem1 4659  rankr1 4674  ranklim 4685  r1pwcl 4687  rankxplim 4712  rankxplim3 4714  rankxpsuc 4715  aceq3 4733  ac6lem 4754  kmlem9 4773  zorn2lem3 4790  zorn2lem4 4791  zorn2lem6 4793  zorn2lem7 4794  fodom 4798  fodomb 4800  brdom7disj 4804  brdom6disj 4805  unidom 4808  carden 4831  carddom 4836  sucdom 4842  unxpdomlem 4843  cardlim 4851  cardiun 4859  alephcard 4867  alephnbtwn 4868  alephnbtwn2 4869  alephord 4875  alephsucdom 4880  cardaleph 4885  alephsson 4894  alephfp 4900  alephval2 4902  cflim 4909  cfeq0 4914  axextnd 4943  axrepndlem1 4944  axrepndlem2 4945  axunnd 4948  axpowndlem2 4950  axpowndlem3 4951  axpowndlem4 4952  axpownd 4953  axregndlem2 4955  axregnd 4956  axinfndlem1 4957  axinfnd 4958  axacndlem4 4962  axacndlem5 4963  axacnd 4964  addasspi 5023  mulasspi 5025  distrpi 5026  addnidpi 5028  ltapi 5030  ltmpi 5031  ltaddpq 5079  ltexpq2 5081  halfpq 5082  ltbtwnpq 5084  prub 5098  genpnmax 5110  mulclprlem 5121  distrlem1pr 5127  distrlem2pr 5128  1idpr 5133  psslinpr 5135  prlem934b 5138  prlem934 5139  ltaddpr 5140  ltexprlem6 5147  ltexpri 5149  ltapr 5151  prlem936 5155  reclem3pr 5158  reclem4pr 5159  suplem2pr 5162  mulgt0sr 5214  suppsr3 5224  axcnre 5286  cnegextlem1 5345  cnegextlem3 5347  cnegext 5348  0cnALT 5350  subnegt 5394  subeq0t 5403  muladd11t 5422  negsubdit 5457  submul2t 5460  nncant 5469  addsub4t 5473  ltxrt 5495  ltxrltt 5500  letrt 5525  xrltnsymt 5550  xrlttrit 5552  xrlttrt 5553  xrletrt 5564  xrret 5569  xrre2t 5570  ltleaddt 5645  ltaddpost 5651  lenegcon2t 5659  subge0t 5674  recextlem1 5682  recext 5684  divdivdivt 5785  conjmult 5797  letrp1t 5816  ltdivmult 5867  lt2msq 5881  lerec2t 5889  lediv12it 5896  ledivp1t 5905  xrmax2 5910  xrmin1 5911  xrmin2 5912  peano2nn 5935  nn2get 5942  nnleltp1t 5954  nnaddm1clt 5958  halfaddsubt 6041  avglet 6044  sup2 6051  infm3 6054  infmsup 6068  xrsupsslem 6076  xrinfmsslem 6077  xrsupss 6078  xrinfmss 6079  xrub 6080  supxrre 6083  nn0addclt 6120  nn0ltp1let 6127  nn0ltlem1t 6129  elnnz1 6155  znegclt 6163  zltp1let 6181  zltlem1t 6184  gtndivt 6193  primet 6195  zeot 6199  zneo 6200  peano2uz2 6201  uzind 6205  uzindOLD 6208  uzwo4OLD 6210  flget 6233  ceilet 6250  quoremz 6251  quoremOLD 6252  intfracqOLD 6255  qaddclt 6269  qmulclt 6271  qbtwnxr 6279  om2uzlt 6298  seq1rn2 6321  ser1recl 6331  ser1add 6339  shftval3t 6348  shftf 6351  2shft 6352  shftcan2t 6353  elioo3g 6380  elioc2t 6390  elico2t 6391  elicc2t 6392  ioojoint 6416  uztrn 6428  eluzp1lt 6434  peano2uzr 6448  uzaddclt 6449  uzind4i 6454  uzwo 6455  uzwoOLD 6456  elfz2t 6472  eluzfzt 6477  elfzle3 6485  fznt 6493  fznn0sub2t 6499  fzaddelt 6500  fzsubelt 6501  fzoptht 6502  fzss2t 6504  fzelp1t 6508  elfzp1 6510  fzrevt 6511  fzrev2t 6512  fzrev2it 6513  fzrev3t 6514  fzneuzt 6518  fsequb 6523  fseqsupcl 6525  fseqsupub 6526  seqzeq 6555  seqzrn2 6556  expnnvalt 6572  expp1t 6574  expm1t 6583  expge0t 6591  expge1t 6593  mulexpt 6594  expaddt 6596  expword2it 6605  expmwordit 6606  exple1t 6607  sqlecant 6641  subsqt 6642  subsq2t 6643  bernneq 6652  expnbndt 6654  expnlbndt 6655  sqr11 6703  sqrmsq2 6706  sqr2irr 6729  rimul 6744  replimt 6761  rerebt 6776  mulretOLD 6777  resubt 6806  imsubt 6809  cjsubt 6816  sqabsaddt 6848  sqabssubt 6849  absexpt 6868  absmaxt 6897  seq1bnd 6910  seq1ublem 6911  cau3ir 6915  cvganz 6924  caubnd 6926  facnn2t 6939  facclt 6940  facdivt 6942  facwordit 6944  faclbnd 6945  faclbnd3 6947  faclbnd4lem1 6948  faclbnd4lem3 6950  faclbnd4lem4 6951  faclbnd6 6954  facavgt 6955  bcval3t 6960  bcval4t 6961  bccl2t 6971  permnnt 6973  sumex 6981  sumeq2 6985  serzfsum 7004  fsum1 7005  fsum1s 7009  fsump1s 7013  fsumsplit 7020  csbfsum 7027  fsumcom 7028  fsumrev 7029  fsumconst 7038  fsumcmpndx2 7042  serzsplit 7056  binomlem1 7066  binomlem2 7067  binomlem4 7069  binomlem5 7070  binom1p 7073  bcxmas 7076  2climnn 7102  2climnn0 7103  climshft 7104  climshft2 7106  iserzshft2 7107  climrecl 7110  climge0 7112  climaddlem3 7116  climmullem1 7120  climmullem3 7122  climmullem4 7123  climmullem5 7124  climmullem8 7127  climsub 7130  iserzmulc1 7136  climcmplem 7137  climsqueeze 7140  climsqueeze2 7141  clim2serz 7145  climsup 7155  climcau 7156  caucvglem5 7161  caucvglem6 7162  caucvg 7163  ser1cmp2lem 7176  ser1cmp2 7177  isumnul 7203  isumreclt 7210  reccnv 7218  infcvglem3 7223  expcnvlem6 7232  geoisum1c 7245  cvgratlem1ALT 7247  cvgratlem1 7250  cvgratlem4 7253  cvgratlem5 7254  fsum0diaglem1 7256  fsum0diaglem2 7257  fsum0diag2 7259  fsum0diag4 7261  elcncf 7265  cncffvrn 7273  mulc1cncf 7279  ivthlem6 7286  ivthlem7 7287  eftclt 7303  efseq0ex 7311  efaddlem2 7339  efaddlem5 7342  efaddlem9 7346  efaddlem14 7351  efne0t 7369  efsubt 7371  efexpt 7372  reeftclt 7374  eftlclt 7379  reeftlclt 7380  abspef01tlub 7395  reeff1o 7426  sinsubt 7455  cossubt 7456  demoivre 7484  acdc3lem 7486  acdc2lem1 7488  acdc2lem2 7489  acdc5lem1 7491  acdc5lem2 7492  acdclem 7494  acdcALT 7496  nn0ennn 7497  xpnnen 7499  znnenlem 7501  znnen 7502  infpnlem1 7506  ruclem24 7533  ruclem27 7536  ruclem28 7537  infxpidmlem4 7555  infxpidmlem5 7556  infxpidmlem7 7558  infxpidmlem8 7559  infxpidmlem9 7560  infunabs 7565  infcdaabs 7566  infdif 7568  infdif2 7569  infmap2lem2 7580  alephadd 7582  iunopnt 7599  eltopss 7603  istps2 7607  eltgt 7618  eltg2t 7619  tg2t 7621  tgclt 7624  eltg3t 7626  tgss2t 7637  basgen2t 7639  sn0top 7647  iscld 7669  ntrval2 7686  ntrss 7688  elcls 7704  neiss2 7716  neiint 7719  isneip 7720  neips 7727  islp2 7747  clslp 7748  cnpco 7769  iscncl 7770  cnsscnp 7772  sncld 7787  metreslem 7822  metxp 7834  blval 7837  bl2in 7843  opni 7864  opni3 7866  blssopn 7867  blnei 7879  metcnplem 7886  metcnpi 7890  metcnpi2 7891  metcnpi3 7892  metcnpi4 7893  metcni2 7895  metcnss 7898  metcnss2 7899  metdnsconst 7901  cncfmet 7905  ioo2bl 7912  tgioolem 7914  tgioo 7915  lmconst 7934  lmnn 7935  iscau3 7938  iscau4 7940  iscau5 7941  iscaunns 7944  caun0 7945  lmuni 7951  lmss 7953  lmfexlem2 7957  lmle 7960  metelcls 7965  xplmi 7973  xplm 7975  xpcn 7976  opr1cn 7978  bopcnlem2 7982  bopcnlem3 7983  fsumcnlem 7989  iscms2lem4 7992  lmcau 7996  cncms 7998  bcthlem2 8000  bcthlem7 8005  bcthlem9 8007  bcthlem14 8012  bcthlem16 8014  bcthlem18 8016  bcthlem20 8018  bcthlem21 8019  bcthlem26 8024  bcthlem28 8026  bcthlem31 8029  bcthlem33 8031  grpidinvlem2 8049  grpidinv 8052  grpideu 8053  grprcan 8063  grpinveu 8064  grpinvid1 8072  grpinvid2 8073  grplcan 8075  isgrp2i 8076  grpdivdiv 8087  grpmuldivass 8088  grppnpcan2 8092  grpnpncan 8094  abl4 8105  ablmuldiv 8107  abldivdiv4 8109  ablnnncan 8111  ablnnncan1 8113  subgopr 8118  subgabl 8123  vcdi 8171  vcdir 8172  vcass 8173  vcsubdir 8175  vcz 8189  nvex 8230  nvscom 8250  nvmdi 8270  nvsubadd 8275  cnnvm 8313  imsmetlem 8323  sqcn 8335  va1cnlem 8345  ipfval 8352  ipcl 8365  ip1cnilem6 8378  sspval 8382  sspmlem 8391  lnocoi 8418  nmoub3i 8436  0oo 8449  0lno 8450  nmlno0lem 8453  blocnilem 8464  cnph 8478  ipasslem1 8490  ipasslem2 8491  ipasslem4 8493  ipasslem5 8494  ipasslem11 8500  ipdi 8503  ipassr 8506  ipassr2 8507  ipsubdi 8509  ipblnfi 8516  ubthlem3 8531  ubthlem8 8536  ubthlem9 8537  ubthlem10 8538  minveclem17 8561  minveclem20 8564  minveclem22 8566  minveclem24 8568  minveclem25 8569  minveclem27 8571  minveclem30 8574  minveclem31 8575  htthlem5 8624  pstr 8652  spwpr3OLD 8662  pilem2 8672  abssinper 8712  efif1lem5 8734  shftefif1olem 8741  eff1i 8744  axgroth3 8779  grothinf 8781  hvmul0ort 8894  hvaddsubvalt 8902  hvsub4t 8906  hvpncant 8908  hvmulcant 8939  hvmulcan2t 8940  hvaddsub4t 8945  normpyct 9013  hlimcaui 9106  helch 9116  hhssnv 9134  occont 9160  ocorth 9164  occllem6 9178  occl 9181  projlem2 9187  projlem8 9193  projlem26 9211  pjtheu 9235  pjeq2t 9241  shscl 9281  shsel1t 9285  hsupss 9309  spanss 9318  orthin 9370  chsscon2t 9425  chpsscon2t 9428  chdmm3t 9450  chdmm4t 9451  chdmj3t 9454  chdmj4t 9455  h1de2b 9477  spansnss2t 9498  spanunsn 9502  h1datom 9504  osumlem7 9584  nonbool 9596  5oalem1 9599  5oalem2 9600  5oalem3 9601  5oalem5 9603  pjot 9616  pjsumt 9655  pjoi0t 9662  pjnorm2t 9672  hosubnegt 9733  honegsubdit 9736  hosub4t 9739  unopf1ot 9840  unopnormt 9841  nmlnop0ALT 9920  lnopm 9925  lnophs 9926  lnopco 9928  lnopeq0 9932  nmopunt 9939  nmcopexlem3 9953  nmcopexlem6 9956  nmcoplb 9958  nmophm 9961  lnopcon 9963  lnfnsub 9975  nmbdfnlb 9978  nmcfnexlem3 9982  nmcfnexlem6 9985  nmcfnlb 9987  lnfncon 9990  nlelsh 9993  nlelch 9994  riesz3 9995  riesz4 9996  riesz1t 9998  cnlnadjlem2 10001  cnlnadjlem6 10005  adjbdlnb 10017  nmopco 10028  adjco 10033  rnbra 10040  bra11 10041  cnvbravalt 10043  cnvbramult 10048  kbass4t 10052  kbass5t 10053  leoprf2t 10060  leoprft 10061  leopmulit 10066  leopnmidt 10071  pjbdln 10076  hmopidmch 10079  hmopidmpj 10080  pjadjco 10089  pjss1co 10091  pjss2co 10092  pjorthco 10097  pjscj 10098  pjssdif2 10102  pjhmopidm 10110  pjinvar 10119  pjclem4a 10126  pjclem4 10127  pjadj2co 10132  pj3s 10135  pj3cor1 10137  hstoct 10149  hstnmoct 10150  hstoht 10159  stcltr1 10201  cvcon3t 10211  cvnbtwnt 10213  mdbr3 10224  mdbr4 10225  dmdmdt 10227  dmdbr3 10232  dmdbr4 10233  dmdbr5 10235  mdsl0 10237  ssmd2 10239  mdslmd1lem2 10253  mdslmd2 10257  mdslmd3 10259  mdslmd4 10260  atcveq0 10275  superpos 10281  chjatom 10284  chrelat 10291  cvbr3 10294  atcv0eq 10306  atoml 10309  atcvatlem 10312  irredlem3 10319  atcvat3 10323  atcvat4 10324  atmd 10326  mdsymlem3 10332  mdsymlem4 10333  mdsymlem5 10334  sumdmdi 10342  sumdmdlem 10345  sumdmdlem2 10346  dmdbr6at 10350  cdjreu 10359  cdj1 10360  cdj3lem1 10361  cdj3lem2b 10364  cdj3 10368  nndivlub 10422  uninqs 10441  elo 10444  infi1 10447  infi1OLD 10448  fine 10449  fineOLD 10450  sppfi 10486  sppfiOLD 10487  cdrci 10494  oisbmj 10498  truni1 10499  cnrsfin 10509  cnrscoa 10510  mapdiscn 10511  cnvhmph 10527  hmphsyma 10528  hmphre 10530  hmphtr 10531  hmpher 10536  hmeogrp 10538  homcard 10539  homcardus 10540  hmeobc 10542  unpde2eg2 10544  setwoe 10546  top2usne 10549  qusp 10555  oefil2 10567  fgsb 10570  fgsbOLD 10571  fgsb2 10580  cnfilca 10583  cnfilcaOLD 10584  rcfpfillem3 10589  rcfpfillem3OLD 10590  rcfpfillem4 10591  rcfpfillem4OLD 10592  rcfpfil 10597  rcfpfilOLD 10598  sfvlim 10605  mslb1 10629  iintlem1 10632  iint 10634  1ded 10671  1cat 10692  cmpassoh 10729  homgrf 10730  ismonb 10738  ismonb1 10739  ismonb2 10740  imonclem 10741  ismonc 10742  cmpmon 10743  icmpmon 10744  idmon 10745  isepib 10748  isepib1 10749  isepib2 10750  idfisf 10760

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