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  388  sylan2i  389  sylancl  394  sylancr  395  mpan  402  mpan2  403  mpani  408  mpan2i  409  anbi2i  433  anbi1i  434  nsyl3  544  mt2  556  mt2i  560  mto  575  mtoi  577  sylnib  588  simprimdc  744  con1biimdc  755  pm2.54dc  778  pm5.17dc  798  pm5.21nd  813  pm5.71dc  854  dedlema  862  dedlemb  863  a1tru  1242  dfbi3dc  1269  hbth  1328  dfexdc  1367  a17d  1397  nfvd  1399  nfan  1435  nfim  1442  19.21ht  1451  nfbi  1459  alrimd  1479  19.32dc  1547  equsexd  1595  spime  1607  equveli  1620  sbieh  1651  dvelimfALT2  1676  cbvald  1778  cbvexdh  1779  nfsbxy  1796  sbcomxyyz  1824  dvelimALT  1864  dvelimfv  1865  hbsb4t  1867  dvelimor  1872  eubii  1887  nfeudv  1893  nfmo  1898  mobii  1915  moimv  1944  2euswapdc  1969  eqidd  2019  syl5eq  2062  syl6eq  2066  syl5eqel  2102  syl5eleq  2104  syl6eqel  2106  syl6eleq  2108  nfcvd  2157  dvelimc  2176  nnedc  2189  necon1idc  2232  ralbii  2304  rexbii  2305  nfraldxy  2330  nfrexdxy  2331  nfralxy  2334  nfrexxy  2335  nfralya  2336  nfrexya  2337  rgenw  2350  ralimi  2358  rexim  2387  reximi  2390  rexlimivw  2403  r19.29af2  2426  r19.32vdc  2433  nfreudxy  2457  nfreuxy  2458  reubii  2469  rmobii  2474  ceqsralt  2554  vtoclgft  2577  rr19.28v  2656  reu8  2710  cdeqth  2724  nfsbc1d  2753  nfsbc1  2754  nfsbc  2757  sbcbii  2791  sbc2iegf  2801  sbc2iedv  2803  sbc3ie  2804  rmob  2823  sbcnel12g  2840  sbcne12g  2841  csbcomg  2846  csbeq2i  2849  nfcsb1  2854  nfcsb  2857  csbiebt  2859  csbief  2864  csbie2t  2867  sbcnestgf  2870  syl5ss  2929  syl6ss  2930  syl5sseqr  2967  syl6eqss  2968  difssd  3044  ssconb  3049  abvor0dc  3215  rabnc  3223  npss0  3239  nfif  3329  rexsnsOLD  3380  disjpr2  3404  tpid3g  3453  neldifsnd  3468  diftpsn3  3475  preq12bg  3514  intmin  3605  int0el  3615  dfiun2  3661  dfiin2  3662  dfiunv2  3663  iunrab  3674  iunid  3682  iun0  3683  iinrabm  3689  iunin1  3691  2iunin  3693  iinin1m  3696  syl5breq  3769  ssbri  3776  nfbr  3778  opabbii  3794  mpteq2i  3814  mpteq12i  3815  opth1  3943  copsexg  3951  copsex4g  3954  epelg  3997  issod  4026  trsucss  4106  bm2.5ii  4168  ordsucss  4176  onsucelsucr  4179  ordunisuc2r  4185  ordirr  4205  peano5  4244  finds1  4248  ordom  4252  0elnn  4263  csbcnvg  4442  dmxpinm  4479  dfiun3  4514  dfiin3  4515  dmcosseq  4526  resiun1  4553  resiun2  4554  resima2  4567  iss  4577  resiima  4606  relbrcnvg  4627  inimasn  4664  elxp4  4731  elxp5  4732  dfco2  4743  coiun  4753  relssdmrn  4764  unielrel  4768  relfld  4769  cnviinm  4782  cnvsom  4784  nfiotadxy  4793  nfiotaxy  4794  iota2df  4814  funssres  4864  fntp  4878  imadif  4901  imain  4903  sbcfng  4966  sbcfg  4967  fun  4984  fun11iun  5068  funcocnv2  5072  f1oprg  5089  sefvex  5117  tz6.12f  5123  dfimafn2  5144  fnsnfv  5153  ssimaex  5155  fvun1  5160  fvmptg  5169  fvmpt3i  5173  fvopab6  5185  fndmdifcom  5194  respreima  5216  fmptco  5251  fcoconst  5255  dfmpt  5261  fmptapd  5275  fmptpr  5276  isocnv2  5373  nfriotadxy  5396  nfriota  5397  riota2f  5409  nfov  5455  oprabbii  5479  mpt2eq123i  5487  ovmpt4g  5542  ovmpt2dxf  5545  ovmpt2x  5548  ovmpt2ga  5549  ovi3  5556  ov6g  5557  ovelrn  5568  caovcom  5577  caovass  5580  caovdi  5599  caovimo  5613  ofc12  5650  oprabex3  5675  reldm  5731  oprabco  5757  oprab2co  5758  mpt2xopoveq  5773  sprmpt2  5775  brtpos2  5784  reldmtpos  5786  dmtpos  5789  dftpos4  5796  tposfn2  5799  smores  5825  tfrlemisucfn  5855  tfrlemiubacc  5861  tfrlemi14  5865  frectfr  5896  frec0g  5898  oacl  5951  omcl  5952  oeicl  5953  oawordi  5960  nnsucelsuc  5981  nntri1  5985  nnaord  5989  nnmordi  5996  nnmord  5997  nnaordex  6007  nnm00  6009  swoer  6041  eqer  6045  0er  6047  uniqs  6071  xpiderm  6084  erinxp  6087  qliftf  6098  brecop  6103  ecopovtrn  6110  ecopover  6111  ecopoverg  6114  th3qlem1  6115  elni2  6168  enqeceq  6212  mulcanenqec  6239  enq0er  6284  enq0eceq  6286  nqnq0pi  6287  mulcanenq0ec  6294  nnnq0lem1  6295  addnq0mo  6296  mulnq0mo  6297  prarloclemlo  6342  prarloclem3  6345  genipv  6357  nqprrnd  6392  nqprdisj  6393  nqprloc  6394  1idprl  6423  1idpru  6424  recexprlemlol  6454  recexprlemupu  6456  enreceq  6477  prsrlem1  6483  addsrmo  6484  mulsrmo  6485  0idsr  6508  pn0sr  6512  recexsrlem  6514  axcnex  6549  axmulcl  6556  axmulass  6561  axdistr  6562  ax0id  6566  axpre-ltirr  6570  axpre-lttrn  6572  axpre-ltadd  6573  axpre-mulgt0  6574  0cnd  6616  0red  6624  1red  6638  1cnd  6639  ltxrlt  6680  1p1times  6734  nfneg  6795  negsub  6845  pncan1  6961  npcan1  6962  kcnktkm1cn  6966  mulsubfacd  7001  2spim  7152  bj-sbimeh  7158  bj-rspgt  7171  cbvrald  7173  bdsepnft  7252  bj-om  7298  peano5set  7301  bj-nntrans  7312  bj-nnelirr  7314  setindft  7322
  Copyright terms: Public domain W3C validator