ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  a1i 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  2a1i  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  569  mt2i  573  mto  588  mtoi  590  sylnib  601  simprimdc  756  con1biimdc  767  pm2.54dc  790  pm5.17dc  810  pm5.21nd  825  pm5.71dc  868  dedlema  876  dedlemb  877  a1tru  1259  xorbi12i  1274  dfbi3dc  1288  hbth  1352  dfexdc  1390  a17d  1420  nfvd  1422  nfan  1457  nfim  1464  19.21ht  1473  nfbi  1481  alrimd  1501  19.32dc  1569  equsexd  1617  spime  1629  equveli  1642  sbieh  1673  dvelimfALT2  1698  cbvald  1800  cbvexdh  1801  nfsbxy  1818  sbcomxyyz  1846  dvelimALT  1886  dvelimfv  1887  hbsb4t  1889  dvelimor  1894  eubii  1909  nfeudv  1915  nfmo  1920  mobii  1937  moimv  1966  2euswapdc  1991  eqidd  2041  syl5eq  2084  syl6eq  2088  syl5eqel  2124  syl5eleq  2126  syl6eqel  2128  syl6eleq  2130  nfcvd  2179  dvelimc  2198  nnedc  2211  necon1idc  2255  ralbii  2327  rexbii  2328  nfraldxy  2353  nfrexdxy  2354  nfralxy  2357  nfrexxy  2358  nfralya  2359  nfrexya  2360  rgenw  2373  ralimi  2381  rexim  2410  reximi  2413  rexlimivw  2426  r19.29af2  2449  r19.32vdc  2456  nfreudxy  2480  nfreuxy  2481  reubii  2492  rmobii  2497  ceqsralt  2578  vtoclgft  2601  rr19.28v  2680  reu8  2734  cdeqth  2748  nfsbc1d  2777  nfsbc1  2778  nfsbc  2781  sbcbii  2815  sbc2iegf  2825  sbc2iedv  2827  sbc3ie  2828  sbcrext  2832  rmob  2847  sbcnel12g  2864  sbcne12g  2865  csbcomg  2870  csbeq2i  2873  nfcsb1  2878  nfcsb  2881  csbiebt  2883  csbief  2888  csbie2t  2891  sbcnestgf  2894  syl5ss  2953  syl6ss  2954  syl5sseqr  2991  syl6eqss  2992  difssd  3068  ssconb  3073  abvor0dc  3239  rabnc  3247  npss0  3263  nfif  3353  rexsnsOLD  3407  disjpr2  3431  tpid3g  3480  neldifsnd  3495  diftpsn3  3502  preq12bg  3541  intmin  3632  int0el  3642  dfiun2  3688  dfiin2  3689  dfiunv2  3690  iunrab  3701  iunid  3709  iun0  3710  iinrabm  3716  iunin1  3718  2iunin  3720  iinin1m  3723  syl5breq  3796  ssbri  3803  nfbr  3805  opabbii  3821  mpteq2i  3841  mpteq12i  3842  opth1  3970  copsexg  3978  copsex4g  3981  epelg  4024  issod  4053  fr0  4083  trsucss  4147  bm2.5ii  4209  ordsucss  4217  onsucelsucr  4221  ordunisuc2r  4227  ordirr  4252  peano5  4299  finds1  4303  ordom  4307  0elnn  4318  csbcnvg  4497  dmxpinm  4534  dfiun3  4569  dfiin3  4570  dmcosseq  4581  resiun1  4608  resiun2  4609  resima2  4622  iss  4632  resiima  4661  relbrcnvg  4682  inimasn  4719  elxp4  4786  elxp5  4787  dfco2  4798  coiun  4808  relssdmrn  4819  unielrel  4823  relfld  4824  cnviinm  4837  cnvsom  4839  nfiotadxy  4848  nfiotaxy  4849  iota2df  4869  funssres  4920  fntp  4934  imadif  4957  imain  4959  sbcfng  5022  sbcfg  5023  fun  5041  fun11iun  5125  funcocnv2  5129  f1oprg  5146  sefvex  5174  tz6.12f  5180  dfimafn2  5201  fnsnfv  5210  ssimaex  5212  fvun1  5217  fvmptg  5226  fvmpt3i  5230  fvopab6  5242  fndmdifcom  5251  respreima  5273  fmptco  5308  fcoconst  5312  dfmpt  5318  fmptapd  5332  fmptpr  5333  isocnv2  5430  riotaexg  5450  nfriotadxy  5454  nfriota  5455  riota2f  5467  nfov  5513  oprabbii  5538  mpt2eq123i  5546  ovmpt4g  5601  ovmpt2dxf  5604  ovmpt2x  5607  ovmpt2ga  5608  ovi3  5615  ov6g  5616  ovelrn  5627  caovcom  5636  caovass  5639  caovdi  5658  caovimo  5672  ofc12  5709  oprabex3  5734  reldm  5790  oprabco  5816  oprab2co  5817  mpt2xopoveq  5833  sprmpt2  5835  brtpos2  5844  reldmtpos  5846  dmtpos  5849  dftpos4  5856  tposfn2  5859  smores  5885  tfrlemisucfn  5916  tfrlemiubacc  5922  tfri1  5929  frec0g  5961  frectfr  5963  oacl  6018  omcl  6019  oeicl  6020  oawordi  6027  nnsucelsuc  6048  nntri1  6052  nnsseleq  6057  nnaord  6060  nnmordi  6067  nnmord  6068  nnaordex  6078  nnm00  6080  swoer  6112  eqer  6116  0er  6118  uniqs  6142  xpiderm  6155  erinxp  6158  qliftf  6169  brecop  6174  ecopovtrn  6181  ecopover  6182  ecopoverg  6185  th3qlem1  6186  brdomg  6207  en2i  6228  en3i  6229  dom2  6233  dom3  6234  ener  6237  ensymb  6238  entr  6242  fundmen  6264  xpsnen  6273  xpassen  6282  nneneq  6298  phplem4dom  6302  phpelm  6306  phplem4on  6307  fidceq  6308  fiunsnnn  6316  cardcl  6333  elni2  6384  indpi  6412  enqeceq  6429  mulcanenqec  6456  ltnnnq  6493  enq0er  6505  enq0eceq  6507  nqnq0pi  6508  mulcanenq0ec  6515  nnnq0lem1  6516  addnq0mo  6517  mulnq0mo  6518  prarloclemlo  6564  prarloclem3  6567  genipv  6579  nqprrnd  6613  nqprdisj  6614  nqprloc  6615  1idprl  6660  1idpru  6661  recexprlemlol  6696  recexprlemupu  6698  cauappcvgprlemm  6715  cauappcvgprlemdisj  6721  cauappcvgprlemladdru  6726  cauappcvgprlemladdrl  6727  cauappcvgpr  6732  caucvgprlemm  6738  caucvgprlemcl  6746  caucvgprlemladdrl  6748  caucvgpr  6752  caucvgprprlemmu  6765  caucvgprprlemopu  6769  caucvgprprlemclphr  6775  enreceq  6793  prsrlem1  6799  addsrmo  6800  mulsrmo  6801  0idsr  6824  pn0sr  6828  recexgt0sr  6830  archsr  6838  srpospr  6839  prsradd  6842  prsrlt  6843  caucvgsrlemfv  6847  caucvgsrlembound  6850  caucvgsrlemoffval  6852  caucvgsrlemoffcau  6854  caucvgsrlemoffgt1  6855  caucvgsrlemoffres  6856  caucvgsr  6858  pitonnlem1p1  6894  pitoregt0  6897  recidpirqlemcalc  6905  recidpirq  6906  axcnex  6907  axmulcl  6914  axmulass  6919  axdistr  6920  ax0id  6924  axprecex  6926  axpre-ltirr  6928  axpre-lttrn  6930  axpre-ltadd  6932  axpre-mulgt0  6933  axpre-mulext  6934  axcaucvglemval  6943  axcaucvg  6946  0cnd  6992  0red  7000  1red  7014  1cnd  7015  ltxrlt  7056  1p1times  7118  nfneg  7179  negsub  7229  pncan1  7345  npcan1  7346  kcnktkm1cn  7350  mulsubfacd  7385  rereim  7544  cru  7560  apreim  7561  mulreim  7562  apadd1  7566  apneg  7569  muleqadd  7616  eqneg  7675  mulgt1  7796  cju  7880  nn1suc  7900  2cnd  7955  avglt1  8127  avglt2  8128  add1p1  8138  sub1m1  8139  cnm2m1cnm3  8140  nn0p1gt0  8174  un0addcl  8178  nn0ge2m1nn  8205  0zd  8220  elnn0z  8221  elznn0  8223  1zzd  8235  peano2z  8244  ztri3or0  8250  zlelttric  8253  zltnle  8254  zmulcl  8260  zltp1le  8261  zgt0ge1  8265  elz2  8275  zdceq  8279  zdclt  8281  nn0lt2  8285  zneo  8302  nneo  8304  zeo2  8307  uzind  8312  uzind2  8313  nn0ind  8315  zadd2cl  8330  uzm1  8466  uzin  8468  uz3m2nn  8478  uzind4i  8498  eqreznegel  8512  nn01to3  8515  nn0ge2m1nnALT  8516  divfnzn  8519  cnref1o  8544  rpnegap  8577  ltxr  8653  xrre3  8693  ixxssixx  8729  elioc2  8763  elico2  8764  elicc2  8765  lincmb01cmp  8829  fzdcel  8862  ige3m2fz  8871  fz01en  8875  fzdifsuc  8901  elfz1b  8910  uzsplit  8912  fseq1p1m1  8914  elfzp1b  8917  ige2m1fz1  8929  ige2m1fz  8930  0elfz  8935  fz0tp  8939  fz0fzdiffz0  8945  nn0split  8952  fzoval  8963  fzouzsplit  8993  elfzom1elp1fzo  9016  elfzonlteqm1  9024  fzo0to3tp  9033  fzo0sn0fzo1  9035  fzosplitprm1  9048  frec2uzltd  9058  frec2uzlt2d  9059  frecuzrdgrrn  9063  frec2uzrdg  9064  frecfzennn  9072  iseqss  9095  iseqfveq2  9097  iseqshft2  9101  iserf  9102  iserfre  9103  monoord  9104  isermono  9106  iseqsplit  9107  iseqcaopr3  9109  iseradd  9112  isersub  9113  iseqid3s  9115  iseqhomo  9117  iser0  9119  iser0f  9120  serige0  9121  serile  9122  expivallem  9125  expival  9126  exp0  9128  exp1  9130  expp1  9131  expgt1  9162  ltexp2a  9175  leexp2a  9176  leexp2r  9177  exple1  9179  expubnd  9180  binom21  9232  zesq  9236  expnlbnd2  9243  sqeq0d  9249  shftuz  9287  ovshftex  9289  shftfn  9294  imval  9319  crre  9326  crim  9327  remim  9329  cjreb  9335  readd  9338  remullem  9340  imadd  9346  cjadd  9353  cjreim  9372  cjreim2  9373  cjap  9375  cnrecnv  9379  cvg1nlemcxze  9450  cvg1nlemres  9453  r19.29uz  9459  resqrexlem1arp  9472  resqrexlemf  9474  resqrexlemf1  9475  resqrexlemfp1  9476  resqrexlemover  9477  resqrexlemdec  9478  resqrexlemdecn  9479  resqrexlemlo  9480  resqrexlemcalc1  9481  resqrexlemcalc2  9482  resqrexlemcalc3  9483  resqrexlemnmsq  9484  resqrexlemnm  9485  resqrexlemcvg  9486  resqrexlemglsq  9489  resqrexlemga  9490  resqrexlemsqa  9491  sqrtgt0  9501  sqrtsq  9511  absimle  9549  abstri  9569  cau3lem  9579  amgm2  9583  clim  9670  climshft  9693  climle  9722  clim2iser  9725  clim2iser2  9726  iiserex  9727  iisermulc2  9728  iserile  9730  climserile  9733  climrecvg1n  9735  climcvg1nlem  9736  climcaucn  9738  serif0  9739  sqr2irrlem  9745  sqrt2irr  9746  nn0seqcvgd  9748  ialginv  9754  ialgcvg  9755  ialgcvga  9758  ialgfx  9759  2spim  9770  bj-sbimeh  9776  bj-rspgt  9789  cbvrald  9791  bdsepnft  9871  bj-om  9925  peano5setOLD  9929  bj-nntrans  9940  bj-nnelirr  9942  setindft  9954
  Copyright terms: Public domain W3C validator