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 44. (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  42  mpii  43  mpsyl  64  syl7  68  syl8  70  syl9  71  impbid21d  126  impbid1  140  mpbii  146  mpbiri  166  biidd  170  2th  172  syl5bb  190  syl6bb  194  imbi2i  224  jctil  305  jctir  306  sylani  398  sylan2i  399  sylancl  404  sylancr  405  mpan  415  mpan2  416  mpani  421  mpan2i  422  anbi2i  445  anbi1i  446  nsyl3  589  mt2  602  mt2i  606  mto  621  mtoi  623  sylnib  634  simprimdc  792  con1biimdc  803  pm2.54dc  826  pm5.17dc  846  pm5.21nd  861  pm5.71dc  905  dedlema  913  dedlemb  914  a1tru  1303  xorbi12i  1317  dfbi3dc  1331  hbth  1395  dfexdc  1433  a17d  1463  nfvd  1465  nfan  1500  nfim  1507  19.21ht  1516  nfbi  1524  alrimd  1544  19.32dc  1612  equsexd  1661  spime  1673  equveli  1686  sbieh  1717  dvelimfALT2  1742  cbvald  1845  cbvexdh  1846  nfsbxy  1863  sbcomxyyz  1891  dvelimALT  1931  dvelimfv  1932  hbsb4t  1934  dvelimor  1939  eubii  1954  nfeudv  1960  nfmo  1965  mobii  1982  moimv  2011  2euswapdc  2036  eqidd  2086  syl5eq  2129  syl6eq  2133  syl5eqel  2171  syl5eleq  2173  syl6eqel  2175  syl6eleq  2177  nfcvd  2226  dvelimc  2245  nnedc  2256  necon1idc  2304  ralbii  2380  rexbii  2381  nfraldxy  2406  nfrexdxy  2407  nfralxy  2410  nfrexxy  2411  nfralya  2412  nfrexya  2413  rgenw  2426  ralimi  2434  rexim  2463  reximi  2466  rexlimivw  2481  r19.29af2  2504  r19.32vdc  2512  nfreudxy  2536  nfreuxy  2537  reubii  2548  rmobii  2553  rabbii  2601  ceqsralt  2640  vtoclgft  2663  rr19.28v  2747  reu8  2802  cdeqth  2816  nfsbc1d  2845  nfsbc1  2846  nfsbc  2849  sbcbii  2887  sbc2iegf  2898  sbc2iedv  2900  sbc3ie  2901  sbcrext  2905  rmob  2920  sbcnel12g  2937  sbcne12g  2938  csbcomg  2943  csbeq2i  2946  nfcsb1  2951  nfcsb  2954  csbiebt  2956  csbief  2961  csbie2t  2965  sbcnestgf  2968  syl5ss  3025  syl6ss  3026  ssidd  3034  syl5sseqr  3064  syl6eqss  3065  difssd  3116  ssconb  3122  abvor0dc  3295  rabnc  3304  nfif  3405  disjpr2  3489  tpid3g  3538  neldifsnd  3554  diftpsn3  3561  preq12bg  3600  intmin  3691  int0el  3701  dfiun2  3747  dfiin2  3748  dfiunv2  3749  iunrab  3760  iunid  3768  iun0  3769  iinrabm  3775  iunin1  3777  2iunin  3779  iinin1m  3782  syl5breq  3855  ssbri  3862  nfbr  3864  opabbii  3880  mpteq2i  3900  mpteq12i  3901  opth1  4037  copsexg  4045  copsex4g  4048  epelg  4091  issod  4120  fr0  4152  frind  4153  trsucss  4224  bm2.5ii  4286  ordsucss  4294  onsucelsucr  4298  ordunisuc2r  4304  ordirr  4331  ordfr  4363  peano5  4386  finds1  4390  ordom  4394  0elnn  4405  omsinds  4408  csbcnvg  4588  dmxpinm  4625  dfiun3  4660  dfiin3  4661  dmcosseq  4672  resiun1  4699  resiun2  4700  resima2  4713  iss  4725  resiima  4757  relbrcnvg  4778  inimasn  4815  elxp4  4884  elxp5  4885  dfco2  4896  coiun  4906  relssdmrn  4917  unielrel  4924  relfld  4925  cnviinm  4938  cnvsom  4940  nfiotadxy  4949  nfiotaxy  4950  iota2df  4970  funssres  5021  fntp  5036  imadif  5059  imain  5061  sbcfng  5124  sbcfg  5125  fun  5147  fun11iun  5237  funcocnv2  5241  f1oprg  5258  sefvex  5289  tz6.12f  5296  dfimafn2  5317  fnsnfv  5326  ssimaex  5328  fvun1  5333  fvmptg  5343  fvmpt3i  5347  fvopab6  5359  fndmdifcom  5368  respreima  5390  fmptco  5427  fcoconst  5431  dfmpt  5437  fmptapd  5451  fmptpr  5452  isocnv2  5552  riotaexg  5573  nfriotadxy  5577  nfriota  5578  riota2f  5590  nfov  5636  oprabbii  5661  mpt2eq123i  5669  ovmpt4g  5724  ovmpt2dxf  5727  ovmpt2x  5730  ovmpt2ga  5731  ovi3  5738  ov6g  5739  ovelrn  5750  caovcom  5759  caovass  5762  caovdi  5781  caovimo  5795  ofc12  5832  oprabex3  5857  reldm  5913  oprabco  5939  oprab2co  5940  mpt2xopoveq  5959  sprmpt2  5961  brtpos2  5970  reldmtpos  5972  dmtpos  5975  dftpos4  5982  tposfn2  5985  smores  6011  tfrlemisucfn  6043  tfrlemiubacc  6049  tfri1dALT  6070  tfrcl  6083  tfri1  6084  rdgon  6105  frec0g  6116  frectfr  6119  freccllem  6121  frecfcllem  6123  frecsuclem  6125  oacl  6175  omcl  6176  oeicl  6177  oawordi  6184  nnsucelsuc  6206  nntri1  6211  nnsseleq  6216  nnaord  6220  nnmordi  6227  nnmord  6228  nnaordex  6238  nnm00  6240  swoer  6272  eqer  6276  0er  6278  uniqs  6302  xpiderm  6315  erinxp  6318  qliftf  6329  brecop  6334  ecopovtrn  6341  ecopover  6342  ecopoverg  6345  th3qlem1  6346  elpmg  6373  brdomg  6417  en2i  6439  en3i  6440  dom2  6444  dom3  6445  ener  6448  ensymb  6449  entr  6453  fundmen  6475  mapsnen  6480  map1  6481  xpsnen  6489  xpassen  6498  ssenen  6519  nneneq  6525  phplem4dom  6530  phpelm  6534  phplem4on  6535  fidceq  6537  fiunsnnn  6549  finexdc  6570  infm  6572  exmidpw  6576  unfidisj  6584  undifdc  6586  unfiin  6588  xpfi  6590  fisseneq  6592  ssfirab  6593  fnfi  6596  f1finf1o  6605  supubti  6638  suplubti  6639  cnvinfex  6657  eqinfti  6659  infvalti  6661  inflbti  6663  ordiso2  6672  djuex  6680  djuss  6705  1stinl  6709  2ndinl  6710  1stinr  6711  2ndinr  6712  updjudhcoinlf  6715  updjudhcoinrg  6716  casefun  6720  djufun  6728  finomni  6740  fodjuomnilemdc  6743  fodjuomnilemf  6744  fodjuomnilemm  6745  fodjuomnilem0  6746  nnnninf  6750  cardcl  6753  pm54.43  6762  en2other2  6766  exmidfodomrlemr  6772  exmidfodomrlemrALT  6773  elni2  6817  indpi  6845  enqeceq  6862  mulcanenqec  6889  ltnnnq  6926  enq0er  6938  enq0eceq  6940  nqnq0pi  6941  mulcanenq0ec  6948  nnnq0lem1  6949  addnq0mo  6950  mulnq0mo  6951  prarloclemlo  6997  prarloclem3  7000  genipv  7012  nqprrnd  7046  nqprdisj  7047  nqprloc  7048  1idprl  7093  1idpru  7094  recexprlemlol  7129  recexprlemupu  7131  cauappcvgprlemm  7148  cauappcvgprlemdisj  7154  cauappcvgprlemladdru  7159  cauappcvgprlemladdrl  7160  cauappcvgpr  7165  caucvgprlemm  7171  caucvgprlemcl  7179  caucvgprlemladdrl  7181  caucvgpr  7185  caucvgprprlemml  7197  caucvgprprlemmu  7198  caucvgprprlemopu  7202  caucvgprprlemclphr  7208  enreceq  7226  prsrlem1  7232  addsrmo  7233  mulsrmo  7234  0idsr  7257  pn0sr  7261  recexgt0sr  7263  archsr  7271  srpospr  7272  prsradd  7275  prsrlt  7276  caucvgsrlemfv  7280  caucvgsrlembound  7283  caucvgsrlemoffval  7285  caucvgsrlemoffcau  7287  caucvgsrlemoffgt1  7288  caucvgsrlemoffres  7289  caucvgsr  7291  pitonnlem1p1  7327  pitoregt0  7330  recidpirqlemcalc  7338  recidpirq  7339  axcnex  7340  axmulcl  7347  axmulass  7352  axdistr  7353  ax0id  7357  axprecex  7359  axpre-ltirr  7361  axpre-lttrn  7363  axpre-ltadd  7365  axpre-mulgt0  7366  axpre-mulext  7367  axcaucvglemval  7376  axcaucvg  7379  0cnd  7425  0red  7433  1red  7447  1cnd  7448  ltxrlt  7496  1p1times  7560  nfneg  7623  negsub  7674  addlsub  7792  pncan1  7799  npcan1  7800  negf1o  7804  kcnktkm1cn  7805  mulsubfacd  7840  rereim  8004  cru  8020  apreim  8021  mulreim  8022  apadd1  8026  apneg  8029  muleqadd  8076  eqneg  8138  mulgt1  8259  suprlubex  8348  negiso  8351  dfinfre  8352  cju  8356  nn1suc  8376  2cnd  8430  avglt1  8587  avglt2  8588  add1p1  8598  sub1m1  8599  cnm2m1cnm3  8600  xp1d2m1eqxm1d2  8601  div4p1lem1div2  8602  nn0p1gt0  8635  un0addcl  8639  nn0ge2m1nn  8666  0zd  8695  elnn0z  8696  elznn0  8698  1zzd  8710  peano2z  8719  ztri3or0  8725  zlelttric  8728  zltnle  8729  zmulcl  8736  zltp1le  8737  zgt0ge1  8741  elz2  8751  zdceq  8755  zdclt  8757  nn0lt2  8761  zneo  8780  nneo  8782  zeo2  8785  uzind  8790  uzind2  8791  nn0ind  8793  zadd2cl  8808  uzm1  8981  uzin  8983  uz3m2nn  8993  uzind4i  9012  infrenegsupex  9014  supminfex  9017  eqreznegel  9031  nn01to3  9034  nn0ge2m1nnALT  9035  divfnzn  9038  cnref1o  9065  rpnegap  9098  divlt1lt  9133  divle1le  9134  ltxr  9178  xrre3  9216  ixxssixx  9252  elioc2  9286  elico2  9287  elicc2  9288  lincmb01cmp  9352  fzdcel  9386  ige3m2fz  9395  fz01en  9399  fzdifsuc  9425  elfz1b  9434  uzsplit  9436  fseq1p1m1  9438  elfzp1b  9441  ige2m1fz1  9453  ige2m1fz  9454  0elfz  9460  fz0tp  9463  fz0fzdiffz0  9469  nn0split  9475  nnsplit  9476  fzoval  9487  fzouzsplit  9518  elfzom1elp1fzo  9541  elfzonlteqm1  9549  fzo0to3tp  9558  fzo0sn0fzo1  9560  fzosplitprm1  9573  fvinim0ffz  9580  qlelttric  9584  qltnle  9585  qdceq  9586  qbtwnrelemcalc  9595  qbtwnre  9596  ioo0  9599  ioom  9600  ico0  9601  ioc0  9602  2tnp1ge0ge0  9636  flhalf  9637  fldiv4p1lem1div2  9640  intfracq  9655  q0mod  9690  q1mod  9691  mulp1mod1  9700  modqnegd  9714  modsumfzodifsn  9731  frec2uzltd  9738  frec2uzlt2d  9739  frecfzennn  9761  1tonninf  9774  iseqvalcbv  9789  iseqfclt  9794  iseqclt  9798  iseqss  9800  iseqsst  9801  monoord  9810  iseqcaopr3  9815  iseqf1olemp  9836  iseradd  9839  isersub  9840  iseqid3s  9842  iseqhomo  9845  iseqz  9846  iser0  9848  serige0  9851  serile  9852  expival  9856  exp0  9858  expgt1  9892  ltexp2a  9906  leexp2a  9907  leexp2r  9908  exple1  9910  expubnd  9911  binom21  9964  zesq  9969  expnlbnd2  9976  sqeq0d  9982  sqoddm1div8  10003  expcanlem  10021  expcan  10022  nn0opthlem1d  10025  nn0opthlem2d  10026  faclbnd  10046  faclbnd2  10047  bc0k  10061  bcn1  10063  ibcval5  10068  bcn2  10069  bcn2m1  10074  bcn2p1  10075  fihashen1  10104  hashunlem  10109  1elfz0hash  10111  hashprg  10113  hashdifpr  10125  hashxp  10131  zfz1isolem1  10142  iseqcoll  10144  shftuz  10148  ovshftex  10150  shftfn  10155  imval  10180  crre  10187  crim  10188  remim  10190  cjreb  10196  readd  10199  remullem  10201  imadd  10207  cjadd  10214  cjreim  10233  cjreim2  10234  cjap  10236  cnrecnv  10240  cvg1nlemcxze  10311  cvg1nlemres  10314  rexfiuz  10318  r19.29uz  10321  resqrexlem1arp  10334  resqrexlemfp1  10338  resqrexlemover  10339  resqrexlemdec  10340  resqrexlemdecn  10341  resqrexlemlo  10342  resqrexlemcalc1  10343  resqrexlemcalc2  10344  resqrexlemcalc3  10345  resqrexlemnmsq  10346  resqrexlemnm  10347  resqrexlemcvg  10348  resqrexlemglsq  10351  resqrexlemga  10352  resqrexlemsqa  10353  sqrtgt0  10363  sqrtsq  10373  absimle  10413  abstri  10433  cau3lem  10443  amgm2  10447  maxabsle  10533  maxabslemab  10535  maxabslemlub  10536  maxltsup  10547  max0addsup  10548  fimaxre2  10553  clim  10564  climshft  10587  climle  10616  clim2iser  10619  clim2iser2  10620  iiserex  10621  iisermulc2  10622  iserile  10624  climserile  10627  climrecvg1n  10629  climcvg1nlem  10630  climcaucn  10632  isumrblem  10657  fisumcvg  10658  isummolem2a  10662  sum0  10668  fisumss  10672  nndivdvds  10684  absdvdsb  10696  dvdsabsb  10697  dvds1  10736  dvdsfac  10743  zeneo  10753  odd2np1lem  10754  even2n  10756  oexpneg  10759  oddge22np1  10763  evennn02n  10764  evennn2n  10765  2tp1odd  10766  mulsucdiv2z  10767  ltoddhalfle  10775  halfleoddlt  10776  m1expo  10782  m1exp1  10783  nn0enne  10784  nn0ehalf  10785  nn0o1gt2  10787  nno  10788  nn0o  10789  nn0oddm1d2  10791  nnoddm1d2  10792  4dvdseven  10799  flodddiv4  10816  flodddiv4lt  10818  flodddiv4t2lthalf  10819  zsupcllemex  10824  zsupcl  10825  infssuzex  10827  infssuzcldc  10829  gcddvds  10837  zeqzmulgcd  10844  gcdcom  10847  gcdabs  10861  gcdabs1  10862  dfgcd3  10881  gcdass  10886  bezoutr1  10904  nn0seqcvgd  10905  ialginv  10911  ialgcvg  10912  ialgcvga  10915  ialgfx  10916  eucialgcvga  10922  eucialg  10923  lcmval  10927  lcmcom  10928  lcmabs  10940  lcmass  10949  ncoprmgcdne1b  10953  cncongr1  10967  prmind2  10984  dvdsnprmd  10989  prmgt1  10995  oddprmge3  10998  coprm  11005  sqrt2irrlem  11022  sqrt2irr  11023  pw2dvdslemn  11025  pw2dvdseulemle  11027  oddpwdclemxy  11029  oddpwdclemodd  11032  oddpwdclemdc  11033  oddpwdc  11034  sqpweven  11035  2sqpwodd  11036  sqrt2irraplemnn  11039  sqrt2irrap  11040  divdenle  11057  nn0gcdsq  11060  numdensq  11062  nn0sqrtelqelz  11066  dfphi2  11078  phimullem  11083  oddennn  11087  evenennn  11088  unennn  11092  2spim  11112  bj-sbimeh  11118  bj-rspgt  11131  cbvrald  11133  bdsepnft  11223  bj-om  11277  bj-nntrans  11291  bj-nnelirr  11293  setindft  11305  nnsf  11340  peano4nninf  11341  peano3nninf  11342  nninfalllemn  11343  nninfsellemcl  11348  nninfself  11350  nninfsellemeq  11351  nninfsellemeqinf  11353  exmidsbthrlem  11357  qdencn  11360
  Copyright terms: Public domain W3C validator