Theorem a1i 9

Description: Inference derived from axiom ax-1 5. See a1d 22 for an explanation of our informal use of the terms "inference" and "deduction." See also the comment in syld 45. (Contributed by NM, 5-Aug-1993.)

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 5	. 2 |- ( ph -> ( ps -> ph ) )
3	1, 2	ax-mp 7	1 |- ( ps -> ph )

Syntax hints:   -> wi 4

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

This theorem is referenced by:  mp1i  10  imim2i  12  syl  14  mpi  15  idd  21  a1i13  24  2a1i  27  syl6  33  mpdi  43  mpii  44  mpsyl  65  syl7  69  syl8  71  syl9  72  impbid21d  127  impbid1  141  mpbii  147  mpbiri  167  biidd  171  2th  173  syl5bb  191  syl6bb  195  imbi2i  225  jctil  306  jctir  307  sylani  399  sylan2i  400  sylancl  405  sylancr  406  mpan  416  mpan2  417  mpani  422  mpan2i  423  anbi2i  446  anbi1i  447  nsyl3  594  mt2  607  mt2i  611  mto  626  mtoi  628  sylnib  639  simprimdc  797  con1biimdc  808  pm2.54dc  831  pm5.17dc  851  pm5.21nd  866  pm5.71dc  910  dedlema  918  dedlemb  919  a1tru  1312  xorbi12i  1326  dfbi3dc  1340  hbth  1404  dfexdc  1442  a17d  1472  nfvd  1474  nfan  1509  nfim  1516  19.21ht  1525  nfbi  1533  alrimd  1553  19.32dc  1621  equsexd  1671  spime  1683  equveli  1696  sbieh  1727  dvelimfALT2  1752  cbvald  1855  cbvexdh  1856  nfsbxy  1873  sbcomxyyz  1901  dvelimALT  1941  dvelimfv  1942  hbsb4t  1944  dvelimor  1949  eubii  1964  nfeudv  1970  nfmo  1975  mobii  1992  moimv  2021  2euswapdc  2046  eqidd  2096  syl5eq  2139  syl6eq  2143  syl5eqel  2181  syl5eleq  2183  syl6eqel  2185  syl6eleq  2187  nfcvd  2236  dvelimc  2256  nnedc  2267  necon1idc  2315  ralbii  2395  rexbii  2396  nfraldxy  2421  nfrexdxy  2422  nfralxy  2425  nfrexxy  2426  nfralya  2427  nfrexya  2428  rgenw  2441  ralimi  2449  rexim  2479  reximi  2482  rexlimivw  2498  r19.29af2  2522  r19.32vdc  2530  nfreudxy  2554  nfreuxy  2555  reubii  2566  rmobii  2571  rabbii  2619  ceqsralt  2660  vtoclgft  2683  rr19.28v  2770  reu8  2825  cdeqth  2841  nfsbc1d  2870  nfsbc1  2871  nfsbc  2874  sbcbii  2912  sbc2iegf  2923  sbc2iedv  2925  sbc3ie  2926  sbcrext  2930  rmob  2945  sbcnel12g  2962  sbcne12g  2963  csbcomg  2968  csbeq2i  2971  nfcsb1  2976  nfcsb  2979  csbiebt  2981  csbief  2986  csbie2t  2990  sbcnestgf  2993  syl5ss  3050  syl6ss  3051  ssidd  3060  syl5sseqr  3090  syl6eqss  3091  difssd  3142  ssconb  3148  abvor0dc  3325  rabnc  3334  nfif  3439  disjpr2  3526  tpid3g  3577  neldifsnd  3593  diftpsn3  3600  preq12bg  3639  intmin  3730  int0el  3740  dfiun2  3786  dfiin2  3787  dfiunv2  3788  iunrab  3799  iunid  3807  iun0  3808  iinrabm  3814  iunin1  3816  2iunin  3818  iinin1m  3821  syl5breq  3902  ssbri  3909  nfbr  3911  opabbii  3927  mpteq2i  3947  mpteq12i  3948  opth1  4087  copsexg  4095  copsex4g  4098  epelg  4141  issod  4170  fr0  4202  frind  4203  trsucss  4274  bm2.5ii  4341  ordsucss  4349  onsucelsucr  4353  ordunisuc2r  4359  ordirr  4386  ordfr  4418  peano5  4441  finds1  4445  ordom  4449  0elnn  4460  omsinds  4463  0nelrel  4513  csbcnvg  4651  dfiun3  4724  dfiin3  4725  dmcosseq  4736  resiun1  4764  resiun2  4765  resima2  4779  iss  4791  resiima  4823  relbrcnvg  4844  inimasn  4882  elxp4  4952  elxp5  4953  dfco2  4964  coiun  4974  relssdmrn  4985  unielrel  4992  relfld  4993  cnviinm  5006  cnvsom  5008  nfiotadxy  5017  nfiotaxy  5018  iota2df  5038  funssres  5090  fntp  5105  imadif  5128  imain  5130  sbcfng  5193  sbcfg  5194  fun  5218  fun11iun  5309  funcocnv2  5313  f1oprg  5330  sefvex  5361  tz6.12f  5368  dfimafn2  5389  fnsnfv  5398  ssimaex  5400  fvun1  5405  fvmptg  5415  fvmpt3i  5419  fvopab6  5435  fndmdifcom  5444  respreima  5466  fmptco  5503  fcoconst  5507  dfmpt  5513  fmptapd  5527  fmptpr  5528  isocnv2  5629  riotaexg  5650  nfriotadxy  5654  nfriota  5655  riota2f  5667  nfov  5717  oprabbii  5742  mpt2eq123i  5750  ovmpt4g  5805  ovmpt2dxf  5808  ovmpt2x  5811  ovmpt2ga  5812  ovi3  5819  ov6g  5820  ovelrn  5831  caovcom  5840  caovass  5843  caovdi  5862  caovimo  5876  ofc12  5913  oprabex3  5938  reldm  5994  oprabco  6020  oprab2co  6021  disjsnxp  6040  mpt2xopoveq  6043  sprmpt2  6045  brtpos2  6054  reldmtpos  6056  dmtpos  6059  dftpos4  6066  tposfn2  6069  smores  6095  tfrlemisucfn  6127  tfrlemiubacc  6133  tfri1dALT  6154  tfrcl  6167  tfri1  6168  rdgon  6189  frec0g  6200  frectfr  6203  freccllem  6205  frecfcllem  6207  frecsuclem  6209  oacl  6261  omcl  6262  oeicl  6263  oawordi  6270  nnsucelsuc  6292  nntri1  6297  nnsseleq  6302  nnaord  6308  nnmordi  6315  nnmord  6316  nnaordex  6326  nnm00  6328  swoer  6360  eqer  6364  0er  6366  uniqs  6390  erinxp  6406  qliftf  6417  brecop  6422  ecopovtrn  6429  ecopover  6430  ecopoverg  6433  th3qlem1  6434  elpmg  6461  nfixpxy  6514  ixpintm  6522  ixpsnf1o  6533  brdomg  6545  en2i  6567  en3i  6568  dom2  6572  dom3  6573  ener  6576  ensymb  6577  entr  6581  fundmen  6603  mapsnen  6608  map1  6609  xpsnen  6617  xpassen  6626  ssenen  6647  nneneq  6653  phplem4dom  6658  phpelm  6662  phplem4on  6663  fidceq  6665  fiunsnnn  6677  finexdc  6698  infm  6700  exmidpw  6704  unfidisj  6712  undifdc  6714  unfiin  6716  fiintim  6719  xpfi  6720  fisseneq  6722  ssfirab  6723  fnfi  6726  iunfidisj  6735  f1finf1o  6736  fidcenumlemrk  6743  fidcenumlemr  6744  supubti  6774  suplubti  6775  cnvinfex  6793  eqinfti  6795  infvalti  6797  inflbti  6799  ordiso2  6808  djuex  6816  djuss  6841  1stinl  6845  2ndinl  6846  1stinr  6847  2ndinr  6848  updjudhcoinlf  6851  updjudhcoinrg  6852  casefun  6856  caseinl  6862  djufun  6866  ctmlemr  6870  ctm  6871  finomni  6883  fodjuomnilemdc  6887  fodjuf  6888  fodjum  6889  fodju0  6890  nnnninf  6894  omnimkv  6899  mkvprop  6901  cardcl  6906  pm54.43  6915  en2other2  6919  exmidfodomrlemr  6925  exmidfodomrlemrALT  6926  elni2  6970  indpi  6998  enqeceq  7015  mulcanenqec  7042  ltnnnq  7079  enq0er  7091  enq0eceq  7093  nqnq0pi  7094  mulcanenq0ec  7101  nnnq0lem1  7102  addnq0mo  7103  mulnq0mo  7104  prarloclemlo  7150  prarloclem3  7153  genipv  7165  nqprrnd  7199  nqprdisj  7200  nqprloc  7201  1idprl  7246  1idpru  7247  recexprlemlol  7282  recexprlemupu  7284  cauappcvgprlemm  7301  cauappcvgprlemdisj  7307  cauappcvgprlemladdru  7312  cauappcvgprlemladdrl  7313  cauappcvgpr  7318  caucvgprlemm  7324  caucvgprlemcl  7332  caucvgprlemladdrl  7334  caucvgpr  7338  caucvgprprlemml  7350  caucvgprprlemmu  7351  caucvgprprlemopu  7355  caucvgprprlemclphr  7361  enreceq  7379  prsrlem1  7385  addsrmo  7386  mulsrmo  7387  0idsr  7410  pn0sr  7414  recexgt0sr  7416  archsr  7424  srpospr  7425  prsradd  7428  prsrlt  7429  caucvgsrlemfv  7433  caucvgsrlembound  7436  caucvgsrlemoffval  7438  caucvgsrlemoffcau  7440  caucvgsrlemoffgt1  7441  caucvgsrlemoffres  7442  caucvgsr  7444  pitonnlem1p1  7480  pitoregt0  7483  recidpirqlemcalc  7491  recidpirq  7492  axcnex  7493  axmulcl  7500  axmulass  7505  axdistr  7506  ax0id  7510  axprecex  7512  axpre-ltirr  7514  axpre-lttrn  7516  axpre-ltadd  7518  axpre-mulgt0  7519  axpre-mulext  7520  axcaucvglemval  7529  axcaucvg  7532  0cnd  7578  0red  7586  1red  7600  1cnd  7601  ltxrlt  7649  1p1times  7713  nfneg  7776  negsub  7827  addlsub  7945  pncan1  7952  npcan1  7953  negf1o  7957  kcnktkm1cn  7958  mulsubfacd  7993  rereim  8160  cru  8176  apreim  8177  mulreim  8178  apadd1  8182  apneg  8185  muleqadd  8234  eqneg  8296  mulgt1  8421  suprlubex  8510  negiso  8513  dfinfre  8514  sup3exmid  8515  cju  8519  nn1suc  8539  2cnd  8593  avglt1  8752  avglt2  8753  add1p1  8763  sub1m1  8764  cnm2m1cnm3  8765  xp1d2m1eqxm1d2  8766  div4p1lem1div2  8767  nn0p1gt0  8800  un0addcl  8804  nn0ge2m1nn  8831  0zd  8860  elnn0z  8861  elznn0  8863  1zzd  8875  peano2z  8884  ztri3or0  8890  zlelttric  8893  zltnle  8894  zmulcl  8901  zltp1le  8902  zgt0ge1  8906  elz2  8916  zdceq  8920  zdclt  8922  nn0lt2  8926  nn0le2is012  8927  zneo  8946  nneo  8948  zeo2  8951  uzind  8956  uzind2  8957  nn0ind  8959  zadd2cl  8974  uzm1  9148  uzin  9150  uz3m2nn  9160  uzind4i  9179  infrenegsupex  9181  supminfex  9184  eqreznegel  9198  nn01to3  9201  nn0ge2m1nnALT  9202  divfnzn  9205  cnref1o  9232  rpnegap  9265  divlt1lt  9300  divle1le  9301  ltxr  9345  xrre3  9388  xaddf  9410  xaddval  9411  xaddnemnf  9423  xaddnepnf  9424  xaddass2  9436  xltadd1  9442  xaddge0  9444  xlt2add  9446  xleaddadd  9453  ixxssixx  9468  elioc2  9502  elico2  9503  elicc2  9504  lincmb01cmp  9569  fzdcel  9603  ige3m2fz  9612  fz01en  9616  fzdifsuc  9644  elfz1b  9653  uzsplit  9655  fseq1p1m1  9657  elfzp1b  9660  ige2m1fz1  9672  ige2m1fz  9673  0elfz  9681  fz0tp  9684  fz0fzdiffz0  9690  nn0split  9696  nnsplit  9697  fzoval  9708  fzouzsplit  9739  elfzom1elp1fzo  9762  elfzonlteqm1  9770  fzo0to3tp  9779  fzo0sn0fzo1  9781  fzosplitprm1  9794  fvinim0ffz  9801  qlelttric  9805  qltnle  9806  qdceq  9807  qbtwnrelemcalc  9816  qbtwnre  9817  ioo0  9820  ioom  9821  ico0  9822  ioc0  9823  2tnp1ge0ge0  9857  flhalf  9858  fldiv4p1lem1div2  9861  intfracq  9876  q0mod  9911  q1mod  9912  mulp1mod1  9921  modqnegd  9935  modsumfzodifsn  9952  frec2uzltd  9959  frec2uzlt2d  9960  frecfzennn  9982  1tonninf  9995  iseqvalcbv  10012  seq3val  10013  seq3-1  10014  seqf  10015  seq3p1  10016  seq3clss  10017  monoord  10026  seq3caopr3  10031  seq3f1olemp  10052  seq3id3  10057  seq3homo  10060  seq3z  10061  ser0  10064  ser3ge0  10067  exp0  10074  expgt1  10108  ltexp2a  10122  leexp2a  10123  leexp2r  10124  exple1  10126  expubnd  10127  binom21  10181  binom2sub1  10183  zesq  10187  expnlbnd2  10194  sqeq0d  10200  sqoddm1div8  10221  expcanlem  10239  expcan  10240  nn0opthlem1d  10243  nn0opthlem2d  10244  faclbnd  10264  faclbnd2  10265  bc0k  10279  bcn1  10281  bcn2  10287  bcn2m1  10292  bcn2p1  10293  fihashen1  10322  hashunlem  10327  1elfz0hash  10329  hashprg  10331  hashdifpr  10343  hashxp  10349  zfz1isolem1  10360  seq3coll  10362  shftuz  10366  ovshftex  10368  shftfn  10373  imval  10399  crre  10406  crim  10407  remim  10409  cjreb  10415  readd  10418  remullem  10420  imadd  10426  cjadd  10433  cjreim  10452  cjreim2  10453  cjap  10455  cnrecnv  10459  cvg1nlemcxze  10530  cvg1nlemres  10533  rexfiuz  10537  r19.29uz  10540  resqrexlem1arp  10553  resqrexlemfp1  10557  resqrexlemover  10558  resqrexlemdec  10559  resqrexlemdecn  10560  resqrexlemlo  10561  resqrexlemcalc1  10562  resqrexlemcalc2  10563  resqrexlemcalc3  10564  resqrexlemnmsq  10565  resqrexlemnm  10566  resqrexlemcvg  10567  resqrexlemglsq  10570  resqrexlemga  10571  resqrexlemsqa  10572  sqrtgt0  10582  sqrtsq  10592  absimle  10632  abstri  10652  cau3lem  10662  amgm2  10666  maxabsle  10752  maxabslemab  10754  maxabslemlub  10755  maxltsup  10766  max0addsup  10767  fimaxre2  10773  minabs  10782  bdtrilem  10785  bdtri  10786  xrmaxiflemcl  10788  xrmaxiflemcom  10792  xrmaxadd  10804  infxrnegsupex  10806  xrbdtri  10819  clim  10824  climshft  10847  climle  10877  clim2ser  10880  clim2ser2  10881  iserex  10882  isermulc2  10883  climrecvg1n  10891  climcvg1nlem  10892  climcaucn  10894  sumrbdclem  10919  fsum3cvg  10920  summodclem2a  10924  sum0  10931  fisumss  10935  fsumrecl  10944  fsumzcl  10945  fsumnn0cl  10946  fsumrpcl  10947  fsumadd  10949  fsumsplitf  10951  sumsnf  10952  sumpr  10956  sumtp  10957  isumclim3  10966  isumadd  10974  sumsplitdc  10975  fsum2dlemstep  10977  fisumcom2  10981  fsumcom  10982  fisum0diag  10984  fisum0diag2  10990  fsumneg  10994  fsumconst  10997  modfsummodlemstep  11000  modfsummod  11001  fsumge0  11002  fsumlessfi  11003  fsumabs  11008  fsumrelem  11014  iserabs  11018  fsumiun  11020  hash2iun1dif1  11023  binomlem  11026  isumshft  11033  isumnn0nn  11036  isumlessdc  11039  divcnv  11040  trireciplem  11043  trirecip  11044  expcnvap0  11045  expcnvre  11046  expcnv  11047  explecnv  11048  geosergap  11049  geoserap  11050  geolim  11054  georeclim  11056  geo2sum  11057  geo2sum2  11058  geo2lim  11059  geoisumr  11061  geoisum1  11062  geoisum1c  11063  0.999...  11064  geoihalfsum  11065  cvgratnnlembern  11066  cvgratnnlemnexp  11067  cvgratnnlemmn  11068  cvgratnnlemsumlt  11071  cvgratnnlemfm  11072  cvgratnnlemrate  11073  cvgratnn  11074  mertenslemi1  11078  mertenslem2  11079  mertensabs  11080  efcllemp  11097  efcllem  11098  ef0lem  11099  ege2le3  11110  efcj  11112  efgt0  11123  eftlub  11129  efsep  11130  ef4p  11133  efgt1p2  11134  efgt1p  11135  sinval  11142  cosval  11143  tanval2ap  11153  tanval3ap  11154  efi4p  11157  sinadd  11176  cosadd  11177  ef01bndlem  11196  sin01bnd  11197  cos01bnd  11198  sin01gt0  11201  eirraplem  11213  nndivdvds  11229  absdvdsb  11241  dvdsabsb  11242  dvds1  11281  dvdsfac  11288  zeneo  11298  odd2np1lem  11299  even2n  11301  oexpneg  11304  oddge22np1  11308  evennn02n  11309  evennn2n  11310  2tp1odd  11311  mulsucdiv2z  11312  ltoddhalfle  11320  halfleoddlt  11321  m1expo  11327  m1exp1  11328  nn0enne  11329  nn0ehalf  11330  nn0o1gt2  11332  nno  11333  nn0o  11334  nn0oddm1d2  11336  nnoddm1d2  11337  4dvdseven  11344  flodddiv4  11361  flodddiv4lt  11363  flodddiv4t2lthalf  11364  zsupcllemex  11369  zsupcl  11370  infssuzex  11372  infssuzcldc  11374  gcddvds  11382  zeqzmulgcd  11389  gcdcom  11392  gcdabs  11406  gcdabs1  11407  dfgcd3  11426  gcdass  11431  bezoutr1  11449  nn0seqcvgd  11450  alginv  11456  algcvg  11457  algcvga  11460  algfx  11461  eucalgcvga  11467  eucalg  11468  lcmval  11472  lcmcom  11473  lcmabs  11485  lcmass  11494  ncoprmgcdne1b  11498  cncongr1  11512  prmind2  11529  dvdsnprmd  11534  prmgt1  11540  oddprmge3  11543  coprm  11550  sqrt2irrlem  11567  sqrt2irr  11568  pw2dvdslemn  11570  pw2dvdseulemle  11572  oddpwdclemxy  11574  oddpwdclemodd  11577  oddpwdclemdc  11578  oddpwdc  11579  sqpweven  11580  2sqpwodd  11581  sqrt2irraplemnn  11584  sqrt2irrap  11585  divdenle  11602  nn0gcdsq  11605  numdensq  11607  nn0sqrtelqelz  11611  dfphi2  11623  phimullem  11628  oddennn  11632  evenennn  11633  unennn  11637  structcnvcnv  11659  strnfvn  11664  strndxid  11671  fvsetsid  11677  setsfun  11678  setsfun0  11679  setscom  11683  strslfvd  11684  strslfv2d  11685  strslfv2  11686  strslfv  11687  strslss  11690  setsslid  11693  setsslnid  11694  ressval2  11703  ressid  11704  strle1g  11733  strle2g  11734  strle3g  11735  2strbasg  11744  2stropg  11745  srngstrd  11765  lmodstrd  11776  ipsstrd  11784  istopon  11864  fiinbas  11899  baspartn  11900  eltg4i  11907  bastg  11913  unitg  11914  tgdom  11924  tgidm  11926  distop  11937  distopon  11939  epttop  11942  isopn3  11977  tgrest  12021  resttopon  12023  restin  12028  rest0  12031  lmfval  12044  cnfval  12046  cnpfval  12047  cnrest2  12087  cnrest2r  12088  cnptopresti  12089  cnptoprest  12090  cnptoprest2  12091  lmres  12099  blfvalps  12171  blgt0  12188  xblss2ps  12190  xblss2  12191  xmetec  12223  bdxmet  12287  bdmopn  12290  metrest  12292  tgioo  12322  elcncf1ii  12335  cncfmptid  12349  addccncf  12351  cdivcncfap  12352  negcncf  12353  expcncf  12357  limccl  12361  ellimc3ap  12362  limcdifap  12363  2spim  12384  bj-sbimeh  12390  bj-rspgt  12403  cbvrald  12405  bdsepnft  12495  bj-om  12549  bj-nntrans  12563  bj-nnelirr  12565  setindft  12577  nnsf  12609  peano4nninf  12610  peano3nninf  12611  nninfalllemn  12612  nninfsellemcl  12617  nninfself  12619  nninfsellemeq  12620  nninfsellemeqinf  12622  exmidsbthrlem  12626  qdencn  12629