Theorem a1i 10

Description: Inference derived from Axiom ax-1 6. See a1d 22 for an explanation of our informal use of the terms "inference" and "deduction." See also the comment in syld 40. (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 6	. 2 |- (ph -> (ps -> ph))
3	1, 2	ax-mp 5	1 |- (ps -> ph)

Syntax hints:   -> wi 4

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

This theorem is referenced by:  mp1i  11  imim2i  13  syl  15  mpi  16  idd  21  2a1i  24  syl6  29  mpdi  38  mpii  39  mpsyl  59  syl7  63  syl8  65  syl9  66  mt2i  110  nsyl3  111  mt3i  118  nsyl2  119  pm2.21i  123  mt4i  131  pm2.24i  136  pm2.61d1  151  pm2.61d2  152  mto  167  mtoi  169  mt2  170  impbid21d  182  impbid1  194  mpbii  202  mpbiri  224  biidd  228  2th  230  syl5bb  248  syl6bb  252  sylnib  295  imbi2i  303  olci  380  exmidd  405  jctil  523  jctir  524  sylani  635  sylan2i  636  sylancl  643  sylancr  644  mpan  651  mpan2  652  mpani  657  mpan2i  658  anbi2i  675  anbi1i  676  pm5.21nd  868  dedlema  920  dedlemb  921  a1tru  1330  ee02  1377  hadbi123i  1384  cadbi123i  1385  merco2  1501  hbth  1552  a17d  1617  nfvd  1620  exiftru  1657  exiftruOLD  1658  sptruw  1671  spfalwOLD  1699  hba1w  1707  ax11dgen  1722  ax11wdemo  1723  alrimd  1769  nfn  1793  nfim  1813  nfimOLD  1814  hbim  1817  19.23tOLD  1819  spimehOLD  1821  nfan  1824  nfbi  1834  nfnfOLD  1846  dvelimhw  1849  19.21tOLD  1863  dvelimh  1964  cbv3  1982  cbv3h  1983  dvelimf  1997  sbie  2038  sbco2  2086  sbcom2  2114  dvelimALT  2133  dvelimf-o  2180  ax10-16  2190  ax11eq  2193  ax11indalem  2197  ax11inda2ALT  2198  eujustALT  2207  eubii  2213  nfeu  2220  nfmo  2221  mobii  2240  morimv  2252  2euswap  2280  eqidd  2354  syl5eq  2397  syl6eq  2401  syl5eqel  2437  syl5eleq  2439  syl6eqel  2441  syl6eleq  2443  nfcvd  2491  dvelimc  2511  ralbii  2639  rexbii  2640  nfral  2668  rgenw  2682  ralimi  2690  reximi  2722  rexlimivw  2735  nfreu  2786  nfrmo  2787  nfrab  2793  reubii  2798  rmobii  2803  ceqsralt  2883  vtoclgft  2906  rr19.28v  2982  reu8  3033  nfsbc1d  3064  nfsbc1  3065  nfsbc  3068  sbcbii  3102  sbcbiiOLD  3103  sbc2iegf  3113  sbc2iedv  3115  sbc3ie  3116  rmob  3135  sbcnel12g  3154  sbcne12g  3155  csbcomg  3160  csbeq2i  3163  nfcsb1  3168  nfcsb  3171  csbiebt  3173  csbief  3178  csbie2t  3181  sbcnestgf  3184  syl5ss  3284  syl6ss  3285  syl5sseqr  3321  syl6eqss  3322  difssd  3395  ssconb  3400  abvor0  3568  rabxm  3574  rabnc  3575  npss0  3590  pssdifcom1  3636  pssdifcom2  3637  nfif  3687  rexsns  3765  tpid3g  3832  neldifsnd  3843  diftpsn3  3850  ssunsn2  3866  intmin  3947  int0el  3958  dfiun2  4002  dfiin2  4003  iunrab  4014  iunid  4022  iun0  4023  iinrab  4029  iunin1  4032  2iunin  4035  iinin1  4038  preq12bg  4129  eqpw1uni  4331  nfiota  4344  reiotacl  4365  iota2df  4366  0nelsuc  4401  peano3  4405  peano5  4410  finds  4412  nncaddccl  4420  nnsucelr  4429  addcnul1  4453  preaddccan2  4456  ltfinirr  4458  leltfintr  4459  ltfintr  4460  lefinlteq  4464  ltfintri  4467  ltlefin  4469  ssfin  4471  vfinnc  4472  ncfinsn  4477  eqtfinrelk  4487  tfinltfinlem1  4501  evenoddnnnul  4515  evenodddisj  4517  nnadjoin  4521  tfinnn  4535  sfinltfin  4536  vfin1cltv  4548  0cnelphi  4598  phi011lem1  4599  proj1op  4601  proj2op  4602  copsexg  4608  opeq  4620  opabbii  4627  syl5breq  4675  ssbri  4682  nfbr  4684  dfid3  4769  dmcosseq  4974  ssreseq  4998  iss  5001  funssres  5145  funsn  5148  funsngOLD  5149  fnopab2  5209  fun  5237  fun11iun  5306  funbrfv2b  5363  dfimafn2  5368  fvun  5379  fvopab4t  5386  fvopab4g  5389  unpreima  5409  inpreima  5410  respreima  5411  fimacnv  5412  fnasrn  5418  ffvresb  5432  fconst5  5456  nfov  5546  oprabbii  5566  ov2ag  5599  ov3  5600  ov6g  5601  caovcom  5626  caovass  5628  caovdi  5635  mpteq2i  5661  mpt2eq123i  5665  mpteq12i  5666  fvmptss  5706  ovmpt4g  5711  fvmptss2  5726  composefn  5819  fnpw1fn  5854  pw1fnf1o  5856  dfnnc3  5886  clos1nrel  5887  frds  5936  weds  5939  po0  5940  connex0  5941  ider  5944  ssetpov  5945  erref  5960  eqer  5962  erdmrn  5966  erth  5969  erdisj  5973  uniqs  5985  mapsspm  6022  ener  6040  fundmen  6044  enadj  6061  enmap2lem2  6065  enmap1lem2  6071  enmap1  6075  enprmaplem2  6078  enprmaplem5  6081  enprmap  6083  nenpw1pwlem2  6086  elnc  6126  eqncg  6127  ncseqnc  6129  ncdisjun  6137  nnnc  6147  ncspw1eu  6160  eqtc  6162  elce  6176  sbthlem1  6204  lecponc  6214  leconnnc  6219  fntcfn  6246  addccan2nc  6266  ncslesuc  6268  nncdiv3  6278  nnc3n3p1  6279  fnspac  6284  spacis  6289  nchoicelem1  6290  nchoicelem6  6295  nchoicelem8  6297  nchoicelem9  6298  nchoicelem12  6301  fnfreclem2  6319  fnfreclem3  6320