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 715  biass 741  dedlemb 760  hbth 977  19.21t 1091  dvelimfALT 1136  cbv3 1147  cbval 1148  sbt 1175  sbie 1179  hbsb4 1232  sbidm 1238  sbco2 1239  sbcom2 1316  ax11eq 1340  ax11f 1342  ax11indalem 1345  ax11inda2ALT 1346  a12lem1 1353  eubii 1364  hbeu 1366  mobii 1382  moimv 1396  euor2 1414  2euswap 1422  syl5eq 1495  syl6eq 1499  3eqtr4a 1508  syl5eqel 1528  syl5eleq 1530  syl6eqel 1532  syl6eleq 1534  ralbii 1643  rexbii 1644  r19.20si 1682  r19.22si 1710  ralcom2 1752  reubii 1758  hbeqd 1885  hbeld 1886  reu8 1907  sbcieg 1932  sbcbii 1949  hbsbc1gd 1954  hbsbcgd 1955  sbcralt 1961  sbcralgf 1963  hbcsb1gd 1998  hbcsbgd 1999  csbnestglem 2006  csbnest1g 2008  ssconb 2141  reuun1 2248  difsn 2434  snsspr 2440  sspr 2445  hbopd 2466  int0el 2529  eliun 2538  dfiun2 2555  iunab 2565  iun0 2572  syl5breq 2618  ssbri 2625  hbbrd 2627  sbcbrg 2630  opabbii 2639  csbopabg 2646  axrep4 2665  axsep 2670  dfid3 2799  reuuni2f 2846  reuuni2 2847  reuuni4 2850  reuxfr2 2866  reuunixfr 2869  ordtr2 2965  oneqmini 2980  bm2.5ii 2982  trsucss 3019  suceloni 3025  onuninsuc 3071  nlimsucg 3075  orduninsuc 3077  ordunisuc2 3078  onzsl 3080  dfom2 3096  limom 3109  peano3 3114  peano5 3116  finds1 3122  ssrel 3209  ssxp 3218  relopab 3228  hbimad 3363  csbima12g 3364  resiima 3370  ssxpr 3424  relssdr 3455  unielrel 3456  relfld 3457  funssres 3492  opabex2 3550  fnopab2 3558  fun 3580  hbfvd 3669  hbfvd2 3670  tz6.12f 3677  csbfv12g 3681  fvelrnb 3699  dfimafn2 3701  fvelimab 3704  fnsnfv 3706  ssimaex 3707  fvopab4g 3718  eqfnfv 3736  elrnopab 3740  fimacnv 3749  fconst4 3790  iunex 3802  funiunfv 3805  cbvfo 3824  isomin 3838  isoini 3839  f1oweALT 3845  tfrlem4 3853  tfrlem10 3859  tz7.49 3898  abianfplem 3900  abianfp 3901  hboprd 3921  csboprg 3925  oprabbii 3936  oprabex2g 3959  oprabex3 3961  oprabval2gf 3965  oprabval3 3969  oprabval6g 3971  oprvalelrn 3978  1st2val 4033  2nd2val 4034  1stcof 4039  dfoprab5 4053  fnoprab2 4060  elrnoprab 4063  df1st2 4064  df2nd2 4065  oev2 4100  om0r 4112  oaordi 4118  oaord 4119  oaordex 4130  oarec 4134  omordi 4135  omord2 4136  oeord 4153  oewordri 4157  oeworde 4158  oelim2 4160  nnaordex 4187  nnawordex 4188  nneob 4193  omsmolem 4194  brecop 4244  mapsspw 4279  mapss 4284  en2 4337  en3 4338  dom2 4340  fundmen 4363  mapsnen 4364  map1 4365  xpsnen 4369  xpcomen 4373  xpassen 4375  pw2en 4380  sbthbg 4392  canth2 4418  mapdom2lem 4425  mapdom2 4426  mapxpen 4427  xpmapenlem5 4432  mapunen 4434  ssenen 4436  phplem4 4443  nneneq 4444  php3 4447  pssnn 4465  domfi 4468  unfilem1 4476  unfi 4480  unifi 4484  fiint 4486  fodomfib 4493  iunfi 4495  pwfi 4497  pm54.43 4498  inf0 4530  inf3lem3 4539  inf3lem4 4540  dfom3 4554  infensuc 4562  r1lim 4577  r1ord3 4581  ranksn 4613  rankuni2 4614  rankval4 4626  rankc2 4630  rankxpl 4634  rankxpsuc 4639  scott0 4641  cplem1 4644  karden 4650  hta 4652  aceq3lem 4656  aceq5lem4 4662  aceq5lem5 4663  ac6lem 4678  kmlem3 4691  zorn2lem6 4717  zorn2lem7 4718  zorn 4721  fodomb 4724  brdom7disj 4728  brdom6disj 4729  unidom 4732  carden 4755  cardlim 4774  cardiun 4782  alephlim 4787  alephnbtwn2 4792  alephord 4798  alephord3 4801  cardaleph 4808  cardalephex 4809  cardinfima 4814  alephfplem3 4821  alephval3 4826  cfeq0 4837  cfsuc 4838  axextnd 4866  axrepndlem1 4867  axrepndlem2 4868  axunndlem1 4870  axunnd 4871  axpowndlem2 4873  axpowndlem4 4875  axpownd 4876  axregnd 4879  axinfndlem1 4880  axacndlem4 4885  zfcndrep 4889  indpi 4957  ltsopq 4998  prlem934a 5060  prlem936a 5076  reclem4pr 5082  suplem1pr 5084  ltsosr 5126  sqgt0sr 5138  suppsr2 5146  suppsr3 5147  pre-axltadd 5212  pre-axmulgt0 5213  pre-axsup 5214  hbnegd 5286  ltxrt 5418  lelttrt 5447  ltletrt 5448  xrlelttrt 5486  xrltletrt 5487  muleqaddt 5620  divdivmult 5702  lemul12itOLD 5750  mulgt1t 5752  lediv12it 5795  squeeze0 5823  nn1suc 5838  nnleltp1t 5852  nnsub 5854  nnaddm1clt 5856  sup2 5949  dfinfmr 5965  infmsup 5966  xrsupexmnf 5972  xrinfmexpnf 5973  xrsupsslem 5974  xrinfmsslem 5975  xrub 5978  supxrre 5981  supxrmnf 5985  elznn0 6047  nn0subt 6059  zaddclt 6063  zmulclt 6078  zltp1let 6079  dfuz 6101  uzind 6104  uzind2 6105  uzindOLD 6107  nn0ind 6111  flval3t 6133  flhalft 6140  elq 6146  om2uzlt 6186  om2uzlt2 6187  om2uzran 6188  iooval2t 6255  elioc2t 6273  elico2t 6274  elicc2t 6275  ioossre 6279  iccf 6285  uzssz 6313  uzind4i 6337  uzwo 6338  uzwoOLD 6339  elfz2nn0t 6378  fsequb 6406  limsupclt 6413  expordit 6482  expwordit 6485  expubndt 6490  sqlecant 6523  expnbndt 6536  sqrlem6 6559  sqrlem12 6565  cjclt 6647  reret 6685  cjreimt 6714  cjreim2t 6715  absdivz 6745  leabst 6750  abssubne0t 6771  cjdiv 6777  seq1ublem 6799  cau5i 6805  cvg3 6811  faclbnd 6833  faclbnd4lem1 6836  faclbnd4lem4 6839  bcn0t 6852  bcnp11t 6854  fsum1s 6898  fsump1s 6902  fsum1p 6908  fsummulc1 6922  fsumconst 6927  fsumcmp 6929  fsumcmp0 6930  fsumcmpndx2 6931  fsumabs 6932  ser1ser0 6937  binomlem1 6955  binomlem2 6956  binomlem4 6958  bcxmas 6965  climconst 6982  climmullem3 7009  climmulc2 7016  iserzshft 7031  clim2serz 7032  caucvglem2 7045  caucvg3lem 7053  caucvg3t 7055  ser1f0 7057  ser1clim0 7060  cvgcmp2lem 7067  cvgcmpub 7072  isumclim3t 7086  isumnul 7089  fnsmnt 7112  expcnvlem6 7118  geolimilem 7121  georeclim 7126  cvgratlem1ALT 7133  fsum0diag 7144  elcncf1i 7157  mulc1cncf 7165  ivthlem6 7172  ivthlem7 7173  ivthlem6OLD 7181  ivthlem7OLD 7182  ef0lem 7203  efaddlem2 7232  efaddlem10 7240  efaddlem13 7243  efaddlem15 7245  efaddlem16 7246  efaddlem18 7248  efaddlem19 7249  efaddlem23 7253  efaddlem25 7255  ef1tllem 7274  ef01tllem1 7276  ef01tllem2 7277  eirrlem2 7282  abspef01tlub 7287  efcnlem2 7311  reeff1o 7319  efi4pt 7328  subcost 7353  abseft 7376  acdc3lem 7379  acdc2lem2 7382  acdc5lem2 7385  acdclem 7387  acdcALT 7389  infxpidmlem7 7452  infxpidmlem8 7453  infxpdom 7465  infmap2 7474  alephsuc3 7478  subbas2 7538  subtop 7539  indistop 7541  distop 7542  fctop 7543  cctop 7545  iooretop 7552  iincld 7572  clscld 7576  clsval2 7578  sscls 7582  ntrss2 7583  ssnei 7613  idcn 7653  cnpco 7656  iscncl 7657  cncnplem4 7664  cnconst 7667  sncld 7674  metdmdm 7695  blssm 7738  ssblex 7744  opnfss 7746  opnin 7757  tgioolem 7801  dscmet 7804  lmconst 7820  iscau3 7824  caussi 7837  xplmi 7855  fsumcnlem 7871  lmcau 7878  bcthlem8 7888  bcthlem14 7894  bcthlem18 7898  grpidinv2 7942  grpinv 7951  grpsn 8009  cnid 8012  vc0 8075  vcm 8077  vsfval 8132  nvm 8139  nvnncan 8160  nvdif 8169  nmcnc 8213  sm1cnilem 8216  ipfval 8221  ipval2 8226  ipid 8232  ssps 8258  lno0 8286  nmoxr 8296  nmoge0 8297  nmolb 8301  nmoubi 8302  nmoub3i 8303  nmlnoubi 8323  nmblolbii 8325  isblo3i 8327  blocni 8331  phpar 8349  ubthlem5 8399  minveclem9 8419  minveclem35 8445  minvecdist 8451  htthlem11 8494  sinperlem1 8518  sinperlem2 8519  coshalfpip 8531  efifolem5 8554  eff1o 8583  infi1 8706  fine 8707  11st22nd 8713  moec 8716  clsrebb 8737  cdrci 8738  homeofval 8754  idhme 8760  hmphsyma 8766  hmphre 8768  hmeogrp 8776  subsp 8779  qusp 8780  oefil2 8791  fgsb 8794  infi 8798  fgsb2 8799  cnfilca 8801  dtt2 8812  clicls 8816  msr3 8819  msr4 8820  mslb1 8823  2wsms 8824  msra3 8825  cnvtr 8832  1ded 8865  aidm 8877  aidmold 8878  1cat 8886  ishomb 8910  imonclem 8933  ismonc 8934  isfuna 8940  hial0 9117  hial02 9118  bcseq 9135  hlim0 9256  hlimreu 9261  occllem6 9308  occllem7 9309  pjthlem7 9354  pjthlem13 9360  fh1t 9692  osumlem3 9711  osum 9717  hosubid1t 9855  honegnegt 9863  hoeq2t 9888  eigpos 9893  nmopxrt 9924  nmfnxrt 9937  specclt 9956  hhblo 9959  nmoplbt 9962  nmopubt 9963  nmfnlbt 9978  nmfnleubt 9979  elnlfn2t 9983  0cnop 10033  0cnfn 10034  nmopunt 10068  nmbdoplb 10078  nmcopexlem5 10084  nmcoplb 10087  nmophm 10090  lnopcon 10092  nmbdfnlb 10107  nmcfnexlem5 10113  nmcfnlb 10116  lnfncon 10119  cnlnadjlem5 10133  cnlnssadj 10142  adjbdlnt 10145  adjbdlnb 10146  nmopadjlem 10151  nmoptri 10155  nmopco 10156  nmopcoadj 10162  branmfnt 10165  bra11 10168  kbass2t 10176  leop3t 10184  leopmult 10193  leopnmidt 10196  pjbdln 10201  stadd 10297  stadd3 10299  ssmd1 10360  ssmd2 10361  mdslj1 10368  mdslj2 10369  mdslmd1lem1 10374  mdslmd1lem2 10375  csmdsym 10383  elat2 10389  shatomistic 10410  atcvat4 10446  mdsymlem3 10454  mdsymlem6 10457  mdsymlem8 10459  cdj1 10479

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

Copyright terms: Public domain