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  2258  ralbii  2330  rexbii  2331  nfraldxy  2356  nfrexdxy  2357  nfralxy  2360  nfrexxy  2361  nfralya  2362  nfrexya  2363  rgenw  2376  ralimi  2384  rexim  2413  reximi  2416  rexlimivw  2429  r19.29af2  2452  r19.32vdc  2459  nfreudxy  2483  nfreuxy  2484  reubii  2495  rmobii  2500  ceqsralt  2581  vtoclgft  2604  rr19.28v  2683  reu8  2737  cdeqth  2751  nfsbc1d  2780  nfsbc1  2781  nfsbc  2784  sbcbii  2818  sbc2iegf  2828  sbc2iedv  2830  sbc3ie  2831  sbcrext  2835  rmob  2850  sbcnel12g  2867  sbcne12g  2868  csbcomg  2873  csbeq2i  2876  nfcsb1  2881  nfcsb  2884  csbiebt  2886  csbief  2891  csbie2t  2894  sbcnestgf  2897  syl5ss  2956  syl6ss  2957  syl5sseqr  2994  syl6eqss  2995  difssd  3071  ssconb  3076  abvor0dc  3242  rabnc  3250  npss0  3266  nfif  3356  rexsnsOLD  3410  disjpr2  3434  tpid3g  3483  neldifsnd  3498  diftpsn3  3505  preq12bg  3544  intmin  3635  int0el  3645  dfiun2  3691  dfiin2  3692  dfiunv2  3693  iunrab  3704  iunid  3712  iun0  3713  iinrabm  3719  iunin1  3721  2iunin  3723  iinin1m  3726  syl5breq  3799  ssbri  3806  nfbr  3808  opabbii  3824  mpteq2i  3844  mpteq12i  3845  opth1  3973  copsexg  3981  copsex4g  3984  epelg  4027  issod  4056  fr0  4088  frind  4089  trsucss  4160  bm2.5ii  4222  ordsucss  4230  onsucelsucr  4234  ordunisuc2r  4240  ordirr  4267  ordfr  4299  peano5  4321  finds1  4325  ordom  4329  0elnn  4340  csbcnvg  4519  dmxpinm  4556  dfiun3  4591  dfiin3  4592  dmcosseq  4603  resiun1  4630  resiun2  4631  resima2  4644  iss  4654  resiima  4683  relbrcnvg  4704  inimasn  4741  elxp4  4808  elxp5  4809  dfco2  4820  coiun  4830  relssdmrn  4841  unielrel  4845  relfld  4846  cnviinm  4859  cnvsom  4861  nfiotadxy  4870  nfiotaxy  4871  iota2df  4891  funssres  4942  fntp  4956  imadif  4979  imain  4981  sbcfng  5044  sbcfg  5045  fun  5063  fun11iun  5147  funcocnv2  5151  f1oprg  5168  sefvex  5196  tz6.12f  5202  dfimafn2  5223  fnsnfv  5232  ssimaex  5234  fvun1  5239  fvmptg  5248  fvmpt3i  5252  fvopab6  5264  fndmdifcom  5273  respreima  5295  fmptco  5330  fcoconst  5334  dfmpt  5340  fmptapd  5354  fmptpr  5355  isocnv2  5452  riotaexg  5472  nfriotadxy  5476  nfriota  5477  riota2f  5489  nfov  5535  oprabbii  5560  mpt2eq123i  5568  ovmpt4g  5623  ovmpt2dxf  5626  ovmpt2x  5629  ovmpt2ga  5630  ovi3  5637  ov6g  5638  ovelrn  5649  caovcom  5658  caovass  5661  caovdi  5680  caovimo  5694  ofc12  5731  oprabex3  5756  reldm  5812  oprabco  5838  oprab2co  5839  mpt2xopoveq  5855  sprmpt2  5857  brtpos2  5866  reldmtpos  5868  dmtpos  5871  dftpos4  5878  tposfn2  5881  smores  5907  tfrlemisucfn  5938  tfrlemiubacc  5944  tfri1  5951  frec0g  5983  frectfr  5985  oacl  6040  omcl  6041  oeicl  6042  oawordi  6049  nnsucelsuc  6070  nntri1  6074  nnsseleq  6079  nnaord  6082  nnmordi  6089  nnmord  6090  nnaordex  6100  nnm00  6102  swoer  6134  eqer  6138  0er  6140  uniqs  6164  xpiderm  6177  erinxp  6180  qliftf  6191  brecop  6196  ecopovtrn  6203  ecopover  6204  ecopoverg  6207  th3qlem1  6208  brdomg  6229  en2i  6250  en3i  6251  dom2  6255  dom3  6256  ener  6259  ensymb  6260  entr  6264  fundmen  6286  xpsnen  6295  xpassen  6304  nneneq  6320  phplem4dom  6324  phpelm  6328  phplem4on  6329  fidceq  6330  fiunsnnn  6338  ordiso2  6357  cardcl  6361  elni2  6412  indpi  6440  enqeceq  6457  mulcanenqec  6484  ltnnnq  6521  enq0er  6533  enq0eceq  6535  nqnq0pi  6536  mulcanenq0ec  6543  nnnq0lem1  6544  addnq0mo  6545  mulnq0mo  6546  prarloclemlo  6592  prarloclem3  6595  genipv  6607  nqprrnd  6641  nqprdisj  6642  nqprloc  6643  1idprl  6688  1idpru  6689  recexprlemlol  6724  recexprlemupu  6726  cauappcvgprlemm  6743  cauappcvgprlemdisj  6749  cauappcvgprlemladdru  6754  cauappcvgprlemladdrl  6755  cauappcvgpr  6760  caucvgprlemm  6766  caucvgprlemcl  6774  caucvgprlemladdrl  6776  caucvgpr  6780  caucvgprprlemmu  6793  caucvgprprlemopu  6797  caucvgprprlemclphr  6803  enreceq  6821  prsrlem1  6827  addsrmo  6828  mulsrmo  6829  0idsr  6852  pn0sr  6856  recexgt0sr  6858  archsr  6866  srpospr  6867  prsradd  6870  prsrlt  6871  caucvgsrlemfv  6875  caucvgsrlembound  6878  caucvgsrlemoffval  6880  caucvgsrlemoffcau  6882  caucvgsrlemoffgt1  6883  caucvgsrlemoffres  6884  caucvgsr  6886  pitonnlem1p1  6922  pitoregt0  6925  recidpirqlemcalc  6933  recidpirq  6934  axcnex  6935  axmulcl  6942  axmulass  6947  axdistr  6948  ax0id  6952  axprecex  6954  axpre-ltirr  6956  axpre-lttrn  6958  axpre-ltadd  6960  axpre-mulgt0  6961  axpre-mulext  6962  axcaucvglemval  6971  axcaucvg  6974  0cnd  7020  0red  7028  1red  7042  1cnd  7043  ltxrlt  7085  1p1times  7147  nfneg  7208  negsub  7259  pncan1  7375  npcan1  7376  kcnktkm1cn  7380  mulsubfacd  7415  rereim  7577  cru  7593  apreim  7594  mulreim  7595  apadd1  7599  apneg  7602  muleqadd  7649  eqneg  7708  mulgt1  7829  cju  7913  nn1suc  7933  2cnd  7988  avglt1  8163  avglt2  8164  add1p1  8174  sub1m1  8175  cnm2m1cnm3  8176  div4p1lem1div2  8177  nn0p1gt0  8211  un0addcl  8215  nn0ge2m1nn  8242  0zd  8257  elnn0z  8258  elznn0  8260  1zzd  8272  peano2z  8281  ztri3or0  8287  zlelttric  8290  zltnle  8291  zmulcl  8297  zltp1le  8298  zgt0ge1  8302  elz2  8312  zdceq  8316  zdclt  8318  nn0lt2  8322  zneo  8339  nneo  8341  zeo2  8344  uzind  8349  uzind2  8350  nn0ind  8352  zadd2cl  8367  uzm1  8503  uzin  8505  uz3m2nn  8515  uzind4i  8535  eqreznegel  8549  nn01to3  8552  nn0ge2m1nnALT  8553  divfnzn  8556  cnref1o  8582  rpnegap  8615  divlt1lt  8650  divle1le  8651  ltxr  8695  xrre3  8735  ixxssixx  8771  elioc2  8805  elico2  8806  elicc2  8807  lincmb01cmp  8871  fzdcel  8904  ige3m2fz  8913  fz01en  8917  fzdifsuc  8943  elfz1b  8952  uzsplit  8954  fseq1p1m1  8956  elfzp1b  8959  ige2m1fz1  8971  ige2m1fz  8972  0elfz  8977  fz0tp  8981  fz0fzdiffz0  8987  nn0split  8994  fzoval  9005  fzouzsplit  9035  elfzom1elp1fzo  9058  elfzonlteqm1  9066  fzo0to3tp  9075  fzo0sn0fzo1  9077  fzosplitprm1  9090  fvinim0ffz  9096  qlelttric  9100  qltnle  9101  qdceq  9102  qbtwnrelemcalc  9110  qbtwnre  9111  2tnp1ge0ge0  9143  flhalf  9144  fldiv4p1lem1div2  9147  intfracq  9162  frec2uzltd  9189  frec2uzlt2d  9190  frecuzrdgrrn  9194  frec2uzrdg  9195  frecfzennn  9203  iseqss  9226  iseqfveq2  9228  iseqshft2  9232  iserf  9233  iserfre  9234  monoord  9235  isermono  9237  iseqsplit  9238  iseqcaopr3  9240  iseradd  9243  isersub  9244  iseqid3s  9246  iseqhomo  9248  iser0  9250  iser0f  9251  serige0  9252  serile  9253  expivallem  9256  expival  9257  exp0  9259  exp1  9261  expp1  9262  expgt1  9293  ltexp2a  9306  leexp2a  9307  leexp2r  9308  exple1  9310  expubnd  9311  binom21  9363  zesq  9367  expnlbnd2  9374  sqeq0d  9380  shftuz  9418  ovshftex  9420  shftfn  9425  imval  9450  crre  9457  crim  9458  remim  9460  cjreb  9466  readd  9469  remullem  9471  imadd  9477  cjadd  9484  cjreim  9503  cjreim2  9504  cjap  9506  cnrecnv  9510  cvg1nlemcxze  9581  cvg1nlemres  9584  r19.29uz  9590  resqrexlem1arp  9603  resqrexlemf  9605  resqrexlemf1  9606  resqrexlemfp1  9607  resqrexlemover  9608  resqrexlemdec  9609  resqrexlemdecn  9610  resqrexlemlo  9611  resqrexlemcalc1  9612  resqrexlemcalc2  9613  resqrexlemcalc3  9614  resqrexlemnmsq  9615  resqrexlemnm  9616  resqrexlemcvg  9617  resqrexlemglsq  9620  resqrexlemga  9621  resqrexlemsqa  9622  sqrtgt0  9632  sqrtsq  9642  absimle  9680  abstri  9700  cau3lem  9710  amgm2  9714  clim  9802  climshft  9825  climle  9854  clim2iser  9857  clim2iser2  9858  iiserex  9859  iisermulc2  9860  iserile  9862  climserile  9865  climrecvg1n  9867  climcvg1nlem  9868  climcaucn  9870  serif0  9871  sqr2irrlem  9877  sqrt2irr  9878  nn0seqcvgd  9880  ialginv  9886  ialgcvg  9887  ialgcvga  9890  ialgfx  9891  2spim  9906  bj-sbimeh  9912  bj-rspgt  9925  cbvrald  9927  bdsepnft  10007  bj-om  10061  peano5setOLD  10065  bj-nntrans  10076  bj-nnelirr  10078  setindft  10090  qdencn  10123
  Copyright terms: Public domain W3C validator