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 45. (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  a1i13  24  2a1i  27  syl6  33  mpdi  43  mpii  44  mpsyl  65  syl7  69  syl8  71  syl9  72  impbid21d  127  impbid1  141  mpbii  147  mpbiri  167  biidd  171  2th  173  syl5bb  191  syl6bb  195  imbi2i  225  jca2  304  jctil  308  jctir  309  sylani  401  sylan2i  402  sylancl  407  sylancr  408  mpan  418  mpan2  419  mpani  424  mpan2i  425  anbi2i  450  anbi1i  451  nsyl3  598  mt2  612  mt2i  616  mto  634  mtoi  636  sylnib  648  simprimdc  825  con1biimdc  839  pm2.54dc  857  pm5.17dc  870  pm5.21nd  882  pm5.71dc  926  dedlema  934  dedlemb  935  a1tru  1328  xorbi12i  1342  dfbi3dc  1356  hbth  1420  dfexdc  1458  a17d  1488  nfvd  1490  nfan  1525  nfim  1532  19.21ht  1541  nfbi  1549  alrimd  1570  19.32dc  1638  equsexd  1688  spime  1700  equveli  1713  sbieh  1744  dvelimfALT2  1769  cbvald  1873  cbvexdh  1874  nfsbxy  1891  sbcomxyyz  1919  dvelimALT  1959  dvelimfv  1960  hbsb4t  1962  dvelimor  1967  eubii  1982  nfeudv  1988  nfmo  1993  mobii  2010  moimv  2039  2euswapdc  2064  eqidd  2114  syl5eq  2157  syl6eq  2161  syl5eqel  2199  syl5eleq  2201  syl6eqel  2203  syl6eleq  2205  nfcvd  2254  dvelimc  2274  nnedc  2285  necon1idc  2333  ralbii  2413  rexbii  2414  nfraldxy  2439  nfrexdxy  2440  nfralxy  2443  nfrexxy  2444  nfralya  2445  nfrexya  2446  rgenw  2459  ralimi  2467  rexim  2498  reximi  2501  rexlimivw  2517  r19.29af2  2544  r19.32vdc  2552  nfreudxy  2576  nfreuxy  2577  reubii  2588  rmobii  2593  rabbii  2641  ceqsralt  2682  vtoclgft  2705  rr19.28v  2792  reu8  2847  cdeqth  2863  nfsbc1d  2892  nfsbc1  2893  nfsbc  2896  sbcbii  2934  sbc2iegf  2945  sbc2iedv  2947  sbc3ie  2948  sbcrext  2952  rmob  2967  sbcnel12g  2984  sbcne12g  2985  csbcomg  2990  csbeq2i  2993  nfcsb1  2998  nfcsb  3001  csbiebt  3003  csbief  3008  csbie2t  3012  sbcnestgf  3015  syl5ss  3072  syl6ss  3073  ssidd  3082  sseqtrrid  3112  syl6eqss  3113  difssd  3167  ssconb  3173  abvor0dc  3350  rabnc  3359  nfif  3464  disjpr2  3551  tpid3g  3602  neldifsnd  3618  diftpsn3  3625  preq12bg  3664  intmin  3755  int0el  3765  dfiun2  3811  dfiin2  3812  dfiunv2  3813  iunrab  3824  iunid  3832  iun0  3833  iinrabm  3839  iunin1  3841  2iunin  3843  iinin1m  3846  breqtrid  3928  ssbri  3935  nfbr  3937  opabbii  3953  mpteq2i  3973  mpteq12i  3974  opth1  4116  copsexg  4124  copsex4g  4127  epelg  4170  issod  4199  fr0  4231  frind  4232  trsucss  4303  bm2.5ii  4370  ordsucss  4378  onsucelsucr  4382  ordunisuc2r  4388  ordirr  4415  ordfr  4447  peano5  4470  finds1  4474  ordom  4478  0elnn  4490  omsinds  4493  0nelrel  4543  csbcnvg  4681  dfiun3  4754  dfiin3  4755  dmcosseq  4766  resiun1  4794  resiun2  4795  resima2  4809  iss  4821  resiima  4853  relbrcnvg  4874  inimasn  4912  elxp4  4982  elxp5  4983  dfco2  4994  coiun  5004  relssdmrn  5015  unielrel  5022  relfld  5023  cnviinm  5036  cnvsom  5038  nfiotadxy  5047  nfiotaxy  5048  iota2df  5068  funssres  5121  fntp  5136  imadif  5159  imain  5161  sbcfng  5226  sbcfg  5227  fun  5251  fun11iun  5342  funcocnv2  5346  f1oprg  5363  sefvex  5394  tz6.12f  5402  dfimafn2  5423  fnsnfv  5432  ssimaex  5434  fvun1  5439  fvmptg  5449  fvmpt3i  5453  fvopab6  5469  fndmdifcom  5478  respreima  5500  fmptco  5538  fcoconst  5543  dfmpt  5549  fmptapd  5563  fmptpr  5564  isocnv2  5665  riotaexg  5686  nfriotadxy  5690  nfriota  5691  riota2f  5703  nfov  5753  oprabbii  5778  mpoeq123i  5786  ovmpt4g  5845  ovmpodxf  5848  ovmpox  5851  ovmpoga  5852  ovi3  5859  ov6g  5860  ovelrn  5871  caovcom  5880  caovass  5883  caovdi  5902  caovimo  5916  ofc12  5954  oprabex3  5979  reldm  6036  fnmpoovd  6064  oprabco  6066  oprab2co  6067  disjsnxp  6086  mpoxopoveq  6089  brtpos2  6100  reldmtpos  6102  dmtpos  6105  dftpos4  6112  tposfn2  6115  smores  6141  tfrlemisucfn  6173  tfrlemiubacc  6179  tfri1dALT  6200  tfrcl  6213  tfri1  6214  rdgon  6235  frec0g  6246  frectfr  6249  freccllem  6251  frecfcllem  6253  frecsuclem  6255  oacl  6308  omcl  6309  oeicl  6310  oawordi  6317  nnsucelsuc  6339  nntri1  6344  nnsseleq  6349  nnaord  6357  nnmordi  6364  nnmord  6365  nnaordex  6375  nnm00  6377  swoer  6409  eqer  6413  0er  6415  uniqs  6439  erinxp  6455  qliftf  6466  brecop  6471  ecopovtrn  6478  ecopover  6479  ecopoverg  6482  th3qlem1  6483  elpmg  6510  nfixpxy  6563  ixpintm  6571  ixpsnf1o  6582  brdomg  6594  en2i  6616  en3i  6617  dom2  6621  dom3  6622  ener  6625  ensymb  6626  entr  6630  fundmen  6652  mapsnen  6657  map1  6658  xpsnen  6666  xpassen  6675  ssenen  6696  nneneq  6702  phplem4dom  6707  phpelm  6711  phplem4on  6712  fidceq  6714  fiunsnnn  6726  finexdc  6747  infm  6749  exmidpw  6753  unfidisj  6761  undifdc  6763  unfiin  6765  fiintim  6768  xpfi  6769  fisseneq  6771  ssfirab  6772  fnfi  6775  iunfidisj  6784  f1finf1o  6785  fidcenumlemrk  6792  fidcenumlemr  6793  elfi2  6810  ssfii  6812  supubti  6836  suplubti  6837  cnvinfex  6855  eqinfti  6857  infvalti  6859  inflbti  6861  ordiso2  6870  djuex  6878  inl11  6900  djuss  6905  1stinl  6909  2ndinl  6910  1stinr  6911  2ndinr  6912  updjudhcoinlf  6915  updjudhcoinrg  6916  casefun  6920  caseinl  6926  caseinr  6927  omp1eomlem  6929  endjusym  6931  difinfsn  6935  djufun  6939  ctmlemr  6943  ctm  6944  ctssdclemn0  6945  ctssdccl  6946  ctssdc  6948  finomni  6960  fodjuomnilemdc  6964  fodjuf  6965  fodjum  6966  fodju0  6967  nnnninf  6971  ctssexmid  6972  omnimkv  6977  mkvprop  6979  cardcl  6984  pm54.43  6993  en2other2  6997  exmidfodomrlemr  7003  exmidfodomrlemrALT  7004  acfun  7008  exmidaclem  7009  endjudisj  7011  djuen  7012  djuassen  7018  xpdjuen  7019  elni2  7064  indpi  7092  enqeceq  7109  mulcanenqec  7136  ltnnnq  7173  enq0er  7185  enq0eceq  7187  nqnq0pi  7188  mulcanenq0ec  7195  nnnq0lem1  7196  addnq0mo  7197  mulnq0mo  7198  prarloclemlo  7244  prarloclem3  7247  genipv  7259  nqprrnd  7293  nqprdisj  7294  nqprloc  7295  1idprl  7340  1idpru  7341  recexprlemlol  7376  recexprlemupu  7378  cauappcvgprlemm  7395  cauappcvgprlemdisj  7401  cauappcvgprlemladdru  7406  cauappcvgprlemladdrl  7407  cauappcvgpr  7412  caucvgprlemm  7418  caucvgprlemcl  7426  caucvgprlemladdrl  7428  caucvgpr  7432  caucvgprprlemml  7444  caucvgprprlemmu  7445  caucvgprprlemopu  7449  caucvgprprlemclphr  7455  enreceq  7473  prsrlem1  7479  addsrmo  7480  mulsrmo  7481  0idsr  7504  pn0sr  7508  recexgt0sr  7510  archsr  7518  srpospr  7519  prsradd  7522  prsrlt  7523  caucvgsrlemfv  7527  caucvgsrlembound  7530  caucvgsrlemoffval  7532  caucvgsrlemoffcau  7534  caucvgsrlemoffgt1  7535  caucvgsrlemoffres  7536  caucvgsr  7538  pitonnlem1p1  7575  pitoregt0  7578  recidpirqlemcalc  7586  recidpirq  7587  axcnex  7588  axmulcl  7595  axmulass  7602  axdistr  7603  ax0id  7607  axprecex  7609  axpre-ltirr  7611  axpre-lttrn  7613  axpre-ltadd  7615  axpre-mulgt0  7616  axpre-mulext  7617  axcaucvglemval  7626  axcaucvg  7629  0cnd  7677  0red  7685  1red  7699  1cnd  7700  ltxrlt  7748  1p1times  7813  nfneg  7876  negsub  7927  addlsub  8045  pncan1  8052  npcan1  8053  negf1o  8057  kcnktkm1cn  8058  mulsubfacd  8093  rereim  8260  cru  8276  apreim  8277  mulreim  8278  apadd1  8282  apneg  8285  muleqadd  8336  eqneg  8399  mulgt1  8525  suprlubex  8614  negiso  8617  dfinfre  8618  sup3exmid  8619  cju  8623  nn1suc  8643  2cnd  8697  avglt1  8856  avglt2  8857  add1p1  8867  sub1m1  8868  cnm2m1cnm3  8869  xp1d2m1eqxm1d2  8870  div4p1lem1div2  8871  nn0p1gt0  8904  un0addcl  8908  nn0ge2m1nn  8935  0zd  8964  elnn0z  8965  elznn0  8967  1zzd  8979  peano2z  8988  ztri3or0  8994  zlelttric  8997  zltnle  8998  zmulcl  9005  zltp1le  9006  zgt0ge1  9010  elz2  9020  zdceq  9024  zdclt  9026  nn0lt2  9030  nn0le2is012  9031  zneo  9050  nneo  9052  zeo2  9055  uzind  9060  uzind2  9061  nn0ind  9063  zadd2cl  9078  uzm1  9252  uzin  9254  uz3m2nn  9264  uzind4i  9283  infrenegsupex  9285  supminfex  9288  eqreznegel  9302  nn01to3  9305  nn0ge2m1nnALT  9306  divfnzn  9309  cnref1o  9336  rpnegap  9369  divlt1lt  9404  divle1le  9405  ltxr  9449  xrre3  9492  xaddf  9514  xaddval  9515  xaddnemnf  9527  xaddnepnf  9528  xaddass2  9540  xltadd1  9546  xaddge0  9548  xlt2add  9550  xleaddadd  9557  ixxssixx  9572  elioc2  9606  elico2  9607  elicc2  9608  lincmb01cmp  9673  fzdcel  9707  ige3m2fz  9716  fz01en  9720  fzdifsuc  9748  elfz1b  9757  uzsplit  9759  fseq1p1m1  9761  elfzp1b  9764  ige2m1fz1  9776  ige2m1fz  9777  0elfz  9785  fz0tp  9788  fz0fzdiffz0  9794  nn0split  9800  nnsplit  9801  fzoval  9812  fzouzsplit  9843  elfzom1elp1fzo  9866  elfzonlteqm1  9874  fzo0to3tp  9883  fzo0sn0fzo1  9885  fzosplitprm1  9898  fvinim0ffz  9905  qlelttric  9909  qltnle  9910  qdceq  9911  qbtwnrelemcalc  9920  qbtwnre  9921  ioo0  9924  ioom  9925  ico0  9926  ioc0  9927  2tnp1ge0ge0  9961  flhalf  9962  fldiv4p1lem1div2  9965  intfracq  9980  q0mod  10015  q1mod  10016  mulp1mod1  10025  modqnegd  10039  modsumfzodifsn  10056  frec2uzltd  10063  frec2uzlt2d  10064  frecfzennn  10086  uzennn  10096  1tonninf  10100  iseqvalcbv  10117  seq3val  10118  seqvalcd  10119  seq3-1  10120  seqf  10121  seq3p1  10122  seqf2  10124  seq1cd  10125  seqp1cd  10126  seq3clss  10127  monoord  10136  seq3caopr3  10141  seq3f1olemp  10162  seq3id3  10167  seq3homo  10170  seq3z  10171  ser0  10174  ser3ge0  10177  exp0  10184  expgt1  10218  ltexp2a  10232  leexp2a  10233  leexp2r  10234  exple1  10236  expubnd  10237  binom21  10291  binom2sub1  10293  zesq  10297  expnlbnd2  10304  sqeq0d  10310  sqoddm1div8  10331  expcanlem  10349  expcan  10350  nn0opthlem1d  10353  nn0opthlem2d  10354  faclbnd  10374  faclbnd2  10375  bc0k  10389  bcn1  10391  bcn2  10397  bcn2m1  10402  bcn2p1  10403  fihashen1  10432  hashunlem  10437  1elfz0hash  10439  hashprg  10441  hashdifpr  10453  hashxp  10459  zfz1isolem1  10470  seq3coll  10472  shftuz  10476  ovshftex  10478  shftfn  10483  imval  10509  crre  10516  crim  10517  remim  10519  cjreb  10525  readd  10528  remullem  10530  imadd  10536  cjadd  10543  cjreim  10562  cjreim2  10563  cjap  10565  cnrecnv  10569  cvg1nlemcxze  10640  cvg1nlemres  10643  rexfiuz  10647  r19.29uz  10650  resqrexlem1arp  10663  resqrexlemfp1  10667  resqrexlemover  10668  resqrexlemdec  10669  resqrexlemdecn  10670  resqrexlemlo  10671  resqrexlemcalc1  10672  resqrexlemcalc2  10673  resqrexlemcalc3  10674  resqrexlemnmsq  10675  resqrexlemnm  10676  resqrexlemcvg  10677  resqrexlemglsq  10680  resqrexlemga  10681  resqrexlemsqa  10682  sqrtgt0  10692  sqrtsq  10702  absimle  10742  abstri  10762  cau3lem  10772  amgm2  10776  maxabsle  10862  maxabslemab  10864  maxabslemlub  10865  maxltsup  10876  max0addsup  10877  fimaxre2  10884  minabs  10893  bdtrilem  10896  bdtri  10897  xrmaxiflemcl  10900  xrmaxiflemcom  10904  xrmaxadd  10916  infxrnegsupex  10918  xrbdtri  10931  clim  10936  climshft  10959  climle  10989  clim2ser  10992  clim2ser2  10993  iserex  10994  isermulc2  10995  climrecvg1n  11003  climcvg1nlem  11004  climcaucn  11006  sumrbdclem  11031  fsum3cvg  11032  summodclem2a  11036  sum0  11043  fisumss  11047  fsumrecl  11056  fsumzcl  11057  fsumnn0cl  11058  fsumrpcl  11059  fsumadd  11061  fsumsplitf  11063  sumsnf  11064  sumpr  11068  sumtp  11069  isumclim3  11078  isumadd  11086  sumsplitdc  11087  fsum2dlemstep  11089  fisumcom2  11093  fsumcom  11094  fisum0diag  11096  fisum0diag2  11102  fsumneg  11106  fsumconst  11109  modfsummodlemstep  11112  modfsummod  11113  fsumge0  11114  fsumlessfi  11115  fsumabs  11120  fsumrelem  11126  iserabs  11130  fsumiun  11132  hash2iun1dif1  11135  binomlem  11138  isumshft  11145  isumnn0nn  11148  isumlessdc  11151  divcnv  11152  trireciplem  11155  trirecip  11156  expcnvap0  11157  expcnvre  11158  expcnv  11159  explecnv  11160  geosergap  11161  geoserap  11162  geolim  11166  georeclim  11168  geo2sum  11169  geo2sum2  11170  geo2lim  11171  geoisumr  11173  geoisum1  11174  geoisum1c  11175  0.999...  11176  geoihalfsum  11177  cvgratnnlembern  11178  cvgratnnlemnexp  11179  cvgratnnlemmn  11180  cvgratnnlemsumlt  11183  cvgratnnlemfm  11184  cvgratnnlemrate  11185  cvgratnn  11186  mertenslemi1  11190  mertenslem2  11191  mertensabs  11192  efcllemp  11209  efcllem  11210  ef0lem  11211  ege2le3  11222  efcj  11224  efgt0  11235  eftlub  11241  efsep  11242  ef4p  11245  efgt1p2  11246  efgt1p  11247  sinval  11254  cosval  11255  tanval2ap  11265  tanval3ap  11266  efi4p  11269  sinadd  11288  cosadd  11289  ef01bndlem  11308  sin01bnd  11309  cos01bnd  11310  sin01gt0  11313  eirraplem  11325  nndivdvds  11341  absdvdsb  11353  dvdsabsb  11354  dvds1  11393  dvdsfac  11400  zeneo  11410  odd2np1lem  11411  even2n  11413  oexpneg  11416  oddge22np1  11420  evennn02n  11421  evennn2n  11422  2tp1odd  11423  mulsucdiv2z  11424  ltoddhalfle  11432  halfleoddlt  11433  m1expo  11439  m1exp1  11440  nn0enne  11441  nn0ehalf  11442  nn0o1gt2  11444  nno  11445  nn0o  11446  nn0oddm1d2  11448  nnoddm1d2  11449  4dvdseven  11456  flodddiv4  11473  flodddiv4lt  11475  flodddiv4t2lthalf  11476  zsupcllemex  11481  zsupcl  11482  infssuzex  11484  infssuzcldc  11486  gcddvds  11494  zeqzmulgcd  11501  gcdcom  11504  gcdabs  11518  gcdabs1  11519  dfgcd3  11538  gcdass  11543  bezoutr1  11561  nn0seqcvgd  11562  alginv  11568  algcvg  11569  algcvga  11572  algfx  11573  eucalgcvga  11579  eucalg  11580  lcmval  11584  lcmcom  11585  lcmabs  11597  lcmass  11606  ncoprmgcdne1b  11610  cncongr1  11624  prmind2  11641  dvdsnprmd  11646  prmgt1  11652  oddprmge3  11655  coprm  11662  sqrt2irrlem  11679  sqrt2irr  11680  pw2dvdslemn  11682  pw2dvdseulemle  11684  oddpwdclemxy  11686  oddpwdclemodd  11689  oddpwdclemdc  11690  oddpwdc  11691  sqpweven  11692  2sqpwodd  11693  sqrt2irraplemnn  11696  sqrt2irrap  11697  divdenle  11714  nn0gcdsq  11717  numdensq  11719  nn0sqrtelqelz  11723  dfphi2  11735  phimullem  11740  oddennn  11744  evenennn  11745  unennn  11749  ennnfonelemj0  11753  ennnfonelemg  11755  ennnfonelemh  11756  ennnfonelemp1  11758  ennnfonelem1  11759  ennnfonelemhdmp1  11761  ennnfonelemss  11762  ennnfonelemkh  11764  ennnfonelemhf1o  11765  ennnfonelemex  11766  ennnfonelemhom  11767  ennnfonelemrn  11771  ennnfonelemnn0  11774  ctinfomlemom  11779  ctinf  11782  ctiunctlemuom  11786  ctiunct  11790  unct  11791  structcnvcnv  11812  strnfvn  11817  strndxid  11824  fvsetsid  11830  setsfun  11831  setsfun0  11832  setscom  11836  strslfvd  11837  strslfv2d  11838  strslfv2  11839  strslfv  11840  strslss  11843  setsslid  11846  setsslnid  11847  ressval2  11856  ressid  11857  strle1g  11886  strle2g  11887  strle3g  11888  2strbasg  11897  2stropg  11898  srngstrd  11918  lmodstrd  11929  ipsstrd  11937  istopon  12017  fiinbas  12053  baspartn  12054  eltg4i  12061  bastg  12067  unitg  12068  tgdom  12078  tgidm  12080  distop  12091  distopon  12093  epttop  12096  isopn3  12131  tgrest  12175  resttopon  12177  restin  12182  rest0  12185  lmfval  12198  cnfval  12200  cnpfval  12201  cnrest2  12241  cnrest2r  12242  cnptopresti  12243  cnptoprest  12244  cnptoprest2  12245  lmres  12253  txbasval  12272  tx1cn  12274  tx2cn  12275  txcnp  12276  txrest  12281  txdis1cn  12283  blfvalps  12368  blgt0  12385  xblss2ps  12387  xblss2  12388  xmetec  12420  bdxmet  12484  bdmopn  12487  metrest  12489  xmetxp  12490  txmetcnp  12501  tgioo  12526  divcnap  12535  fsumcncntop  12536  elcncf1ii  12547  cncfmptid  12563  addccncf  12566  cdivcncfap  12567  negcncf  12568  expcncf  12572  limccl  12578  ellimc3apf  12579  limcdifap  12581  limcmpted  12582  cnplimcim  12586  cnplimclemr  12588  limccnpcntop  12594  limccnp2lem  12595  limccnp2cntop  12596  reldvg  12597  dvfvalap  12599  dvidlemap  12609  dvcnp2cntop  12612  dvaddxx  12615  dviaddf  12616  2spim  12657  bj-sbimeh  12663  bj-rspgt  12676  cbvrald  12678  bdsepnft  12768  bj-om  12818  bj-nntrans  12832  bj-nnelirr  12834  setindft  12846  nnsf  12880  peano4nninf  12881  peano3nninf  12882  nninfalllemn  12883  nninfsellemcl  12888  nninfself  12890  nninfsellemeq  12891  nninfsellemeqinf  12893  nninffeq  12897  exmidsbthrlem  12898  qdencn  12903  isomninnlem  12906  cvgcmp2nlemabs  12908  cvgcmp2n  12909  trilpolemclim  12910  trilpolemcl  12911  trilpolemisumle  12912  trilpolemgt1  12913  trilpolemeq1  12914  trilpolemlt1  12915
  Copyright terms: Public domain W3C validator