ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  a1i Structured version   GIF 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  541  mt2  553  mt2i  557  mto  572  mtoi  574  sylnib  585  simprimdc  740  con1biimdc  751  pm2.54dc  774  pm5.17dc  794  pm5.21nd  809  pm5.71dc  850  dedlema  858  dedlemb  859  a1tru  1240  dfbi3dc  1267  hbth  1326  dfexdc  1364  a17d  1394  nfvd  1396  nfan  1431  nfim  1438  19.21ht  1447  nfbi  1455  alrimd  1475  19.32dc  1543  equsexd  1591  spime  1603  equveli  1616  sbieh  1647  dvelimfALT2  1672  cbvald  1774  cbvexdh  1775  nfsbxy  1792  sbcomxyyz  1820  dvelimALT  1860  dvelimfv  1861  hbsb4t  1863  dvelimor  1868  eubii  1883  nfeudv  1889  nfmo  1894  mobii  1911  moimv  1940  2euswapdc  1965  eqidd  2015  syl5eq  2058  syl6eq  2062  syl5eqel  2098  syl5eleq  2100  syl6eqel  2102  syl6eleq  2104  nfcvd  2153  dvelimc  2172  nnedc  2185  necon1idc  2228  ralbii  2300  rexbii  2301  nfraldxy  2326  nfrexdxy  2327  nfralxy  2330  nfrexxy  2331  nfralya  2332  nfrexya  2333  rgenw  2346  ralimi  2354  rexim  2383  reximi  2386  rexlimivw  2399  r19.29af2  2422  r19.32vdc  2429  nfreudxy  2453  nfreuxy  2454  reubii  2465  rmobii  2470  ceqsralt  2550  vtoclgft  2573  rr19.28v  2652  reu8  2706  cdeqth  2720  nfsbc1d  2749  nfsbc1  2750  nfsbc  2753  sbcbii  2787  sbc2iegf  2797  sbc2iedv  2799  sbc3ie  2800  rmob  2819  sbcnel12g  2836  sbcne12g  2837  csbcomg  2842  csbeq2i  2845  nfcsb1  2850  nfcsb  2853  csbiebt  2855  csbief  2860  csbie2t  2863  sbcnestgf  2866  syl5ss  2925  syl6ss  2926  syl5sseqr  2963  syl6eqss  2964  difssd  3040  ssconb  3045  abvor0dc  3211  rabnc  3219  npss0  3235  nfif  3323  rexsnsOLD  3374  disjpr2  3398  tpid3g  3447  neldifsnd  3462  diftpsn3  3469  preq12bg  3508  intmin  3599  int0el  3609  dfiun2  3655  dfiin2  3656  dfiunv2  3657  iunrab  3668  iunid  3676  iun0  3677  iinrabm  3683  iunin1  3685  2iunin  3687  iinin1m  3690  syl5breq  3763  ssbri  3770  nfbr  3772  opabbii  3788  mpteq2i  3808  mpteq12i  3809  opth1  3937  copsexg  3945  copsex4g  3948  epelg  3991  issod  4020  trsucss  4099  bm2.5ii  4161  ordsucss  4169  onsucelsucr  4172  ordunisuc2r  4178  ordirr  4198  peano5  4237  finds1  4241  ordom  4245  0elnn  4256  csbcnvg  4435  dmxpinm  4472  dfiun3  4507  dfiin3  4508  dmcosseq  4519  resiun1  4546  resiun2  4547  resima2  4560  iss  4570  resiima  4599  relbrcnvg  4620  inimasn  4657  elxp4  4724  elxp5  4725  dfco2  4736  coiun  4746  relssdmrn  4757  unielrel  4761  relfld  4762  cnviinm  4775  cnvsom  4777  nfiotadxy  4786  nfiotaxy  4787  iota2df  4807  funssres  4857  fntp  4871  imadif  4894  imain  4896  sbcfng  4959  sbcfg  4960  fun  4977  fun11iun  5061  funcocnv2  5065  f1oprg  5082  sefvex  5110  tz6.12f  5116  dfimafn2  5137  fnsnfv  5146  ssimaex  5148  fvun1  5153  fvmptg  5162  fvmpt3i  5166  fvopab6  5178  fndmdifcom  5187  respreima  5209  fmptco  5244  fcoconst  5248  dfmpt  5254  fmptapd  5268  fmptpr  5269  isocnv2  5366  nfriotadxy  5389  nfriota  5390  riota2f  5402  nfov  5448  oprabbii  5472  mpt2eq123i  5480  ovmpt4g  5535  ovmpt2dxf  5538  ovmpt2x  5541  ovmpt2ga  5542  ovi3  5549  ov6g  5550  ovelrn  5561  caovcom  5570  caovass  5573  caovdi  5592  caovimo  5606  ofc12  5643  oprabex3  5668  reldm  5724  oprabco  5750  oprab2co  5751  mpt2xopoveq  5766  sprmpt2  5768  brtpos2  5777  reldmtpos  5779  dmtpos  5782  dftpos4  5789  tposfn2  5792  smores  5818  tfrlemisucfn  5848  tfrlemiubacc  5854  tfrlemi14  5858  frectfr  5889  frec0g  5891  oacl  5944  omcl  5945  oeicl  5946  oawordi  5953  nnsucelsuc  5974  nntri1  5978  nnaord  5982  nnmordi  5989  nnmord  5990  nnaordex  6000  nnm00  6002  swoer  6034  eqer  6038  0er  6040  uniqs  6064  xpiderm  6077  erinxp  6080  qliftf  6091  brecop  6096  ecopovtrn  6103  ecopover  6104  ecopoverg  6107  th3qlem1  6108  elni2  6161  enqeceq  6205  mulcanenqec  6232  enq0er  6277  enq0eceq  6279  nqnq0pi  6280  mulcanenq0ec  6287  nnnq0lem1  6288  addnq0mo  6289  mulnq0mo  6290  prarloclemlo  6335  prarloclem3  6338  genipv  6350  nqprrnd  6385  nqprdisj  6386  nqprloc  6387  1idprl  6416  1idpru  6417  recexprlemlol  6448  recexprlemupu  6450  enreceq  6475  prsrlem1  6481  addsrmo  6482  mulsrmo  6483  0idsr  6506  pn0sr  6510  recexgt0sr  6512  axcnex  6551  axmulcl  6558  axmulass  6563  axdistr  6564  ax0id  6568  axprecex  6570  axpre-ltirr  6572  axpre-lttrn  6574  axpre-ltadd  6576  axpre-mulgt0  6577  axpre-mulext  6578  0cnd  6622  0red  6630  1red  6644  1cnd  6645  ltxrlt  6686  1p1times  6748  nfneg  6809  negsub  6859  pncan1  6975  npcan1  6976  kcnktkm1cn  6980  mulsubfacd  7015  rereim  7174  cru  7190  apreim  7191  mulreim  7192  apadd1  7196  apneg  7199  muleqadd  7235  eqneg  7294  mulgt1  7413  cju  7497  nn1suc  7517  2cnd  7571  avglt1  7742  avglt2  7743  add1p1  7753  sub1m1  7754  cnm2m1cnm3  7755  nn0p1gt0  7786  un0addcl  7790  nn0ge2m1nn  7817  0zd  7832  elnn0z  7833  elznn0  7835  1zzd  7847  peano2z  7855  ztri3or0  7861  zltnle  7864  zmulcl  7869  zltp1le  7870  zgt0ge1  7874  zdceq  7885  nn0lt2  7888  zneo  7905  nneo  7907  zeo2  7910  uzind  7915  uzind2  7916  nn0ind  7918  zadd2cl  7932  divfnzn  8040  rpnegap  8097  ltxr  8172  xrre3  8212  2spim  8243  bj-sbimeh  8249  bj-rspgt  8262  cbvrald  8264  bdsepnft  8343  bj-om  8393  peano5set  8396  bj-nntrans  8407  bj-nnelirr  8409  setindft  8417
  Copyright terms: Public domain W3C validator