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  sbcieg 1964  sbcbii 1981  hbsbc1gd 1986  hbsbcgd 1987  sbcralt 1993  sbcralgf 1995  hbcsb1gd 2030  hbcsbgd 2031  csbnestglem 2038  csbnest1g 2040  ssconb 2173  reuun1 2280  difsn 2468  snsspr 2474  sspr 2479  hbopd 2501  int0el 2565  eliun 2574  dfiun2 2591  iunab 2601  iun0 2608  syl5breq 2655  ssbri 2662  hbbrd 2664  sbcbrg 2667  opabbii 2676  csbopabg 2683  axrep4 2702  axsep 2707  dfid3 2842  reuuni2f 2889  reuuni2 2890  reuuni4 2893  reuxfr2 2909  reuunixfr 2912  ordtr2 3008  oneqmini 3023  bm2.5ii 3025  trsucss 3062  suceloni 3068  onuninsuc 3114  nlimsucg 3118  orduninsuc 3120  ordunisuc2 3121  onzsl 3123  dfom2 3139  limom 3152  peano3 3157  peano5 3159  finds1 3165  ssrel 3253  ssxp 3262  relopab 3272  hbimad 3418  csbima12g 3419  resiima 3425  ssxpr 3481  relssdr 3519  unielrel 3520  relfld 3521  funssres 3558  opabex2 3616  fnopab2 3624  fun 3647  hbfvd 3736  hbfvd2 3737  tz6.12f 3744  csbfv12g 3748  fvelrnb 3766  dfimafn2 3768  fvelimab 3771  fnsnfv 3773  ssimaex 3774  fvopab4g 3785  eqfnfv 3803  elrnopab 3807  fimacnv 3816  fconst4 3857  iunex 3869  funiunfv 3872  cbvfo 3891  isomin 3905  isoini 3906  f1oweALT 3912  tfrlem4 3920  tfrlem10 3926  tz7.49 3965  abianfplem 3967  abianfp 3968  hboprd 3988  csboprg 3992  oprabbii 4003  oprabex2g 4026  oprabex3 4028  oprabval2gf 4032  oprabval3 4036  oprabval6g 4038  oprvalelrn 4045  1stcof 4107  dfoprab5 4121  fnoprab2 4128  elrnoprab 4131  df1st2 4132  df2nd2 4133  oev2 4168  om0r 4180  oaordi 4186  oaord 4187  oaordex 4198  oarec 4202  omordi 4203  omord2 4204  oeord 4221  oewordri 4225  oeworde 4226  oelim2 4228  nnaordex 4255  nnawordex 4256  nneob 4261  omsmolem 4262  brecop 4312  mapsspw 4347  mapss 4352  isfi 4388  en2 4408  en3 4409  dom2 4411  fundmen 4434  mapsnen 4435  map1 4436  xpsnen 4441  xpcomen 4445  xpassen 4447  pw2en 4452  sbthbg 4464  canth2 4490  mapdom2lem 4499  mapdom2 4500  mapxpen 4501  xpmapenlem5 4506  mapunen 4508  ssenen 4510  phplem4 4517  nneneq 4518  php3 4521  php3OLD 4522  pssnn 4544  domfiOLD 4550  unfilem1 4560  unfi 4563  unfiOLD 4564  unifiOLD 4570  fiint 4572  fiintOLD 4573  pwfi 4579  pwfiOLD 4580  pm54.43 4581  inf0 4615  inf3lem3 4624  inf3lem4 4625  dfom3 4639  infensuc 4648  r1lim 4663  r1ord3 4667  ranksn 4699  rankuni2 4700  rankval4 4712  rankc2 4716  rankxpl 4720  rankxpsuc 4725  scott0 4727  cplem1 4730  karden 4736  hta 4738  aceq3lem 4742  aceq5lem4 4748  aceq5lem5 4749  ac6lem 4764  kmlem3 4777  zorn2lem6 4803  zorn2lem7 4804  zorn 4807  fodomb 4810  brdom7disj 4814  brdom6disj 4815  unidom 4818  carden 4841  cardlim 4862  cardiun 4870  alephlim 4875  alephnbtwn2 4880  alephord 4886  alephord3 4889  cardaleph 4896  cardalephex 4897  cardinfima 4902  alephfplem3 4909  alephval3 4914  cfeq0 4926  cfsuc 4927  axextnd 4955  axrepndlem1 4956  axrepndlem2 4957  axunndlem1 4959  axunnd 4960  axpowndlem2 4962  axpowndlem4 4964  axpownd 4965  axregnd 4968  axinfndlem1 4969  axacndlem4 4974  zfcndrep 4978  indpi 5046  ltsopq 5087  prlem934a 5149  prlem936a 5165  reclem4pr 5171  suplem1pr 5173  ltsosr 5215  sqgt0sr 5227  suppsr2 5235  suppsr3 5236  pre-axltadd 5301  pre-axmulgt0 5302  pre-axsup 5303  hbnegd 5375  ltxrt 5507  lelttrt 5535  ltletrt 5536  xrlelttrt 5574  xrltletrt 5575  muleqaddt 5712  divdivmult 5797  lemul12itOLD 5845  mulgt1t 5847  lediv12it 5898  squeeze0 5926  nn1suc 5941  nnleltp1t 5956  nnsub 5958  nnaddm1clt 5960  sup2 6053  dfinfmr 6069  infmsup 6070  xrsupexmnf 6076  xrinfmexpnf 6077  xrsupsslem 6078  xrinfmsslem 6079  xrub 6082  supxrre 6085  supxrmnf 6089  elznn0 6151  nn0subt 6163  zaddclt 6167  zmulclt 6182  zltp1let 6183  dfuz 6204  uzind 6207  uzind2 6208  uzindOLD 6210  nn0ind 6214  flval3t 6241  flhalft 6248  intfracq 6255  elq 6258  om2uzlt 6299  om2uzlt2 6300  om2uzran 6301  iooval2t 6368  elioc2t 6391  elico2t 6392  elicc2t 6393  iccf 6402  uzssz 6431  uzind4i 6455  uzwo 6456  uzwoOLD 6457  elfz2nn0t 6496  fsequb 6524  limsupclt 6531  expordit 6601  expwordit 6604  expubndt 6609  sqlecant 6642  expnbndt 6655  sqrlem6 6679  sqrlem12 6685  cjclt 6765  cjreimt 6828  cjreim2t 6829  absdivz 6859  leabst 6864  abssubne0t 6882  cjdiv 6888  seq1ublem 6911  cau5i 6917  cvg3 6923  faclbnd 6945  faclbnd4lem1 6948  faclbnd4lem4 6951  bcn0t 6963  bcnp11t 6965  fsum1s 7009  fsump1s 7013  fsum1p 7019  fsummulc1 7033  fsumcmp 7040  fsumcmp0 7041  fsumcmpndx2 7042  fsumabs 7043  ser1ser0 7048  binomlem1 7066  binomlem2 7067  binomlem4 7069  bcxmas 7076  climconst 7094  climmullem3 7122  climmulc2 7129  iserzshft 7144  clim2serz 7145  caucvglem2 7158  caucvg3lem 7166  caucvg3t 7168  ser1clim0 7173  cvgcmp2lem 7180  cvgcmpub 7185  isumclim3t 7200  isumnul 7203  fnsmnt 7226  expcnvlem6 7232  geolimilem 7235  georeclim 7240  cvgratlem1ALT 7247  fsum0diag 7258  elcncf1i 7271  mulc1cncf 7279  ivthlem6 7286  ivthlem7 7287  ef0lem 7310  efaddlem2 7339  efaddlem10 7347  efaddlem13 7350  efaddlem15 7352  efaddlem16 7353  efaddlem18 7355  efaddlem19 7356  efaddlem23 7360  efaddlem25 7362  ef1tllem 7381  ef01tllem1 7383  ef01tllem2 7384  ef01tllem2OLD 7385  eirrlem2 7390  abspef01tlub 7395  efcnlem2 7420  reeff1o 7426  efi4pt 7435  subcost 7460  abseft 7484  acdc3lem 7487  acdc2lem2 7490  acdc5lem2 7493  infxpidmlem7 7559  infxpidmlem8 7560  infxpdom 7572  infmap2 7583  alephsuc3 7587  subtop 7643  indistop 7645  distop 7646  fctopOLD 7647  cctop 7649  iooretop 7656  iincld 7676  clscld 7680  clsval2 7682  sscls 7686  ntrss2 7687  ssnei 7721  idcn 7763  cnpco 7766  iscncl 7767  cncnplem4 7774  cnconst 7777  sncld 7784  metdmdm 7805  blssm 7847  ssblex 7853  opnfss 7855  opnin 7866  tgioolem 7911  dscmet 7915  lmconst 7931  iscau3 7935  iscau4 7937  caussi 7951  xplmi 7970  fsumcnlem 7986  lmcau 7993  bcthlem8 8003  bcthlem14 8009  bcthlem18 8013  grpidinv2 8056  grpinv 8065  grpsn 8120  cnid 8123  vc0 8184  vcm 8186  vsfval 8250  nvm 8258  nvnncan 8279  nvdif 8289  nmcn3 8337  nmcnc 8338  sm1cnilem 8343  ipfval 8348  ipval2 8353  ipid 8359  ssps 8385  lno0 8413  nmoxr 8425  nmoge0 8426  nmolb 8430  nmoubi 8431  nmoub3i 8432  nmlnoubi 8452  nmblolbii 8455  isblo3i 8457  blocni 8461  phpar 8479  ubthlem5 8529  minveclem35 8575  minvecdist 8581  htthlem11 8626  pslem 8643  psdmrn 8644  spwval2 8649  spwval3 8650  spwnex3 8651  spwpr4OLD 8658  spwpr4aOLD 8659  sinperlem1 8681  sinperlem2 8682  coshalfpip 8696  abssinper 8707  efifolem5 8721  eff1o 8743  hial0 8963  hial02 8964  bcseq 8981  hlim0 9100  hlimreu 9105  occllem6 9173  occllem7 9174  pjthlem7 9220  pjthlem13 9226  fh1t 9556  osumlem3 9575  osum 9581  hosubid1t 9719  honegnegt 9727  hoeq2t 9752  eigpos 9757  nmopxrt 9788  nmfnxrt 9801  specclt 9820  hhblo 9823  nmoplbt 9826  nmopubt 9827  nmfnlbt 9843  nmfnleubt 9844  elnlfn2t 9848  0cnop 9898  0cnfn 9899  nmopunt 9934  nmbdoplb 9944  nmcopexlem5 9950  nmcoplb 9953  nmophm 9956  lnopcon 9958  nmbdfnlb 9973  nmcfnexlem5 9979  nmcfnlb 9982  lnfncon 9985  cnlnadjlem5 9999  cnlnssadj 10008  adjbdlnt 10011  adjbdlnb 10012  nmopadjlem 10017  adjeq0 10019  nmoptri 10022  nmopco 10023  nmopcoadj 10029  branmfnt 10033  bra11 10036  kbass2t 10045  leop3t 10053  leopmult 10062  leopnmidt 10066  pjbdln 10071  stadd 10168  stadd3 10170  ssmd1 10233  ssmd2 10234  mdslj1 10241  mdslj2 10242  mdslmd1lem1 10247  mdslmd1lem2 10248  csmdsym 10256  elat2 10262  shatomistic 10283  atcvat4 10319  mdsymlem3 10327  mdsymlem6 10330  mdsymlem8 10332  cdj1 10355  infi1 10441  fine 10442  11st22nd 10448  moec 10451  inposet 10477  clsrebb 10479  cdrci 10480  homeofval 10502  idhme 10508  hmphsyma 10514  hmphre 10516  hmeogrp 10524  homcard 10525  eqindhome 10527  hmeobc 10528  top2usne 10535  homindlem3 10537  subsp 10540  qusp 10541  oefil2 10552  fgsb 10555  infi 10559  fgsb2 10560  cnfilca 10562  rcfpfil 10569  limfillem2OLD 10579  dtt2 10589  clicls 10593  msr3 10596  msr4 10597  mslb1 10600  2wsms 10601  cnvtr 10609  1ded 10642  aidm 10654  1cat 10663  ishomb 10687  ismonc 10713  isepia 10718  isfuna 10725

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

Copyright terms: Public domain