ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  a1i Structured version   Unicode version

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 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 5 . 2
31, 2ax-mp 7 1
Colors of variables: wff set class
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  a1ii  24  syl6  29  mpdi  38  mpii  39  mpsyl  59  syl7  63  syl8  65  syl9  66  impbid21d  119  impbid1  130  mpbii  136  mpbiri  157  biidd  161  2th  163  syl5bb  181  syl6bb  185  imbi2i  215  jctil  295  jctir  296  sylani  386  sylan2i  387  sylancl  392  sylancr  393  mpan  400  mpan2  401  mpani  406  mpan2i  407  anbi2i  430  anbi1i  431  nsyl3  556  mt2  568  mt2i  572  mto  587  mtoi  589  sylnib  600  simprimdc  755  con1biimdc  766  pm2.54dc  789  pm5.17dc  809  pm5.21nd  824  pm5.71dc  867  dedlema  875  dedlemb  876  a1tru  1258  dfbi3dc  1285  hbth  1349  dfexdc  1387  a17d  1417  nfvd  1419  nfan  1454  nfim  1461  19.21ht  1470  nfbi  1478  alrimd  1498  19.32dc  1566  equsexd  1614  spime  1626  equveli  1639  sbieh  1670  dvelimfALT2  1695  cbvald  1797  cbvexdh  1798  nfsbxy  1815  sbcomxyyz  1843  dvelimALT  1883  dvelimfv  1884  hbsb4t  1886  dvelimor  1891  eubii  1906  nfeudv  1912  nfmo  1917  mobii  1934  moimv  1963  2euswapdc  1988  eqidd  2038  syl5eq  2081  syl6eq  2085  syl5eqel  2121  syl5eleq  2123  syl6eqel  2125  syl6eleq  2127  nfcvd  2176  dvelimc  2195  nnedc  2208  necon1idc  2252  ralbii  2324  rexbii  2325  nfraldxy  2350  nfrexdxy  2351  nfralxy  2354  nfrexxy  2355  nfralya  2356  nfrexya  2357  rgenw  2370  ralimi  2378  rexim  2407  reximi  2410  rexlimivw  2423  r19.29af2  2446  r19.32vdc  2453  nfreudxy  2477  nfreuxy  2478  reubii  2489  rmobii  2494  ceqsralt  2575  vtoclgft  2598  rr19.28v  2677  reu8  2731  cdeqth  2745  nfsbc1d  2774  nfsbc1  2775  nfsbc  2778  sbcbii  2812  sbc2iegf  2822  sbc2iedv  2824  sbc3ie  2825  rmob  2844  sbcnel12g  2861  sbcne12g  2862  csbcomg  2867  csbeq2i  2870  nfcsb1  2875  nfcsb  2878  csbiebt  2880  csbief  2885  csbie2t  2888  sbcnestgf  2891  syl5ss  2950  syl6ss  2951  syl5sseqr  2988  syl6eqss  2989  difssd  3065  ssconb  3070  abvor0dc  3236  rabnc  3244  npss0  3260  nfif  3350  rexsnsOLD  3401  disjpr2  3425  tpid3g  3474  neldifsnd  3489  diftpsn3  3496  preq12bg  3535  intmin  3626  int0el  3636  dfiun2  3682  dfiin2  3683  dfiunv2  3684  iunrab  3695  iunid  3703  iun0  3704  iinrabm  3710  iunin1  3712  2iunin  3714  iinin1m  3717  syl5breq  3790  ssbri  3797  nfbr  3799  opabbii  3815  mpteq2i  3835  mpteq12i  3836  opth1  3964  copsexg  3972  copsex4g  3975  epelg  4018  issod  4047  trsucss  4126  bm2.5ii  4188  ordsucss  4196  onsucelsucr  4199  ordunisuc2r  4205  ordirr  4225  peano5  4264  finds1  4268  ordom  4272  0elnn  4283  csbcnvg  4462  dmxpinm  4499  dfiun3  4534  dfiin3  4535  dmcosseq  4546  resiun1  4573  resiun2  4574  resima2  4587  iss  4597  resiima  4626  relbrcnvg  4647  inimasn  4684  elxp4  4751  elxp5  4752  dfco2  4763  coiun  4773  relssdmrn  4784  unielrel  4788  relfld  4789  cnviinm  4802  cnvsom  4804  nfiotadxy  4813  nfiotaxy  4814  iota2df  4834  funssres  4885  fntp  4899  imadif  4922  imain  4924  sbcfng  4987  sbcfg  4988  fun  5006  fun11iun  5090  funcocnv2  5094  f1oprg  5111  sefvex  5139  tz6.12f  5145  dfimafn2  5166  fnsnfv  5175  ssimaex  5177  fvun1  5182  fvmptg  5191  fvmpt3i  5195  fvopab6  5207  fndmdifcom  5216  respreima  5238  fmptco  5273  fcoconst  5277  dfmpt  5283  fmptapd  5297  fmptpr  5298  isocnv2  5395  riotaexg  5415  nfriotadxy  5419  nfriota  5420  riota2f  5432  nfov  5478  oprabbii  5502  mpt2eq123i  5510  ovmpt4g  5565  ovmpt2dxf  5568  ovmpt2x  5571  ovmpt2ga  5572  ovi3  5579  ov6g  5580  ovelrn  5591  caovcom  5600  caovass  5603  caovdi  5622  caovimo  5636  ofc12  5673  oprabex3  5698  reldm  5754  oprabco  5780  oprab2co  5781  mpt2xopoveq  5796  sprmpt2  5798  brtpos2  5807  reldmtpos  5809  dmtpos  5812  dftpos4  5819  tposfn2  5822  smores  5848  tfrlemisucfn  5879  tfrlemiubacc  5885  tfri1  5892  frec0g  5922  frectfr  5924  oacl  5979  omcl  5980  oeicl  5981  oawordi  5988  nnsucelsuc  6009  nntri1  6013  nnaord  6018  nnmordi  6025  nnmord  6026  nnaordex  6036  nnm00  6038  swoer  6070  eqer  6074  0er  6076  uniqs  6100  xpiderm  6113  erinxp  6116  qliftf  6127  brecop  6132  ecopovtrn  6139  ecopover  6140  ecopoverg  6143  th3qlem1  6144  brdomg  6165  en2i  6186  en3i  6187  dom2  6191  dom3  6192  ener  6195  ensymb  6196  entr  6200  fundmen  6222  xpsnen  6231  xpassen  6240  elni2  6298  indpi  6326  enqeceq  6343  mulcanenqec  6370  ltnnnq  6406  enq0er  6418  enq0eceq  6420  nqnq0pi  6421  mulcanenq0ec  6428  nnnq0lem1  6429  addnq0mo  6430  mulnq0mo  6431  prarloclemlo  6477  prarloclem3  6480  genipv  6492  nqprrnd  6526  nqprdisj  6527  nqprloc  6528  1idprl  6566  1idpru  6567  recexprlemlol  6598  recexprlemupu  6600  cauappcvgprlemm  6617  cauappcvgprlemdisj  6623  cauappcvgprlemladdru  6628  cauappcvgprlemladdrl  6629  cauappcvgpr  6634  caucvgprlemm  6639  caucvgprlemcl  6647  caucvgprlemladdrl  6649  caucvgpr  6653  enreceq  6664  prsrlem1  6670  addsrmo  6671  mulsrmo  6672  0idsr  6695  pn0sr  6699  recexgt0sr  6701  archsr  6708  pitonnlem1p1  6742  axcnex  6745  axmulcl  6752  axmulass  6757  axdistr  6758  ax0id  6762  axprecex  6764  axpre-ltirr  6766  axpre-lttrn  6768  axpre-ltadd  6770  axpre-mulgt0  6771  axpre-mulext  6772  0cnd  6818  0red  6826  1red  6840  1cnd  6841  ltxrlt  6882  1p1times  6944  nfneg  7005  negsub  7055  pncan1  7171  npcan1  7172  kcnktkm1cn  7176  mulsubfacd  7211  rereim  7370  cru  7386  apreim  7387  mulreim  7388  apadd1  7392  apneg  7395  muleqadd  7431  eqneg  7490  mulgt1  7610  cju  7694  nn1suc  7714  2cnd  7768  avglt1  7940  avglt2  7941  add1p1  7951  sub1m1  7952  cnm2m1cnm3  7953  nn0p1gt0  7987  un0addcl  7991  nn0ge2m1nn  8018  0zd  8033  elnn0z  8034  elznn0  8036  1zzd  8048  peano2z  8057  ztri3or0  8063  zlelttric  8066  zltnle  8067  zmulcl  8073  zltp1le  8074  zgt0ge1  8078  elz2  8088  zdceq  8092  zdclt  8094  nn0lt2  8098  zneo  8115  nneo  8117  zeo2  8120  uzind  8125  uzind2  8126  nn0ind  8128  zadd2cl  8143  uzm1  8279  uzin  8281  uz3m2nn  8291  uzind4i  8311  eqreznegel  8325  nn01to3  8328  nn0ge2m1nnALT  8329  divfnzn  8332  cnref1o  8357  rpnegap  8390  ltxr  8465  xrre3  8505  ixxssixx  8541  elioc2  8575  elico2  8576  elicc2  8577  lincmb01cmp  8641  fzdcel  8674  ige3m2fz  8683  fz01en  8687  fzdifsuc  8713  elfz1b  8722  uzsplit  8724  fseq1p1m1  8726  elfzp1b  8729  ige2m1fz1  8741  ige2m1fz  8742  0elfz  8747  fz0tp  8751  fz0fzdiffz0  8757  nn0split  8764  fzoval  8775  fzouzsplit  8805  elfzom1elp1fzo  8828  elfzonlteqm1  8836  fzo0to3tp  8845  fzo0sn0fzo1  8847  fzosplitprm1  8860  frec2uzltd  8870  frec2uzlt2d  8871  frecuzrdgrrn  8875  frec2uzrdg  8876  frecfzennn  8884  iseqfveq2  8905  expivallem  8910  expival  8911  exp0  8913  exp1  8915  expp1  8916  expgt1  8947  ltexp2a  8960  leexp2a  8961  leexp2r  8962  exple1  8964  expubnd  8965  binom21  9016  zesq  9020  expnlbnd2  9027  sqeq0d  9033  imval  9078  crre  9085  crim  9086  remim  9088  cjreb  9094  readd  9097  remullem  9099  imadd  9105  cjadd  9112  cjreim  9131  cjreim2  9132  cjap  9134  cnrecnv  9138  sqrtsq  9214  2spim  9241  bj-sbimeh  9247  bj-rspgt  9260  cbvrald  9262  bdsepnft  9342  bj-om  9396  peano5setOLD  9400  bj-nntrans  9411  bj-nnelirr  9413  setindft  9425
  Copyright terms: Public domain W3C validator