Theorem a1i 8

Description: Inference derived from axiom ax-1 4. See a1d 12 for an explanation of our informal use of the terms "inference" and "deduction."

Hypothesis

Ref	Expression
a1i.1	|- ph

Assertion

Ref	Expression
a1i	|- (ps -> ph)

Proof of Theorem a1i

Step	Hyp	Ref	Expression
1		a1i.1	. 2 |- ph
2		ax-1 4	. 2 |- (ph -> (ps -> ph))
3	1, 2	ax-mp 7	1 |- (ps -> ph)

Syntax hints:   -> wi 3

This theorem is referenced by:  syl 10  imim2i 17  mpi 44  mpdi 48  syl9 57  idd 61  pm2.21i 77  pm2.24i 104  pm2.61d1 128  pm2.61d2 129  pm4.2d 171  jctl 290  jctr 291  jctil 292  jctir 293  adantl 390  adantlll 398  sylani 466  sylan2i 467  impbid1 519  impbid2 520  syl5bb 534  syl6bb 538  2th 720  biass 746  dedlemb 765  hbth 1003  19.21t 1117  dvelimfALT 1155  cbv3 1166  cbval 1167  sbt 1194  sbie 1198  hbsb4 1250  sbidm 1256  sbco2 1257  sbcom2 1336  dvelimALT 1355  ax11eq 1365  ax11f 1367  ax11indalem 1370  ax11inda2ALT 1371  a12lem1 1378  eubii 1389  hbeu 1391  mobii 1407  moimv 1421  euor2 1440  2euswap 1448  eqidd 1479  syl5eq 1522  syl6eq 1526  3eqtr4a 1535  syl5eqel 1555  syl5eleq 1557  syl6eqel 1559  syl6eleq 1561  ralbii 1670  rexbii 1671  r19.20si 1709  r19.22si 1737  ralcom2 1779  reubii 1785  hbeqd 1916  hbeld 1917  reu8 1939  cbvsbcv 1961  sbcieg 1965  sbcbii 1982  hbsbc1gd 1987  hbsbcgd 1988  sbcralt 1994  sbcralgf 1996  hbcsb1gd 2031  hbcsbgd 2032  csbnestglem 2039  csbnest1g 2041  ssconb 2174  reuun1 2281  difsn 2469  snsspr 2475  sspr 2480  hbopd 2502  int0el 2566  eliun 2575  dfiun2 2592  iunab 2602  iun0 2609  syl5breq 2656  ssbri 2663  hbbrd 2665  sbcbrg 2668  opabbii 2677  csbopabg 2684  axrep4 2703  axsep 2708  dfid3 2843  reuuni2f 2890  reuuni2 2891  reuuni4 2894  reuxfr2 2910  reuunixfr 2913  ordtr2 3009  oneqmini 3024  bm2.5ii 3026  trsucss 3063  suceloni 3069  onuninsuc 3115  nlimsucg 3119  orduninsuc 3121  ordunisuc2 3122  onzsl 3124  dfom2 3140  limom 3153  peano3 3158  peano5 3160  finds1 3166  ssrel 3254  ssxp 3263  relopab 3273  hbimad 3419  csbima12g 3420  resiima 3426  ssxpr 3482  relssdr 3520  unielrel 3521  relfld 3522  funssres 3559  opabex2 3617  fnopab2 3625  fun 3648  hbfvd 3737  hbfvd2 3738  tz6.12f 3745  csbfv12g 3749  fvelrnb 3767  dfimafn2 3769  fvelimab 3772  fnsnfv 3774  ssimaex 3775  fvopab4g 3786  eqfnfv 3804  elrnopab 3808  fimacnv 3817  fconst4 3858  iunex 3870  funiunfv 3873  cbvfo 3892  isomin 3906  isoini 3907  f1oweALT 3913  tfrlem4 3921  tfrlem10 3927  tz7.49 3966  abianfplem 3968  abianfp 3969  hboprd 3989  csboprg 3993  oprabbii 4004  oprabex2g 4027  oprabex3 4029  oprabval2gf 4033  oprabval3 4037  oprabval6g 4039  oprvalelrn 4046  1stcof 4108  dfoprab5 4122  fnoprab2 4129  elrnoprab 4132  df1st2 4133  df2nd2 4134  oev2 4169  om0r 4181  oaordi 4187  oaord 4188  oaordex 4199  oarec 4203  omordi 4204  omord2 4205  oeord 4222  oewordri 4226  oeworde 4227  oelim2 4229  nnaordex 4256  nnawordex 4257  nneob 4262  omsmolem 4263  brecop 4313  mapsspw 4348  mapss 4353  isfi 4389  en2 4409  en3 4410  dom2 4412  fundmen 4435  mapsnen 4436  map1 4437  xpsnen 4442  xpcomen 4446  xpassen 4448  pw2en 4453  sbthbg 4465  canth2 4491  mapdom2lem 4500  mapdom2 4501  mapxpen 4502  xpmapenlem5 4507  mapunen 4509  ssenen 4511  phplem4 4518  nneneq 4519  php3 4522  php3OLD 4523  pssnn 4546  domfiOLD 4552  unfilem1 4562  unfi 4565  unfiOLD 4566  unifi 4572  unifiOLD 4574  fiint 4576  fiintOLD 4577  pwfi 4586  pwfiOLD 4587  pm54.43 4588  inf0 4622  inf3lem3 4631  inf3lem4 4632  dfom3 4646  infensuc 4655  r1lim 4670  r1ord3 4674  ranksn 4706  rankuni2 4707  rankval4 4719  rankc2 4723  rankxpl 4727  rankxpsuc 4732  scott0 4734  cplem1 4737  karden 4743  hta 4745  aceq3lem 4749  aceq5lem4 4755  aceq5lem5 4756  ac6lem 4771  kmlem3 4784  zorn2lem6 4810  zorn2lem7 4811  zorn 4814  fodomb 4817  brdom7disj 4821  brdom6disj 4822  unidom 4825  carden 4848  cardlim 4869  cardiun 4877  alephlim 4882  alephnbtwn2 4887  alephord 4893  alephord3 4896  cardaleph 4903  cardalephex 4904  cardinfima 4909  alephfplem3 4916  alephval3 4921  cfeq0 4933  cfsuc 4934  axextnd 4962  axrepndlem1 4963  axrepndlem2 4964  axunndlem1 4966  axunnd 4967  axpowndlem2 4969  axpowndlem4 4971  axpownd 4972  axregnd 4975  axinfndlem1 4976  axacndlem4 4981  zfcndrep 4985  indpi 5053  ltsopq 5094  prlem934a 5156  prlem936a 5172  reclem4pr 5178  suplem1pr 5180  ltsosr 5222  sqgt0sr 5234  suppsr2 5242  suppsr3 5243  pre-axltadd 5308  pre-axmulgt0 5309  pre-axsup 5310  hbnegd 5382  ltxrt 5514  lelttrt 5542  ltletrt 5543  xrlelttrt 5581  xrltletrt 5582  muleqaddt 5719  divdivmult 5804  lemul12itOLD 5852  mulgt1t 5854  lediv12it 5905  squeeze0 5933  nn1suc 5948  nnleltp1t 5963  nnsub 5965  nnaddm1clt 5967  sup2 6060  dfinfmr 6076  infmsup 6077  xrsupexmnf 6083  xrinfmexpnf 6084  xrsupsslem 6085  xrinfmsslem 6086  xrub 6089  supxrre 6092  supxrmnf 6096  elznn0 6158  nn0subt 6170  zaddclt 6174  zmulclt 6189  zltp1let 6190  dfuz 6211  uzind 6214  uzind2 6215  uzindOLD 6217  nn0ind 6221  flval3t 6248  flhalft 6255  intfracq 6262  elq 6265  om2uzlt 6306  om2uzlt2 6307  om2uzran 6308  iooval2t 6375  elioc2t 6398  elico2t 6399  elicc2t 6400  iccf 6409  uzssz 6438  uzind4i 6462  uzwo 6463  uzwoOLD 6464  elfz2nn0t 6503  fsequb 6531  limsupclt 6538  expordit 6608  expwordit 6611  expubndt 6616  sqlecant 6649  expnbndt 6662  sqrlem6 6686  sqrlem12 6692  cjclt 6772  cjreimt 6835  cjreim2t 6836  absdivz 6866  leabst 6871  abssubne0t 6889  cjdiv 6895  seq1ublem 6918  cau5i 6924  cvg3 6930  faclbnd 6952  faclbnd4lem1 6955  faclbnd4lem4 6958  bcn0t 6970  bcnp11t 6972  fsum1s 7016  fsump1s 7020  fsum1p 7026  fsummulc1 7040  fsumcmp 7047  fsumcmp0 7048  fsumcmpndx2 7049  fsumabs 7050  ser1ser0 7055  binomlem1 7073  binomlem2 7074  binomlem4 7076  bcxmas 7083  climconst 7101  climmullem3 7129  climmulc2 7136  iserzshft 7151  clim2serz 7152  caucvglem2 7165  caucvg3lem 7173  caucvg3t 7175  ser1clim0 7180  cvgcmp2lem 7187  cvgcmpub 7192  isumclim3t 7207  isumnul 7210  fnsmnt 7233  expcnvlem6 7239  geolimilem 7242  georeclim 7247  cvgratlem1ALT 7254  fsum0diag 7265  elcncf1i 7278  mulc1cncf 7286  ivthlem6 7293  ivthlem7 7294  ef0lem 7317  efaddlem2 7346  efaddlem10 7354  efaddlem13 7357  efaddlem15 7359  efaddlem16 7360  efaddlem18 7362  efaddlem19 7363  efaddlem23 7367  efaddlem25 7369  ef1tllem 7388  ef01tllem1 7390  ef01tllem2 7391  ef01tllem2OLD 7392  eirrlem2 7397  abspef01tlub 7402  efcnlem2 7427  reeff1o 7433  efi4pt 7442  subcost 7467  abseft 7491  acdc3lem 7494  acdc2lem2 7497  acdc5lem2 7500  infxpidmlem7 7566  infxpidmlem8 7567  infxpdom 7579  infmap2 7590  alephsuc3 7594  subtop 7650  indistop 7652  distop 7653  fctopOLD 7654  cctop 7656  iooretop 7663  iincld 7683  clscld 7687  clsval2 7689  sscls 7693  ntrss2 7694  ssnei 7728  idcn 7770  cnpco 7773  iscncl 7774  cncnplem4 7781  cnconst 7784  sncld 7791  metdmdm 7812  blssm 7854  ssblex 7860  opnfss 7862  opnin 7873  tgioolem 7918  dscmet 7922  lmconst 7938  iscau3 7942  iscau4 7944  caussi 7958  xplmi 7977  fsumcnlem 7993  lmcau 8000  bcthlem8 8010  bcthlem14 8016  bcthlem18 8020  grpidinv2 8063  grpinv 8072  grpsn 8127  cnid 8130  vc0 8191  vcm 8193  vsfval 8257  nvm 8265  nvnncan 8286  nvdif 8296  nmcn3 8344  nmcnc 8345  sm1cnilem 8350  ipfval 8355  ipval2 8360  ipid 8366  ssps 8392  lno0 8420  nmoxr 8432  nmoge0 8433  nmolb 8437  nmoubi 8438  nmoub3i 8439  nmlnoubi 8459  nmblolbii 8462  isblo3i 8464  blocni 8468  phpar 8486  ubthlem5 8536  minveclem35 8582  minvecdist 8588  htthlem11 8633  pslem 8650  psdmrn 8651  spwval2 8656  spwval3 8657  spwnex3 8658  spwpr4OLD 8665  spwpr4aOLD 8666  sinperlem1 8688  sinperlem2 8689  coshalfpip 8703  abssinper 8714  efifolem5 8728  eff1o 8750  hial0 8970  hial02 8971  bcseq 8988  hlim0 9107  hlimreu 9112  occllem6 9180  occllem7 9181  pjthlem7 9227  pjthlem13 9233  fh1t 9563  osumlem3 9582  osum 9588  hosubid1t 9726  honegnegt 9734  hoeq2t 9759  eigpos 9764  nmopxrt 9795  nmfnxrt 9808  specclt 9827  hhblo 9830  nmoplbt 9833  nmopubt 9834  nmfnlbt 9850  nmfnleubt 9851  elnlfn2t 9855  0cnop 9905  0cnfn 9906  nmopunt 9941  nmbdoplb 9951  nmcopexlem5 9957  nmcoplb 9960  nmophm 9963  lnopcon 9965  nmbdfnlb 9980  nmcfnexlem5 9986  nmcfnlb 9989  lnfncon 9992  cnlnadjlem5 10006  cnlnssadj 10015  adjbdlnt 10018  adjbdlnb 10019  nmopadjlem 10024  adjeq0 10026  nmoptri 10029  nmopco 10030  nmopcoadj 10036  branmfnt 10040  bra11 10043  kbass2t 10052  leop3t 10060  leopmult 10069  leopnmidt 10073  pjbdln 10078  stadd 10176  stadd3 10178  ssmd1 10241  ssmd2 10242  mdslj1 10249  mdslj2 10250  mdslmd1lem1 10255  mdslmd1lem2 10256  csmdsym 10264  elat2 10270  shatomistic 10291  atcvat4 10327  mdsymlem3 10335  mdsymlem6 10338  mdsymlem8 10340  cdj1 10363  infi1 10449  fine 10450  11st22nd 10456  moec 10459  inposet 10485  clsrebb 10487  cdrci 10488  homeofval 10510  idhme 10516  hmphsyma 10522  hmphre 10524  hmeogrp 10532  homcard 10533  eqindhome 10535  hmeobc 10536  top2usne 10543  homindlem3 10545  subsp 10548  qusp 10549  oefil2 10560  fgsb 10563  infi 10567  fgsb2 10568  cnfilca 10570  rcfpfil 10577  limfillem2OLD 10587  dtt2 10597  clicls 10601  msr3 10604  msr4 10605  mslb1 10608  2wsms 10609  cnvtr 10617  1ded 10650  aidm 10662  1cat 10671  ishomb 10695  ismonc 10721  isepia 10726  isfuna 10733

This theorem was proved from axioms:  ax-1 4  ax-mp 7

Copyright terms: Public domain