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.2i 171  jctl 290  jctr 291  jctil 292  jctir 293  adantl 388  adantlll 396  sylani 464  sylan2i 465  impbid1 515  impbid2 516  syl5bb 530  syl6bb 534  2th 716  biass 742  dedlemb 761  hbth 998  19.21t 1111  dvelimfALT 1149  cbv3 1160  cbval 1161  sbt 1188  sbie 1192  hbsb4 1243  sbidm 1249  sbco2 1250  sbcom2 1329  ax11eq 1356  ax11f 1358  ax11indalem 1361  ax11inda2ALT 1362  a12lem1 1369  eubii 1380  hbeu 1382  mobii 1398  moimv 1412  euor2 1430  2euswap 1438  syl5eq 1511  syl6eq 1515  3eqtr4a 1524  syl5eqel 1544  syl5eleq 1546  syl6eqel 1548  syl6eleq 1550  ralbii 1659  rexbii 1660  r19.20si 1698  r19.22si 1726  ralcom2 1768  reubii 1774  hbeqd 1904  hbeld 1905  reu8 1926  sbcieg 1951  sbcbii 1968  hbsbc1gd 1973  hbsbcgd 1974  sbcralt 1980  sbcralgf 1982  hbcsb1gd 2017  hbcsbgd 2018  csbnestglem 2025  csbnest1g 2027  ssconb 2160  reuun1 2267  difsn 2455  snsspr 2461  sspr 2466  hbopd 2488  int0el 2551  eliun 2560  dfiun2 2577  iunab 2587  iun0 2594  syl5breq 2640  ssbri 2647  hbbrd 2649  sbcbrg 2652  opabbii 2661  csbopabg 2668  axrep4 2687  axsep 2692  dfid3 2826  reuuni2f 2873  reuuni2 2874  reuuni4 2877  reuxfr2 2893  reuunixfr 2896  ordtr2 2992  oneqmini 3007  bm2.5ii 3009  trsucss 3046  suceloni 3052  onuninsuc 3098  nlimsucg 3102  orduninsuc 3104  ordunisuc2 3105  onzsl 3107  dfom2 3123  limom 3136  peano3 3141  peano5 3143  finds1 3149  ssrel 3237  ssxp 3246  relopab 3256  hbimad 3396  csbima12g 3397  resiima 3403  ssxprOLD 3461  ssxpr 3462  relssdr 3499  unielrel 3500  relfld 3501  funssres 3538  opabex2 3596  fnopab2 3604  fun 3626  hbfvd 3715  hbfvd2 3716  tz6.12f 3723  csbfv12g 3727  fvelrnb 3745  dfimafn2 3747  fvelimab 3750  fnsnfv 3752  ssimaex 3753  fvopab4g 3764  eqfnfv 3782  elrnopab 3786  fimacnv 3795  fconst4 3836  iunex 3848  funiunfv 3851  cbvfo 3870  isomin 3884  isoini 3885  f1oweALT 3891  tfrlem4 3899  tfrlem10 3905  tz7.49 3944  abianfplem 3946  abianfp 3947  hboprd 3967  csboprg 3971  oprabbii 3982  oprabex2g 4005  oprabex3 4007  oprabval2gf 4011  oprabval3 4015  oprabval6g 4017  oprvalelrn 4024  1st2val 4079  2nd2val 4080  1stcof 4085  dfoprab5 4099  fnoprab2 4106  elrnoprab 4109  df1st2 4110  df2nd2 4111  oev2 4146  om0r 4158  oaordi 4164  oaord 4165  oaordex 4176  oarec 4180  omordi 4181  omord2 4182  oeord 4199  oewordri 4203  oeworde 4204  oelim2 4206  nnaordex 4233  nnawordex 4234  nneob 4239  omsmolem 4240  brecop 4290  mapsspw 4325  mapss 4330  en2 4383  en3 4384  dom2 4386  fundmen 4409  mapsnen 4410  map1 4411  xpsnen 4415  xpcomen 4419  xpassen 4421  pw2en 4426  sbthbg 4438  canth2 4464  mapdom2lem 4473  mapdom2 4474  mapxpen 4475  xpmapenlem5 4480  mapunen 4482  ssenen 4484  phplem4 4491  nneneq 4492  php3 4495  pssnn 4513  domfi 4516  unfilem1 4524  unfi 4528  unifi 4532  fiint 4534  fodomfib 4541  iunfi 4543  pwfi 4545  pm54.43 4546  inf0 4578  inf3lem3 4587  inf3lem4 4588  dfom3 4602  infensuc 4610  r1lim 4625  r1ord3 4629  ranksn 4661  rankuni2 4662  rankval4 4674  rankc2 4678  rankxpl 4682  rankxpsuc 4687  scott0 4689  cplem1 4692  karden 4698  hta 4700  aceq3lem 4704  aceq5lem4 4710  aceq5lem5 4711  ac6lem 4726  kmlem3 4739  zorn2lem6 4765  zorn2lem7 4766  zorn 4769  fodomb 4772  brdom7disj 4776  brdom6disj 4777  unidom 4780  carden 4803  cardlim 4823  cardiun 4831  alephlim 4836  alephnbtwn2 4841  alephord 4847  alephord3 4850  cardaleph 4857  cardalephex 4858  cardinfima 4863  alephfplem3 4870  alephval3 4875  cfeq0 4886  cfsuc 4887  axextnd 4915  axrepndlem1 4916  axrepndlem2 4917  axunndlem1 4919  axunnd 4920  axpowndlem2 4922  axpowndlem4 4924  axpownd 4925  axregnd 4928  axinfndlem1 4929  axacndlem4 4934  zfcndrep 4938  indpi 5006  ltsopq 5047  prlem934a 5109  prlem936a 5125  reclem4pr 5131  suplem1pr 5133  ltsosr 5175  sqgt0sr 5187  suppsr2 5195  suppsr3 5196  pre-axltadd 5261  pre-axmulgt0 5262  pre-axsup 5263  hbnegd 5335  ltxrt 5467  lelttrt 5496  ltletrt 5497  xrlelttrt 5535  xrltletrt 5536  muleqaddt 5669  divdivmult 5751  lemul12itOLD 5799  mulgt1t 5801  lediv12it 5844  squeeze0 5872  nn1suc 5887  nnleltp1t 5901  nnsub 5903  nnaddm1clt 5905  sup2 5998  dfinfmr 6014  infmsup 6015  xrsupexmnf 6021  xrinfmexpnf 6022  xrsupsslem 6023  xrinfmsslem 6024  xrub 6027  supxrre 6030  supxrmnf 6034  elznn0 6096  nn0subt 6108  zaddclt 6112  zmulclt 6127  zltp1let 6128  dfuz 6150  uzind 6153  uzind2 6154  uzindOLD 6156  nn0ind 6160  flval3t 6182  flhalft 6189  elq 6195  om2uzlt 6235  om2uzlt2 6236  om2uzran 6237  iooval2t 6304  elioc2t 6322  elico2t 6323  elicc2t 6324  ioossre 6328  iccf 6334  uzssz 6362  uzind4i 6386  uzwo 6387  uzwoOLD 6388  elfz2nn0t 6427  fsequb 6455  limsupclt 6462  expordit 6531  expwordit 6534  expubndt 6539  sqlecant 6572  expnbndt 6585  sqrlem6 6608  sqrlem12 6614  cjclt 6696  reret 6734  cjreimt 6763  cjreim2t 6764  absdivz 6794  leabst 6799  abssubne0t 6820  cjdiv 6826  seq1ublem 6848  cau5i 6854  cvg3 6860  faclbnd 6882  faclbnd4lem1 6885  faclbnd4lem4 6888  bcn0t 6901  bcnp11t 6903  fsum1s 6947  fsump1s 6951  fsum1p 6957  fsummulc1 6971  fsumconst 6976  fsumcmp 6978  fsumcmp0 6979  fsumcmpndx2 6980  fsumabs 6981  ser1ser0 6986  binomlem1 7004  binomlem2 7005  binomlem4 7007  bcxmas 7014  climconst 7031  climmullem3 7058  climmulc2 7065  iserzshft 7080  clim2serz 7081  caucvglem2 7094  caucvg3lem 7102  caucvg3t 7104  ser1f0 7106  ser1clim0 7109  cvgcmp2lem 7116  cvgcmpub 7121  isumclim3t 7135  isumnul 7138  fnsmnt 7161  expcnvlem6 7167  geolimilem 7170  georeclim 7175  cvgratlem1ALT 7182  fsum0diag 7193  elcncf1i 7206  mulc1cncf 7214  ivthlem6 7221  ivthlem7 7222  ivthlem6OLD 7230  ivthlem7OLD 7231  ef0lem 7252  efaddlem2 7281  efaddlem10 7289  efaddlem13 7292  efaddlem15 7294  efaddlem16 7295  efaddlem18 7297  efaddlem19 7298  efaddlem23 7302  efaddlem25 7304  ef1tllem 7323  ef01tllem1 7325  ef01tllem2 7326  eirrlem2 7331  abspef01tlub 7336  efcnlem2 7360  reeff1o 7368  efi4pt 7377  subcost 7402  abseft 7425  acdc3lem 7428  acdc2lem2 7431  acdc5lem2 7434  acdclem 7436  acdcALT 7438  infxpidmlem7 7501  infxpidmlem8 7502  infxpdom 7514  infmap2 7523  alephsuc3 7527  subbas2 7587  subtop 7588  indistop 7590  distop 7591  fctop 7592  cctop 7594  iooretop 7601  iincld 7621  clscld 7625  clsval2 7627  sscls 7631  ntrss2 7632  ssnei 7665  idcn 7705  cnpco 7708  iscncl 7709  cncnplem4 7716  cnconst 7719  sncld 7726  metdmdm 7747  blssm 7790  ssblex 7796  opnfss 7798  opnin 7809  tgioolem 7853  dscmet 7856  lmconst 7872  iscau3 7876  caussi 7889  xplmi 7907  fsumcnlem 7923  lmcau 7930  bcthlem8 7940  bcthlem14 7946  bcthlem18 7950  grpidinv2 7994  grpinv 8003  grpsn 8061  cnid 8064  vc0 8125  vcm 8127  vsfval 8194  nvm 8202  nvnncan 8223  nvdif 8232  nmcnc 8276  sm1cnilem 8281  ipfval 8286  ipval2 8291  ipid 8297  ssps 8323  lno0 8351  nmoxr 8361  nmoge0 8362  nmolb 8366  nmoubi 8367  nmoub3i 8368  nmlnoubi 8388  nmblolbii 8390  isblo3i 8392  blocni 8396  phpar 8414  ubthlem5 8464  minveclem9 8484  minveclem35 8510  minvecdist 8516  htthlem11 8560  pslem 8573  psdmrn 8574  spwval2 8577  spwval3 8578  spwnex3 8579  sinperlem1 8605  sinperlem2 8606  coshalfpip 8618  efifolem5 8641  eff1o 8670  hial0 8889  hial02 8890  bcseq 8907  hlim0 9026  hlimreu 9031  occllem6 9094  occllem7 9095  pjthlem7 9140  pjthlem13 9146  fh1t 9478  osumlem3 9497  osum 9503  hosubid1t 9641  honegnegt 9649  hoeq2t 9674  eigpos 9679  nmopxrt 9710  nmfnxrt 9723  specclt 9742  hhblo 9745  nmoplbt 9748  nmopubt 9749  nmfnlbt 9764  nmfnleubt 9765  elnlfn2t 9769  0cnop 9819  0cnfn 9820  nmopunt 9854  nmbdoplb 9864  nmcopexlem5 9870  nmcoplb 9873  nmophm 9876  lnopcon 9878  nmbdfnlb 9893  nmcfnexlem5 9899  nmcfnlb 9902  lnfncon 9905  cnlnadjlem5 9919  cnlnssadj 9928  adjbdlnt 9931  adjbdlnb 9932  nmopadjlem 9937  nmoptri 9941  nmopco 9942  nmopcoadj 9948  branmfnt 9951  bra11 9954  kbass2t 9962  leop3t 9970  leopmult 9979  leopnmidt 9982  pjbdln 9987  stadd 10083  stadd3 10085  ssmd1 10146  ssmd2 10147  mdslj1 10154  mdslj2 10155  mdslmd1lem1 10160  mdslmd1lem2 10161  csmdsym 10169  elat2 10175  shatomistic 10196  atcvat4 10232  mdsymlem3 10240  mdsymlem6 10243  mdsymlem8 10245  cdj1 10265  infi1 10347  fine 10348  11st22nd 10354  moec 10357  clsrebb 10380  cdrci 10381  homeofval 10403  idhme 10409  hmphsyma 10415  hmphre 10417  hmeogrp 10425  homcard 10426  subsp 10429  qusp 10430  oefil2 10441  fgsb 10444  infi 10448  fgsb2 10449  cnfilca 10451  dtt2 10462  clicls 10466  msr3 10469  msr4 10470  mslb1 10473  2wsms 10474  msra3 10475  cnvtr 10482  1ded 10515  aidm 10527  aidmold 10528  1cat 10536  ishomb 10560  imonclem 10583  ismonc 10584  isfuna 10592

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

Copyright terms: Public domain