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  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  enq0er  6417  enq0eceq  6419  nqnq0pi  6420  mulcanenq0ec  6427  nnnq0lem1  6428  addnq0mo  6429  mulnq0mo  6430  prarloclemlo  6476  prarloclem3  6479  genipv  6491  nqprrnd  6525  nqprdisj  6526  nqprloc  6527  1idprl  6565  1idpru  6566  recexprlemlol  6597  recexprlemupu  6599  cauappcvgprlemm  6616  cauappcvgprlemdisj  6622  cauappcvgprlemladdru  6627  cauappcvgprlemladdrl  6628  cauappcvgpr  6633  enreceq  6644  prsrlem1  6650  addsrmo  6651  mulsrmo  6652  0idsr  6675  pn0sr  6679  recexgt0sr  6681  archsr  6688  pitonnlem1p1  6722  axcnex  6725  axmulcl  6732  axmulass  6737  axdistr  6738  ax0id  6742  axprecex  6744  axpre-ltirr  6746  axpre-lttrn  6748  axpre-ltadd  6750  axpre-mulgt0  6751  axpre-mulext  6752  0cnd  6798  0red  6806  1red  6820  1cnd  6821  ltxrlt  6862  1p1times  6924  nfneg  6985  negsub  7035  pncan1  7151  npcan1  7152  kcnktkm1cn  7156  mulsubfacd  7191  rereim  7350  cru  7366  apreim  7367  mulreim  7368  apadd1  7372  apneg  7375  muleqadd  7411  eqneg  7470  mulgt1  7590  cju  7674  nn1suc  7694  2cnd  7748  avglt1  7920  avglt2  7921  add1p1  7931  sub1m1  7932  cnm2m1cnm3  7933  nn0p1gt0  7967  un0addcl  7971  nn0ge2m1nn  7998  0zd  8013  elnn0z  8014  elznn0  8016  1zzd  8028  peano2z  8037  ztri3or0  8043  zlelttric  8046  zltnle  8047  zmulcl  8053  zltp1le  8054  zgt0ge1  8058  elz2  8068  zdceq  8072  zdclt  8074  nn0lt2  8078  zneo  8095  nneo  8097  zeo2  8100  uzind  8105  uzind2  8106  nn0ind  8108  zadd2cl  8123  uzm1  8259  uzin  8261  uz3m2nn  8271  uzind4i  8291  eqreznegel  8305  nn01to3  8308  nn0ge2m1nnALT  8309  divfnzn  8312  cnref1o  8337  rpnegap  8370  ltxr  8445  xrre3  8485  ixxssixx  8521  elioc2  8555  elico2  8556  elicc2  8557  lincmb01cmp  8621  fzdcel  8654  ige3m2fz  8663  fz01en  8667  fzdifsuc  8693  elfz1b  8702  uzsplit  8704  fseq1p1m1  8706  elfzp1b  8709  ige2m1fz1  8721  ige2m1fz  8722  0elfz  8727  fz0tp  8731  fz0fzdiffz0  8737  nn0split  8744  fzoval  8755  fzouzsplit  8785  elfzom1elp1fzo  8808  elfzonlteqm1  8816  fzo0to3tp  8825  fzo0sn0fzo1  8827  fzosplitprm1  8840  frec2uzltd  8850  frec2uzlt2d  8851  frecuzrdgrrn  8855  frec2uzrdg  8856  frecfzennn  8864  iseqfveq2  8885  expivallem  8890  expival  8891  exp0  8893  exp1  8895  expp1  8896  expgt1  8927  ltexp2a  8940  leexp2a  8941  leexp2r  8942  exple1  8944  expubnd  8945  binom21  8996  zesq  9000  expnlbnd2  9007  sqeq0d  9013  imval  9058  crre  9065  crim  9066  remim  9068  cjreb  9074  readd  9077  remullem  9079  imadd  9085  cjadd  9092  cjreim  9111  cjreim2  9112  cjap  9114  cnrecnv  9118  sqrtsq  9194  2spim  9221  bj-sbimeh  9227  bj-rspgt  9240  cbvrald  9242  bdsepnft  9321  bj-om  9371  peano5set  9374  bj-nntrans  9385  bj-nnelirr  9387  setindft  9395
  Copyright terms: Public domain W3C validator