Theorem adantl 390

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 394  ad2antlr 407  ad2antrl 408  ad2antll 409  jaao 429  sylan9 470  mpan9 472  sylan9bb 542  im2anan9 565  im2anan9r 566  bi2bian9 636  pm5.18 662  pm5.75 751  ccase2 759  prlem1 772  3ad2ant3 804  ax11v2 1217  ax11b 1222  sbcom 1260  sbal1 1348  ax11eq 1365  ax11el 1366  ax11inda 1373  euim 1423  euor2 1440  2exeu 1449  2eu5 1456  eqeqan12d 1493  sylan9eq 1530  vtoclegft 1859  eqvinc 1886  reu3 1934  sbcthdv 1950  sbccomglem 1991  sbccomg 1992  sbcralt 1993  csbcomg 2020  hbcsb1gd 2030  hbcsbgd 2031  sylan9ss 2078  elin 2210  sspr 2479  unissel 2531  intab 2564  copsex4g 2800  solin 2863  reuuni1 2888  alxfr 2902  ralxfrALT 2906  wefrc 2949  ordelon 2977  tz7.7 2979  ordunidif 3011  onint0 3013  onnmin 3021  onmindif 3066  onmindif2 3067  ordelsuc 3077  ordsucelsuc 3079  ordtri2or2 3084  ordsucun 3088  onsucuni2 3097  nlimsucg 3118  ordunisuc2 3121  limuni3 3129  tfi 3132  peano5 3159  findsg 3163  tfinds 3167  tfindsg 3168  ssnlim 3173  brinxp 3238  ideqg 3282  relssres 3398  relimasn 3431  soirri 3448  ssxpr 3481  xpexr2 3486  unixp0 3524  funssres 3558  funun 3560  fununi 3569  resfunexg 3585  cofunexg 3586  fco 3642  funssxp 3644  fssres2 3650  f1o2 3699  f1orescnv 3710  fnbrfvb 3759  fvelimab 3771  ssimaex 3774  dmfco 3779  fvco 3780  fvopab3ig 3784  fvimacnv 3811  fvimacnvALT 3815  dff2 3823  fopabco 3838  fopabcos 3839  fconst5 3854  iunexg 3868  f1ocnvfv1 3884  f1ocnvfv2 3885  isotr 3903  isotrALT 3904  isoini 3906  f1oiso 3910  tfrlem11 3927  tfr3 3932  rdglim2 3955  eloprabg 4013  oprssoprval 4040  f2ndres 4100  curry1 4104  oe0lem 4158  oe0 4167  oev2 4168  oasuc 4169  omsuc 4171  oesuc 4172  oalim 4173  omlim 4174  oecl 4178  oawordri 4190  oaord1 4191  oaword2 4193  oawordeulem 4194  oaordex 4198  oa00 4199  oalimcl 4200  oaass 4201  oarec 4202  omord 4205  omwordi 4208  omwordri 4209  omword1 4210  om00 4212  omlimcl 4215  odi 4216  oewordi 4224  oewordri 4225  oelim2 4228  nnarcl 4238  oaabs 4258  nneob 4261  omsmo 4263  ecoprass 4326  ecoprdi 4327  elmapg 4339  elpm 4342  fundmen 4434  pw2en 4452  sbthlem8 4460  sdomdomtr 4475  ensdomtr 4477  domsdomtr 4482  enen2 4484  domen1 4485  domen2 4486  fodomr 4489  mapenlem2 4496  mapxpen 4501  xpmapenlem5 4506  phplem2 4515  phplem4 4517  php2 4520  php3 4521  php3OLD 4522  onomeneq 4525  pssnn 4544  ssfi 4547  ssfiOLD 4548  isfinite2 4557  isfinite2OLD 4558  unfilem1 4560  fodomfi 4575  fodomfiOLD 4576  pwfiOLD 4580  suppr 4599  zfregfr 4610  inf3lem6 4627  dfom3 4639  r1ord3 4667  r1val1 4668  tz9.12lem1 4669  rankr1 4684  ranklim 4695  r1pwcl 4697  rankxplim 4722  rankxplim3 4724  rankxpsuc 4725  aceq3 4743  ac6lem 4764  kmlem9 4783  zorn2lem3 4800  zorn2lem4 4801  zorn2lem6 4803  zorn2lem7 4804  fodom 4808  fodomb 4810  brdom7disj 4814  brdom6disj 4815  unidom 4818  carden 4841  carddom 4846  sucdom 4852  sucdomOLD 4853  unxpdomlem 4854  cardlim 4862  cardiun 4870  alephcard 4878  alephnbtwn 4879  alephnbtwn2 4880  alephord 4886  alephsucdom 4891  cardaleph 4896  alephsson 4905  alephfp 4911  alephval2 4913  cflim 4921  cfeq0 4926  axextnd 4955  axrepndlem1 4956  axrepndlem2 4957  axunnd 4960  axpowndlem2 4962  axpowndlem3 4963  axpowndlem4 4964  axpownd 4965  axregndlem2 4967  axregnd 4968  axinfndlem1 4969  axinfnd 4970  axacndlem4 4974  axacndlem5 4975  axacnd 4976  addasspi 5035  mulasspi 5037  distrpi 5038  addnidpi 5040  ltapi 5042  ltmpi 5043  ltaddpq 5091  ltexpq2 5093  halfpq 5094  ltbtwnpq 5096  prub 5110  genpnmax 5122  mulclprlem 5133  distrlem1pr 5139  distrlem2pr 5140  1idpr 5145  psslinpr 5147  prlem934b 5150  prlem934 5151  ltaddpr 5152  ltexprlem6 5159  ltexpri 5161  ltapr 5163  prlem936 5167  reclem3pr 5170  reclem4pr 5171  suplem2pr 5174  mulgt0sr 5226  suppsr3 5236  axcnre 5298  cnegextlem1 5357  cnegextlem3 5359  cnegext 5360  0cnALT 5362  subnegt 5406  subeq0t 5415  muladd11t 5434  negsubdit 5469  submul2t 5472  nncant 5481  addsub4t 5485  ltxrt 5507  ltxrltt 5512  letrt 5537  xrltnsymt 5562  xrlttrit 5564  xrlttrt 5565  xrletrt 5576  xrret 5581  xrre2t 5582  ltleaddt 5657  ltaddpost 5663  lenegcon2t 5671  subge0t 5686  recextlem1 5694  recext 5696  divdivdivt 5787  conjmult 5799  letrp1t 5818  ltdivmult 5869  lt2msq 5883  lerec2t 5891  lediv12it 5898  ledivp1t 5907  xrmax2 5912  xrmin1 5913  xrmin2 5914  peano2nn 5937  nn2get 5944  nnleltp1t 5956  nnaddm1clt 5960  halfaddsubt 6043  avglet 6046  sup2 6053  infm3 6056  infmsup 6070  xrsupsslem 6078  xrinfmsslem 6079  xrsupss 6080  xrinfmss 6081  xrub 6082  supxrre 6085  nn0addclt 6122  nn0ltp1let 6129  nn0ltlem1t 6131  elnnz1 6157  znegclt 6165  zltp1let 6183  zltlem1t 6186  gtndivt 6195  primet 6197  zeot 6201  zneo 6202  peano2uz2 6203  uzind 6207  uzindOLD 6210  uzwo4OLD 6212  flget 6235  ceilet 6252  quoremz 6253  intfracq 6255  fldivt 6256  qaddclt 6270  qmulclt 6272  qbtwnxr 6280  om2uzlt 6299  seq1rn2 6322  ser1recl 6332  ser1add 6340  shftval3t 6349  shftf 6352  2shft 6353  shftcan2t 6354  elioo3g 6381  elioc2t 6391  elico2t 6392  elicc2t 6393  ioojoint 6417  uztrn 6429  eluzp1lt 6435  peano2uzr 6449  uzaddclt 6450  uzind4i 6455  uzwo 6456  uzwoOLD 6457  elfz2t 6473  eluzfzt 6478  elfzle3 6486  fznt 6494  fznn0sub2t 6500  fzaddelt 6501  fzsubelt 6502  fzoptht 6503  fzss2t 6505  fzelp1t 6509  elfzp1 6511  fzrevt 6512  fzrev2t 6513  fzrev2it 6514  fzrev3t 6515  fzneuzt 6519  fsequb 6524  fseqsupcl 6526  fseqsupub 6527  seqzeq 6556  seqzrn2 6557  expnnvalt 6573  expp1t 6575  expm1t 6584  expge0t 6592  expge1t 6594  mulexpt 6595  expaddt 6597  expword2it 6606  expmwordit 6607  exple1t 6608  sqlecant 6642  subsqt 6643  subsq2t 6644  bernneq 6653  expnbndt 6655  expnlbndt 6656  sqr11 6704  sqrmsq2 6707  sqr2irr 6730  rimul 6745  replimt 6762  rerebt 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 7485  acdc3lem 7487  acdc2lem1 7489  acdc2lem2 7490  acdc5lem1 7492  acdc5lem2 7493  acdclem 7495  acdcALT 7497  nn0ennn 7498  xpnnen 7500  znnenlem 7502  znnen 7503  infpnlem1 7507  ruclem24 7534  ruclem27 7537  ruclem28 7538  infxpidmlem4 7556  infxpidmlem5 7557  infxpidmlem7 7559  infxpidmlem8 7560  infxpidmlem9 7561  infunabs 7566  infcdaabs 7567  infdif 7569  infdif2 7570  infmap2lem2 7582  alephadd 7584  iunopnt 7600  eltopss 7604  istps2 7608  eltgt 7617  eltg2t 7618  tg2t 7620  tgclt 7623  eltg3t 7625  tgss2t 7636  basgen2t 7638  sn0top 7644  iscld 7666  ntrval2 7683  ntrss 7685  elcls 7701  neiss2 7713  neiint 7716  isneip 7717  neips 7724  islp2 7744  clslp 7745  cnpco 7766  iscncl 7767  cnsscnp 7769  sncld 7784  metreslem 7819  metxp 7831  blval 7834  bl2in 7840  opni 7861  opni3 7863  blssopn 7864  blnei 7876  metcnplem 7883  metcnpi 7887  metcnpi2 7888  metcnpi3 7889  metcnpi4 7890  metcni2 7892  metcnss 7895  metcnss2 7896  metdnsconst 7898  cncfmet 7902  ioo2bl 7909  tgioolem 7911  tgioo 7912  lmconst 7931  lmnn 7932  iscau3 7935  iscau4 7937  iscau5 7938  iscaunns 7941  caun0 7942  lmuni 7948  lmss 7950  lmfexlem2 7954  lmle 7957  metelcls 7962  xplmi 7970  xplm 7972  xpcn 7973  opr1cn 7975  bopcnlem2 7979  bopcnlem3 7980  fsumcnlem 7986  iscms2lem4 7989  lmcau 7993  cncms 7995  bcthlem2 7997  bcthlem7 8002  bcthlem9 8004  bcthlem14 8009  bcthlem16 8011  bcthlem18 8013  bcthlem20 8015  bcthlem21 8016  bcthlem26 8021  bcthlem28 8023  bcthlem31 8026  bcthlem33 8028  grpidinvlem2 8046  grpidinv 8049  grpideu 8050  grprcan 8059  grpinveu 8060  grpinvid1 8068  grpinvid2 8069  grplcan 8071  isgrp2i 8072  grpdivdiv 8083  grpmuldivass 8084  grppnpcan2 8088  grpnpncan 8090  abl4 8101  ablmuldiv 8103  abldivdiv4 8105  ablnnncan 8107  ablnnncan1 8109  subgopr 8114  subgabl 8119  vcdi 8167  vcdir 8168  vcass 8169  vcsubdir 8171  vcz 8185  nvex 8226  nvscom 8246  nvmdi 8266  nvsubadd 8271  cnnvm 8309  imsmetlem 8319  sqcn 8331  va1cnlem 8341  ipfval 8348  ipcl 8361  ip1cnilem6 8374  sspval 8378  sspmlem 8387  lnocoi 8414  nmoub3i 8432  0oo 8445  0lno 8446  nmlno0lem 8449  blocnilem 8460  cnph 8474  ipasslem1 8486  ipasslem2 8487  ipasslem4 8489  ipasslem5 8490  ipasslem11 8496  ipdi 8499  ipassr 8502  ipassr2 8503  ipsubdi 8505  ipblnfi 8512  ubthlem3 8527  ubthlem8 8532  ubthlem9 8533  ubthlem10 8534  minveclem17 8557  minveclem20 8560  minveclem22 8562  minveclem24 8564  minveclem25 8565  minveclem27 8567  minveclem30 8570  minveclem31 8571  htthlem5 8620  pstr 8648  pilem2 8667  abssinper 8707  efif1lem5 8729  shftefif1olem 8736  eff1i 8739  axgroth3 8774  grothinf 8776  hvmul0ort 8889  hvaddsubvalt 8897  hvsub4t 8901  hvpncant 8903  hvmulcant 8934  hvmulcan2t 8935  hvaddsub4t 8940  normpyct 9008  hlimcaui 9101  helch 9111  hhssnv 9129  occont 9155  ocorth 9159  occllem6 9173  occl 9176  projlem2 9182  projlem8 9188  projlem26 9206  pjtheu 9230  pjeq2t 9236  shscl 9276  shsel1t 9280  hsupss 9304  spanss 9313  orthin 9365  chsscon2t 9420  chpsscon2t 9423  chdmm3t 9445  chdmm4t 9446  chdmj3t 9449  chdmj4t 9450  h1de2b 9472  spansnss2t 9493  spanunsn 9497  h1datom 9499  osumlem7 9579  nonbool 9591  5oalem1 9594  5oalem2 9595  5oalem3 9596  5oalem5 9598  pjot 9611  pjsumt 9650  pjoi0t 9657  pjnorm2t 9667  hosubnegt 9728  honegsubdit 9731  hosub4t 9734  unopf1ot 9835  unopnormt 9836  nmlnop0ALT 9915  lnopm 9920  lnophs 9921  lnopco 9923  lnopeq0 9927  nmopunt 9934  nmcopexlem3 9948  nmcopexlem6 9951  nmcoplb 9953  nmophm 9956  lnopcon 9958  lnfnsub 9970  nmbdfnlb 9973  nmcfnexlem3 9977  nmcfnexlem6 9980  nmcfnlb 9982  lnfncon 9985  nlelsh 9988  nlelch 9989  riesz3 9990  riesz4 9991  riesz1t 9993  cnlnadjlem2 9996  cnlnadjlem6 10000  adjbdlnb 10012  nmopco 10023  adjco 10028  rnbra 10035  bra11 10036  cnvbravalt 10038  cnvbramult 10043  kbass4t 10047  kbass5t 10048  leoprf2t 10055  leoprft 10056  leopmulit 10061  leopnmidt 10066  pjbdln 10071  hmopidmch 10074  hmopidmpj 10075  pjadjco 10084  pjss1co 10086  pjss2co 10087  pjorthco 10092  pjscj 10093  pjssdif2 10097  pjhmopidm 10105  pjinvar 10114  pjclem4a 10121  pjclem4 10122  pjadj2co 10127  pj3s 10130  pj3cor1 10132  hstoct 10144  hstnmoct 10145  hstoht 10154  stcltr1 10196  cvcon3t 10206  cvnbtwnt 10208  mdbr3 10219  mdbr4 10220  dmdmdt 10222  dmdbr3 10227  dmdbr4 10228  dmdbr5 10230  mdsl0 10232  ssmd2 10234  mdslmd1lem2 10248  mdslmd2 10252  mdslmd3 10254  mdslmd4 10255  atcveq0 10270  superpos 10276  chjatom 10279  chrelat 10286  cvbr3 10289  atcv0eq 10301  atoml 10304  atcvatlem 10307  irredlem3 10314  atcvat3 10318  atcvat4 10319  atmd 10321  mdsymlem3 10327  mdsymlem4 10328  mdsymlem5 10329  sumdmdi 10337  sumdmdlem 10340  sumdmdlem2 10341  dmdbr6at 10345  cdjreu 10354  cdj1 10355  cdj3lem1 10356  cdj3lem2b 10359  cdj3 10363  nndivlub 10417  uninqs 10436  elo 10439  infi1 10441  fine 10442  sppfi 10472  inposet 10477  cdrci 10480  oisbmj 10484  truni1 10485  cnrsfin 10495  cnrscoa 10496  mapdiscn 10497  cnvhmph 10513  hmphsyma 10514  hmphre 10516  hmphtr 10517  hmpher 10522  hmeogrp 10524  homcard 10525  homcardus 10526  hmeobc 10528  setwoe 10532  top2usne 10535  qusp 10541  oefil2 10552  fgsb 10555  fgsb2 10560  cnfilca 10562  rcfpfillem3 10565  rcfpfillem4 10566  rcfpfil 10569  sfvlim 10576  mslb1 10600  iintlem1 10603  iint 10605  1ded 10642  1cat 10663  cmpassoh 10700  homgrf 10701  ismonb 10709  ismonb1 10710  ismonb2 10711  imonclem 10712  ismonc 10713  cmpmon 10714  icmpmon 10715  idmon 10716  isepib 10719  isepib1 10720  isepib2 10721  idfisf 10731

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