NFE Home New Foundations Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  NFE Home  >  Th. List  >  a1i Unicode version

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
Assertion
Ref Expression
a1i

Proof of Theorem a1i
StepHypRef Expression
1 a1i.1 . 2
2 ax-1 6 . 2
31, 2ax-mp 5 1
Colors of variables: wff setvar class
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  2490  dvelimc  2510  ralbii  2638  rexbii  2639  nfral  2667  rgenw  2681  ralimi  2689  reximi  2721  rexlimivw  2734  nfreu  2785  nfrmo  2786  nfrab  2792  reubii  2797  rmobii  2802  ceqsralt  2882  vtoclgft  2905  rr19.28v  2981  reu8  3032  nfsbc1d  3063  nfsbc1  3064  nfsbc  3067  sbcbii  3101  sbcbiiOLD  3102  sbc2iegf  3112  sbc2iedv  3114  sbc3ie  3115  rmob  3134  sbcnel12g  3153  sbcne12g  3154  csbcomg  3159  csbeq2i  3162  nfcsb1  3167  nfcsb  3170  csbiebt  3172  csbief  3177  csbie2t  3180  sbcnestgf  3183  syl5ss  3283  syl6ss  3284  syl5sseqr  3320  syl6eqss  3321  difssd  3394  ssconb  3399  abvor0  3567  rabxm  3573  rabnc  3574  npss0  3589  pssdifcom1  3635  pssdifcom2  3636  nfif  3686  rexsns  3764  tpid3g  3831  neldifsnd  3842  diftpsn3  3849  ssunsn2  3865  intmin  3946  int0el  3957  dfiun2  4001  dfiin2  4002  iunrab  4013  iunid  4021  iun0  4022  iinrab  4028  iunin1  4031  2iunin  4034  iinin1  4037  preq12bg  4128  eqpw1uni  4330  nfiota  4343  reiotacl  4364  iota2df  4365  0nelsuc  4400  peano3  4404  peano5  4409  finds  4411  nncaddccl  4419  nnsucelr  4428  addcnul1  4452  preaddccan2  4455  ltfinirr  4457  leltfintr  4458  ltfintr  4459  lefinlteq  4463  ltfintri  4466  ltlefin  4468  ssfin  4470  vfinnc  4471  ncfinsn  4476  eqtfinrelk  4486  tfinltfinlem1  4500  evenoddnnnul  4514  evenodddisj  4516  nnadjoin  4520  tfinnn  4534  sfinltfin  4535  vfin1cltv  4547  0cnelphi  4597  phi011lem1  4598  proj1op  4600  proj2op  4601  copsexg  4607  opeq  4619  opabbii  4626  syl5breq  4674  ssbri  4681  nfbr  4683  dfid3  4768  dmcosseq  4973  ssreseq  4997  iss  5000  funssres  5144  funsn  5147  funsngOLD  5148  fnopab2  5208  fun  5236  fun11iun  5305  funbrfv2b  5362  dfimafn2  5367  fvun  5378  fvopab4t  5385  fvopab4g  5388  unpreima  5408  inpreima  5409  respreima  5410  fimacnv  5411  fnasrn  5417  ffvresb  5431  fconst5  5455  nfov  5545  oprabbii  5565  ov2ag  5598  ov3  5599  ov6g  5600  caovcom  5625  caovass  5627  caovdi  5634  mpteq2i  5660  mpt2eq123i  5664  mpteq12i  5665  fvmptss  5705  ovmpt4g  5710  fvmptss2  5725  composefn  5818  fnpw1fn  5853  pw1fnf1o  5855  dfnnc3  5885  clos1nrel  5886  frds  5935  weds  5938  po0  5939  connex0  5940  ider  5943  ssetpov  5944  erref  5959  eqer  5961  erdmrn  5965  erth  5968  erdisj  5972  uniqs  5984  mapsspm  6021  ener  6039  fundmen  6043  enadj  6060  enmap2lem2  6064  enmap1lem2  6070  enmap1  6074  enprmaplem2  6077  enprmaplem5  6080  enprmap  6082  nenpw1pwlem2  6085  elnc  6125  eqncg  6126  ncseqnc  6128  ncdisjun  6136  nnnc  6146  ncspw1eu  6159  eqtc  6161  elce  6175  sbthlem1  6203  lecponc  6213  leconnnc  6218  fntcfn  6245  addccan2nc  6265  ncslesuc  6267  nncdiv3  6277  nnc3n3p1  6278  fnspac  6283  spacis  6288  nchoicelem1  6289  nchoicelem6  6294  nchoicelem8  6296  nchoicelem9  6297  nchoicelem12  6300  fnfreclem2  6318  fnfreclem3  6319
  Copyright terms: Public domain W3C validator