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 538  im2anan9 561  im2anan9r 562  bi2bian9 632  pm5.18 657  pm5.75 746  ccase2 754  prlem1 767  3ad2ant3 799  ax11v2 1199  ax11b 1204  sbcom 1242  sbal1 1328  ax11eq 1340  ax11el 1341  ax11inda 1348  euim 1398  euor2 1414  2exeu 1423  2eu5 1430  eqeqan12d 1466  sylan9eq 1503  vtoclegft 1831  eqvinc 1855  reu3 1902  sbcthdv 1918  sbccomglem 1959  sbccomg 1960  sbcralt 1961  csbcomg 1988  hbcsb1gd 1998  hbcsbgd 1999  sylan9ss 2046  elin 2178  sspr 2445  unissel 2495  intab 2528  copsex4g 2761  solin 2821  reuuni1 2845  alxfr 2859  ralxfrALT 2863  wefrc 2906  ordelon 2934  tz7.7 2936  ordunidif 2968  onint0 2970  onnmin 2978  onmindif 3023  onmindif2 3024  ordelsuc 3034  ordsucelsuc 3036  ordtri2or2 3041  ordsucun 3045  onsucuni2 3054  nlimsucg 3075  ordunisuc2 3078  limuni3 3086  tfi 3089  peano5 3116  findsg 3120  tfinds 3124  tfindsg 3125  ssnlim 3130  brinxp 3194  relssres 3343  relimasn 3376  soirri 3391  ssxpr 3424  xpexr2 3426  unixp0 3459  funssres 3492  funun 3494  fununi 3503  resfunexg 3519  cofunexg 3520  fco 3575  funssxp 3577  fssres2 3583  f1o2 3632  f1orescnv 3643  fnbrfvb 3692  fvelimab 3704  ssimaex 3707  dmfco 3712  fvco 3713  fvopab3ig 3717  fvimacnv 3744  fvimacnvALT 3748  dff2 3756  fopabco 3771  fopabcos 3772  fconst5 3787  iunexg 3801  f1ocnvfv1 3817  f1ocnvfv2 3818  isotr 3836  isotrALT 3837  isoini 3839  f1oiso 3843  tfrlem11 3860  tfr3 3865  rdglim2 3888  eloprabg 3946  oprssoprval 3973  f2ndres 4032  curry1 4036  oe0lem 4090  oe0 4099  oev2 4100  oasuc 4101  omsuc 4103  oesuc 4104  oalim 4105  omlim 4106  oecl 4110  oawordri 4122  oaord1 4123  oaword2 4125  oawordeulem 4126  oaordex 4130  oa00 4131  oalimcl 4132  oaass 4133  oarec 4134  omord 4137  omwordi 4140  omwordri 4141  omword1 4142  om00 4144  omlimcl 4147  odi 4148  oewordi 4156  oewordri 4157  oelim2 4160  nnarcl 4170  oaabs 4190  nneob 4193  omsmo 4195  ecoprass 4258  ecoprdi 4259  elmapg 4271  elpm 4274  fundmen 4363  pw2en 4380  sbthlem8 4388  sdomdomtr 4403  ensdomtr 4405  domsdomtr 4410  enen2 4412  domen1 4413  domen2 4414  fodomr 4417  mapenlem2 4422  mapxpen 4427  xpmapenlem5 4432  phplem2 4441  phplem4 4443  php2 4446  php3 4447  onomeneq 4450  onfin 4451  pssnn 4465  ssfi 4467  isfinite2 4475  unfilem1 4476  unfilem3 4478  fodomfi 4492  iunfi 4495  pwfi 4497  suppr 4514  zfregfr 4525  inf3lem6 4542  dfom3 4554  r1ord3 4581  r1val1 4582  tz9.12lem1 4583  rankr1 4598  ranklim 4609  r1pwcl 4611  rankxplim 4636  rankxplim3 4638  rankxpsuc 4639  aceq3 4657  ac6lem 4678  kmlem9 4697  zorn2lem3 4714  zorn2lem4 4715  zorn2lem6 4717  zorn2lem7 4718  fodom 4722  fodomb 4724  brdom7disj 4728  brdom6disj 4729  unidom 4732  carden 4755  carddom 4759  sucdom 4765  unxpdomlem 4766  cardlim 4774  cardiun 4782  alephcard 4790  alephnbtwn 4791  alephnbtwn2 4792  alephord 4798  alephsucdom 4803  cardaleph 4808  alephsson 4817  alephfp 4823  alephval2 4825  cflim 4832  cfeq0 4837  axextnd 4866  axrepndlem1 4867  axrepndlem2 4868  axunnd 4871  axpowndlem2 4873  axpowndlem3 4874  axpowndlem4 4875  axpownd 4876  axregndlem2 4878  axregnd 4879  axinfndlem1 4880  axinfnd 4881  axacndlem4 4885  axacndlem5 4886  axacnd 4887  addasspi 4946  mulasspi 4948  distrpi 4949  addnidpi 4951  ltapi 4953  ltmpi 4954  ltaddpq 5002  ltexpq2 5004  halfpq 5005  ltbtwnpq 5007  prub 5021  genpnmax 5033  mulclprlem 5044  distrlem1pr 5050  distrlem2pr 5051  1idpr 5056  psslinpr 5058  prlem934b 5061  prlem934 5062  ltaddpr 5063  ltexprlem6 5070  ltexpri 5072  ltapr 5074  prlem936 5078  reclem3pr 5081  reclem4pr 5082  suplem2pr 5085  mulgt0sr 5137  suppsr3 5147  axcnre 5209  cnegextlem1 5268  cnegextlem3 5270  cnegext 5271  0cnALT 5273  subnegt 5317  subeq0t 5326  muladd11t 5345  negsubdit 5380  submul2t 5383  nncant 5392  addsub4t 5396  ltxrt 5418  ltxrltt 5423  letrt 5449  xrltnsymt 5474  xrlttrit 5476  xrlttrt 5477  xrletrt 5488  xrret 5493  xrre2t 5494  ltleaddt 5570  ltaddpost 5575  lenegcon2t 5583  subge0t 5598  recextlem1 5606  recext 5608  divdivdivt 5692  conjmult 5704  letrp1t 5723  lt2msq 5780  lerec2t 5788  lediv12it 5795  ledivp1t 5804  xrmax2 5809  xrmin1 5810  xrmin2 5811  peano2nn 5834  nn2get 5841  nnleltp1t 5852  nnaddm1clt 5856  halfaddsubt 5939  avglet 5942  sup2 5949  infm3 5952  infmsup 5966  xrsupsslem 5974  xrinfmsslem 5975  xrsupss 5976  xrinfmss 5977  xrub 5978  supxrre 5981  nn0addclt 6018  nn0ltp1let 6025  nn0ltlem1t 6027  elnnz1 6053  znegclt 6061  zltp1let 6079  zltlem1t 6082  gtndivt 6091  primet 6093  zeot 6097  zneo 6098  zneoOLD 6099  peano2uz2 6100  uzind 6104  uzindOLD 6107  uzwo4OLD 6109  flget 6129  ceilet 6144  qaddclt 6158  qmulclt 6160  qbtwnxr 6168  om2uzlt 6186  seq1rn2 6209  ser1recl 6219  ser1add 6227  shftval3t 6236  shftf 6239  2shft 6240  shftcan2t 6241  elioo3g 6268  elioc2t 6273  elico2t 6274  elicc2t 6275  ioossre 6279  uztrn 6311  eluzp1lt 6317  peano2uzr 6331  uzaddclt 6332  uzind4i 6337  uzwo 6338  uzwoOLD 6339  elfz2t 6355  eluzfzt 6360  elfzle3 6368  fznt 6376  fznn0sub2t 6382  fzaddelt 6383  fzsubelt 6384  fzoptht 6385  fzss2t 6387  fzelp1t 6391  elfzp1 6393  fzrevt 6394  fzrev2t 6395  fzrev2it 6396  fzrev3t 6397  fzneuzt 6401  fsequb 6406  fseqsupcl 6408  fseqsupub 6409  seqzeq 6438  seqzrn2 6439  expnnvalt 6455  expp1t 6457  expm1t 6466  expge0t 6473  expge1t 6475  mulexpt 6476  expaddt 6478  expword2it 6487  expmwordit 6488  exple1t 6489  sqlecant 6523  subsqt 6524  subsq2t 6525  bernneq 6534  expnbndt 6536  sqr11 6584  sqrmsq2 6587  sqr2irr 6610  crutOLD 6620  rimul 6626  replimt 6643  resubt 6692  imsubt 6695  cjsubt 6702  sqabsaddt 6734  sqabssubt 6735  absexpt 6754  seq1bnd 6798  seq1ublem 6799  cau3ir 6803  cvganz 6812  caubnd 6814  facnn2t 6827  facclt 6828  facdivt 6830  facwordit 6832  faclbnd 6833  faclbnd3 6835  faclbnd4lem1 6836  faclbnd4lem3 6838  faclbnd4lem4 6839  faclbnd6 6842  facavgt 6843  bcval3t 6849  bcval4t 6850  bccl2t 6860  permnnt 6862  sumex 6870  sumeq2 6874  serzfsum 6893  fsum1 6894  fsum1s 6898  fsump1s 6902  fsumsplit 6909  csbfsum 6916  fsumcom 6917  fsumrev 6918  fsumconst 6927  fsumcmpndx2 6931  serzsplit 6945  binomlem1 6955  binomlem2 6956  binomlem4 6958  binomlem5 6959  binom1p 6962  bcxmas 6965  2climnn 6990  2climnn0 6991  climshft 6992  climshft2 6994  iserzshft2 6995  climrecl 6998  climge0 7000  climaddlem3 7003  climmullem1 7007  climmullem3 7009  climmullem4 7010  climmullem5 7011  climmullem8 7014  climsub 7017  iserzmulc1 7023  climcmplem 7024  climsqueeze 7027  climsqueeze2 7028  clim2serz 7032  climsup 7042  climcau 7043  caucvglem5 7048  caucvglem6 7049  caucvg 7050  ser1cmp2lem 7063  ser1cmp2 7064  isumnul 7089  isumreclt 7096  reccnv 7104  infcvglem3 7109  expcnvlem6 7118  geoisum1c 7131  cvgratlem1ALT 7133  cvgratlem1 7136  cvgratlem4 7139  cvgratlem5 7140  fsum0diaglem1 7142  fsum0diaglem2 7143  fsum0diag2 7145  fsum0diag4 7147  elcncf 7151  cncffvrn 7159  mulc1cncf 7165  ivthlem6 7172  ivthlem7 7173  ivthlem6OLD 7181  ivthlem7OLD 7182  eftclt 7196  efseq0ex 7204  efaddlem2 7232  efaddlem5 7235  efaddlem9 7239  efaddlem14 7244  efne0t 7262  efsubt 7264  efexpt 7265  reeftclt 7267  eftlclt 7272  reeftlclt 7273  abspef01tlub 7287  reeff1o 7319  sinsubt 7348  cossubt 7349  demoivre 7377  acdc3lem 7379  acdc2lem1 7381  acdc2lem2 7382  acdc5lem1 7384  acdc5lem2 7385  acdclem 7387  acdcALT 7389  nn0ennn 7390  xpnnen 7392  znnenlem 7394  znnenlemOLD 7395  znnen 7396  infpnlem1 7400  ruclem24 7427  ruclem27 7430  ruclem28 7431  infxpidmlem4 7449  infxpidmlem5 7450  infxpidmlem7 7452  infxpidmlem8 7453  infxpidmlem9 7454  infunabs 7459  infcdaabs 7460  infdif 7462  infdif2 7463  infmap2lem2 7473  alephadd 7475  iunopnt 7492  eltopss 7496  istps2 7500  eltgt 7511  eltg2t 7512  tg2t 7514  tgclt 7517  eltg3t 7519  tgss2t 7530  basgen2t 7532  sn0top 7540  iscld 7562  ntrval2 7579  ntrss 7581  elcls 7596  neiss2 7605  neiint 7608  isneip 7609  neips 7616  islp2 7636  clslp 7637  cnpco 7656  iscncl 7657  cnsscnp 7659  sncld 7674  metreslem 7710  metxp 7722  blval 7725  bl2in 7731  opni 7752  opni3 7754  blssopn 7755  blnei 7766  metcnplem 7773  metcnpi 7777  metcnpi2 7778  metcnpi3 7779  metcnpi4 7780  metcni2 7782  metcnss 7785  metcnss2 7786  metdnsconst 7788  cncfmet 7792  ioo2bl 7799  tgioolem 7801  tgioo 7802  lmconst 7820  lmnn 7821  iscau3 7824  iscau5 7826  caun0 7828  lmuni 7834  lmss 7836  lmfexlem2 7840  lmle 7843  metelcls 7848  xplmi 7855  xplm 7857  xpcn 7858  opr1cn 7860  bopcnlem2 7864  bopcnlem3 7865  fsumcnlem 7871  iscms2lem4 7874  lmcau 7878  cncms 7880  bcthlem2 7882  bcthlem7 7887  bcthlem9 7889  bcthlem14 7894  bcthlem16 7896  bcthlem18 7898  bcthlem20 7900  bcthlem21 7901  bcthlem26 7906  bcthlem28 7908  bcthlem31 7911  bcthlem33 7913  grpidinvlem2 7931  grpidinv 7934  grpideu 7935  grprcan 7945  grpinveu 7946  grpinvid1 7954  grpinvid2 7955  grplcan 7958  isgrp2i 7959  grpdivdiv 7970  grpmuldivass 7971  grppnpcan2 7975  grpnpncan 7977  abl4 7989  ablmuldiv 7992  abldivdiv4 7994  ablnnncan 7996  ablnnncan1 7998  subgopr 8003  subgabl 8008  vcdi 8058  vcdir 8059  vcass 8060  vcsubdir 8062  vcz 8076  nvscom 8128  nvmdi 8147  nvsubadd 8152  cnnvm 8188  imsmetlem 8198  sqcn 8207  va1cnlem 8214  ipfval 8221  ipcl 8234  ip1cnilem6 8247  sspval 8251  sspmlem 8260  lnocoi 8287  nmoub3i 8303  0oo 8316  0lno 8317  nmlno0lem 8320  blocnilem 8330  cnph 8344  ipasslem1 8356  ipasslem2 8357  ipasslem4 8359  ipasslem5 8360  ipasslem11 8366  ipdi 8369  ipassr 8372  ipassr2 8373  ipsubdi 8375  ipblnfi 8382  ubthlem3 8397  ubthlem8 8402  ubthlem9 8403  ubthlem10 8404  minveclem17 8427  minveclem20 8430  minveclem22 8432  minveclem24 8434  minveclem25 8435  minveclem27 8437  minveclem30 8440  minveclem31 8441  htthlem5 8488  pilem2 8504  efif1lem5 8562  shftefif1olem 8574  shftefif1olemOLD 8575  eff1i 8578  axgroth3 8631  grothinf 8633  uninqs 8701  elo 8704  infi1 8706  fine 8707  sppfi 8733  cdrci 8738  oisbmj 8742  truni1 8743  cnvhmph 8765  hmphsyma 8766  hmphre 8768  hmphtr 8769  hmpher 8774  hmeogrp 8776  qusp 8780  oefil2 8791  fgsb 8794  fgsb2 8799  cnfilca 8801  mslb1 8823  iintlem1 8826  iint 8828  1ded 8865  1cat 8886  cmpassoh 8923  homgrf 8924  ismonb 8930  ismonb1 8931  ismonb2 8932  imonclem 8933  ismonc 8934  cmpmon 8935  icmpmon 8937  hvmul0ort 9043  hvaddsubvalt 9051  hvsub4t 9055  hvpncant 9057  hvmulcant 9088  hvmulcan2t 9089  hvaddsub4t 9094  normpyct 9162  hlimcaui 9257  helch 9267  occont 9290  ocorth 9294  occllem6 9308  occl 9311  projlem2 9317  projlem8 9323  projlem26 9341  pjtheu 9364  pjeq2t 9370  shscl 9410  shsel1t 9414  hsupss 9438  spanss 9447  orthin 9499  chsscon2t 9554  chpsscon2t 9557  chdmm3t 9579  chdmm4t 9580  chdmj3t 9583  chdmj4t 9584  h1de2b 9606  h1de2bOLD 9607  spansnss2t 9629  spanunsn 9633  h1datom 9635  osumlem7 9715  nonbool 9727  5oalem1 9730  5oalem2 9731  5oalem3 9732  5oalem5 9734  pjot 9747  pjsumt 9786  pjoi0t 9793  pjnorm2t 9803  hosubnegt 9864  honegsubdit 9867  hosub4t 9870  unopf1ot 9970  unopnormt 9971  nmlnop0ALT 10049  lnopm 10054  lnophs 10055  lnopco 10057  lnopeq0 10061  nmopunt 10068  nmcopexlem3 10082  nmcopexlem6 10085  nmcoplb 10087  nmophm 10090  lnopcon 10092  lnfnsub 10104  nmbdfnlb 10107  nmcfnexlem3 10111  nmcfnexlem6 10114  nmcfnlb 10116  lnfncon 10119  nlelsh 10122  nlelch 10123  riesz3 10124  riesz4 10125  riesz1t 10127  cnlnadjlem2 10130  cnlnadjlem6 10134  adjbdlnb 10146  nmopco 10156  adjco 10161  rnbra 10167  bra11 10168  cnvbravalt 10170  cnvbramult 10174  kbass4t 10178  kbass5t 10179  leoprf2t 10186  leoprft 10187  leopmulit 10192  leopnmidt 10196  pjbdln 10201  hmopidmch 10204  hmopidmpj 10205  pjadjco 10214  pjss1co 10216  pjss2co 10217  pjorthco 10222  pjscj 10223  pjssdif2 10227  pjhmopidm 10234  pjinvar 10243  pjclem4a 10250  pjclem4 10251  pjadj2co 10256  pj3s 10259  pj3cor1 10261  hstoct 10273  hstnmoct 10274  hstoht 10283  stcltr1 10325  cvcon3t 10335  cvnbtwnt 10337  mdbr3 10348  mdbr4 10349  dmdmdt 10351  dmdbr3 10355  dmdbr4 10356  mdsl0 10359  ssmd2 10361  mdslmd1lem2 10375  mdslmd2 10379  mdslmd3 10381  mdslmd4 10382  atcveq0 10397  superpos 10403  chjatom 10406  chrelat 10413  cvbr3 10416  atcv0eq 10428  atoml 10431  atcvatlem 10434  irredlem3 10441  atcvat3 10445  atcvat4 10446  atmd 10448  mdsymlem3 10454  mdsymlem4 10455  mdsymlem5 10456  sumdmdi 10463  sumdmdlem 10466  sumdmdlem2 10467  dmdbr6at 10470  cdjreu 10478  cdj1 10479  cdj3lem1 10480  cdj3lem2b 10483  cdj3 10487

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