ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  a1i Unicode 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  |-  ph
Assertion
Ref Expression
a1i  |-  ( ps 
->  ph )

Proof of Theorem a1i
StepHypRef Expression
1 a1i.1 . 2  |-  ph
2 ax-1 5 . 2  |-  ( ph  ->  ( ps  ->  ph )
)
31, 2ax-mp 7 1  |-  ( ps 
->  ph )
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  63  syl7  67  syl8  69  syl9  70  impbid21d  123  impbid1  134  mpbii  140  mpbiri  161  biidd  165  2th  167  syl5bb  185  syl6bb  189  imbi2i  219  jctil  299  jctir  300  sylani  392  sylan2i  393  sylancl  398  sylancr  399  mpan  408  mpan2  409  mpani  414  mpan2i  415  anbi2i  438  anbi1i  439  nsyl3  564  mt2  577  mt2i  581  mto  596  mtoi  598  sylnib  609  simprimdc  765  con1biimdc  776  pm2.54dc  799  pm5.17dc  819  pm5.21nd  834  pm5.71dc  877  dedlema  885  dedlemb  886  a1tru  1273  xorbi12i  1288  dfbi3dc  1302  hbth  1366  dfexdc  1404  a17d  1434  nfvd  1436  nfan  1471  nfim  1478  19.21ht  1487  nfbi  1495  alrimd  1515  19.32dc  1583  equsexd  1631  spime  1643  equveli  1656  sbieh  1687  dvelimfALT2  1712  cbvald  1814  cbvexdh  1815  nfsbxy  1832  sbcomxyyz  1860  dvelimALT  1900  dvelimfv  1901  hbsb4t  1903  dvelimor  1908  eubii  1923  nfeudv  1929  nfmo  1934  mobii  1951  moimv  1980  2euswapdc  2005  eqidd  2055  syl5eq  2098  syl6eq  2102  syl5eqel  2138  syl5eleq  2140  syl6eqel  2142  syl6eleq  2144  nfcvd  2193  dvelimc  2212  nnedc  2223  necon1idc  2271  ralbii  2345  rexbii  2346  nfraldxy  2371  nfrexdxy  2372  nfralxy  2375  nfrexxy  2376  nfralya  2377  nfrexya  2378  rgenw  2391  ralimi  2399  rexim  2428  reximi  2431  rexlimivw  2444  r19.29af2  2467  r19.32vdc  2474  nfreudxy  2498  nfreuxy  2499  reubii  2510  rmobii  2515  ceqsralt  2596  vtoclgft  2619  rr19.28v  2703  reu8  2757  cdeqth  2771  nfsbc1d  2800  nfsbc1  2801  nfsbc  2804  sbcbii  2842  sbc2iegf  2853  sbc2iedv  2855  sbc3ie  2856  sbcrext  2860  rmob  2875  sbcnel12g  2892  sbcne12g  2893  csbcomg  2898  csbeq2i  2901  nfcsb1  2906  nfcsb  2909  csbiebt  2911  csbief  2916  csbie2t  2919  sbcnestgf  2922  syl5ss  2981  syl6ss  2982  syl5sseqr  3019  syl6eqss  3020  difssd  3096  ssconb  3101  abvor0dc  3267  rabnc  3275  npss0  3291  nfif  3381  rexsnsOLD  3435  disjpr2  3459  tpid3g  3508  neldifsnd  3523  diftpsn3  3530  preq12bg  3569  intmin  3660  int0el  3670  dfiun2  3716  dfiin2  3717  dfiunv2  3718  iunrab  3729  iunid  3737  iun0  3738  iinrabm  3744  iunin1  3746  2iunin  3748  iinin1m  3751  syl5breq  3824  ssbri  3831  nfbr  3833  opabbii  3849  mpteq2i  3869  mpteq12i  3870  opth1  3998  copsexg  4006  copsex4g  4009  epelg  4052  issod  4081  fr0  4113  frind  4114  trsucss  4185  bm2.5ii  4247  ordsucss  4255  onsucelsucr  4259  ordunisuc2r  4265  ordirr  4292  ordfr  4324  peano5  4346  finds1  4350  ordom  4354  0elnn  4365  csbcnvg  4544  dmxpinm  4581  dfiun3  4616  dfiin3  4617  dmcosseq  4628  resiun1  4655  resiun2  4656  resima2  4669  iss  4679  resiima  4708  relbrcnvg  4729  inimasn  4766  elxp4  4833  elxp5  4834  dfco2  4845  coiun  4855  relssdmrn  4866  unielrel  4870  relfld  4871  cnviinm  4884  cnvsom  4886  nfiotadxy  4895  nfiotaxy  4896  iota2df  4916  funssres  4967  fntp  4981  imadif  5004  imain  5006  sbcfng  5069  sbcfg  5070  fun  5088  fun11iun  5172  funcocnv2  5176  f1oprg  5193  sefvex  5221  tz6.12f  5227  dfimafn2  5248  fnsnfv  5257  ssimaex  5259  fvun1  5264  fvmptg  5273  fvmpt3i  5277  fvopab6  5289  fndmdifcom  5298  respreima  5320  fmptco  5355  fcoconst  5359  dfmpt  5365  fmptapd  5379  fmptpr  5380  isocnv2  5477  riotaexg  5497  nfriotadxy  5501  nfriota  5502  riota2f  5514  nfov  5560  oprabbii  5585  mpt2eq123i  5593  ovmpt4g  5648  ovmpt2dxf  5651  ovmpt2x  5654  ovmpt2ga  5655  ovi3  5662  ov6g  5663  ovelrn  5674  caovcom  5683  caovass  5686  caovdi  5705  caovimo  5719  ofc12  5756  oprabex3  5781  reldm  5837  oprabco  5863  oprab2co  5864  mpt2xopoveq  5883  sprmpt2  5885  brtpos2  5894  reldmtpos  5896  dmtpos  5899  dftpos4  5906  tposfn2  5909  smores  5935  tfrlemisucfn  5966  tfrlemiubacc  5972  tfri1  5979  frec0g  6011  frectfr  6013  oacl  6068  omcl  6069  oeicl  6070  oawordi  6077  nnsucelsuc  6098  nntri1  6102  nnsseleq  6107  nnaord  6110  nnmordi  6117  nnmord  6118  nnaordex  6128  nnm00  6130  swoer  6162  eqer  6166  0er  6168  uniqs  6192  xpiderm  6205  erinxp  6208  qliftf  6219  brecop  6224  ecopovtrn  6231  ecopover  6232  ecopoverg  6235  th3qlem1  6236  brdomg  6257  en2i  6278  en3i  6279  dom2  6283  dom3  6284  ener  6287  ensymb  6288  entr  6292  fundmen  6314  xpsnen  6323  xpassen  6332  nneneq  6348  phplem4dom  6352  phpelm  6356  phplem4on  6357  fidceq  6358  fiunsnnn  6366  ordiso2  6385  cardcl  6389  elni2  6440  indpi  6468  enqeceq  6485  mulcanenqec  6512  ltnnnq  6549  enq0er  6561  enq0eceq  6563  nqnq0pi  6564  mulcanenq0ec  6571  nnnq0lem1  6572  addnq0mo  6573  mulnq0mo  6574  prarloclemlo  6620  prarloclem3  6623  genipv  6635  nqprrnd  6669  nqprdisj  6670  nqprloc  6671  1idprl  6716  1idpru  6717  recexprlemlol  6752  recexprlemupu  6754  cauappcvgprlemm  6771  cauappcvgprlemdisj  6777  cauappcvgprlemladdru  6782  cauappcvgprlemladdrl  6783  cauappcvgpr  6788  caucvgprlemm  6794  caucvgprlemcl  6802  caucvgprlemladdrl  6804  caucvgpr  6808  caucvgprprlemmu  6821  caucvgprprlemopu  6825  caucvgprprlemclphr  6831  enreceq  6849  prsrlem1  6855  addsrmo  6856  mulsrmo  6857  0idsr  6880  pn0sr  6884  recexgt0sr  6886  archsr  6894  srpospr  6895  prsradd  6898  prsrlt  6899  caucvgsrlemfv  6903  caucvgsrlembound  6906  caucvgsrlemoffval  6908  caucvgsrlemoffcau  6910  caucvgsrlemoffgt1  6911  caucvgsrlemoffres  6912  caucvgsr  6914  pitonnlem1p1  6950  pitoregt0  6953  recidpirqlemcalc  6961  recidpirq  6962  axcnex  6963  axmulcl  6970  axmulass  6975  axdistr  6976  ax0id  6980  axprecex  6982  axpre-ltirr  6984  axpre-lttrn  6986  axpre-ltadd  6988  axpre-mulgt0  6989  axpre-mulext  6990  axcaucvglemval  6999  axcaucvg  7002  0cnd  7048  0red  7056  1red  7070  1cnd  7071  ltxrlt  7114  1p1times  7178  nfneg  7241  negsub  7292  addlsub  7410  pncan1  7417  npcan1  7418  kcnktkm1cn  7422  mulsubfacd  7457  rereim  7621  cru  7637  apreim  7638  mulreim  7639  apadd1  7643  apneg  7646  muleqadd  7693  eqneg  7753  mulgt1  7874  cju  7959  nn1suc  7979  2cnd  8033  avglt1  8190  avglt2  8191  add1p1  8201  sub1m1  8202  cnm2m1cnm3  8203  xp1d2m1eqxm1d2  8204  div4p1lem1div2  8205  nn0p1gt0  8238  un0addcl  8242  nn0ge2m1nn  8269  0zd  8284  elnn0z  8285  elznn0  8287  1zzd  8299  peano2z  8308  ztri3or0  8314  zlelttric  8317  zltnle  8318  zmulcl  8325  zltp1le  8326  zgt0ge1  8330  elz2  8340  zdceq  8344  zdclt  8346  nn0lt2  8350  zneo  8368  nneo  8370  zeo2  8373  uzind  8378  uzind2  8379  nn0ind  8381  zadd2cl  8396  uzm1  8569  uzin  8571  uz3m2nn  8581  uzind4i  8601  eqreznegel  8616  nn01to3  8619  nn0ge2m1nnALT  8620  divfnzn  8623  cnref1o  8650  rpnegap  8683  divlt1lt  8718  divle1le  8719  ltxr  8766  xrre3  8806  ixxssixx  8842  elioc2  8876  elico2  8877  elicc2  8878  lincmb01cmp  8942  fzdcel  8976  ige3m2fz  8985  fz01en  8989  fzdifsuc  9015  elfz1b  9024  uzsplit  9026  fseq1p1m1  9028  elfzp1b  9031  ige2m1fz1  9043  ige2m1fz  9044  0elfz  9049  fz0tp  9053  fz0fzdiffz0  9059  nn0split  9066  fzoval  9077  fzouzsplit  9107  elfzom1elp1fzo  9130  elfzonlteqm1  9138  fzo0to3tp  9147  fzo0sn0fzo1  9149  fzosplitprm1  9162  fvinim0ffz  9168  qlelttric  9172  qltnle  9173  qdceq  9174  qbtwnrelemcalc  9182  qbtwnre  9183  2tnp1ge0ge0  9216  flhalf  9217  fldiv4p1lem1div2  9220  intfracq  9235  q0mod  9270  q1mod  9271  mulp1mod1  9280  modqnegd  9294  modsumfzodifsn  9311  frec2uzltd  9318  frec2uzlt2d  9319  frecuzrdgrrn  9323  frec2uzrdg  9324  frecfzennn  9332  iseqss  9355  iseqfveq2  9357  iseqshft2  9361  iserf  9362  iserfre  9363  monoord  9364  isermono  9366  iseqsplit  9367  iseqcaopr3  9369  iseradd  9372  isersub  9373  iseqid3s  9375  iseqhomo  9377  iseqz  9378  iser0  9380  iser0f  9381  serige0  9382  serile  9383  expivallem  9386  expival  9387  exp0  9389  exp1  9391  expp1  9392  expgt1  9423  ltexp2a  9437  leexp2a  9438  leexp2r  9439  exple1  9441  expubnd  9442  binom21  9494  zesq  9499  expnlbnd2  9506  sqeq0d  9512  sqoddm1div8  9533  nn0opthlem1d  9552  nn0opthlem2d  9553  facnn  9559  fac0  9560  fac1  9561  facp1  9562  faclbnd  9573  faclbnd2  9574  bc0k  9588  bcn1  9590  ibcval5  9595  bcn2  9596  bcn2m1  9601  bcn2p1  9602  shftuz  9610  ovshftex  9612  shftfn  9617  imval  9642  crre  9649  crim  9650  remim  9652  cjreb  9658  readd  9661  remullem  9663  imadd  9669  cjadd  9676  cjreim  9695  cjreim2  9696  cjap  9698  cnrecnv  9702  cvg1nlemcxze  9773  cvg1nlemres  9776  r19.29uz  9782  resqrexlem1arp  9795  resqrexlemf  9797  resqrexlemf1  9798  resqrexlemfp1  9799  resqrexlemover  9800  resqrexlemdec  9801  resqrexlemdecn  9802  resqrexlemlo  9803  resqrexlemcalc1  9804  resqrexlemcalc2  9805  resqrexlemcalc3  9806  resqrexlemnmsq  9807  resqrexlemnm  9808  resqrexlemcvg  9809  resqrexlemglsq  9812  resqrexlemga  9813  resqrexlemsqa  9814  sqrtgt0  9824  sqrtsq  9834  absimle  9874  abstri  9894  cau3lem  9904  amgm2  9908  clim  9996  climshft  10019  climle  10048  clim2iser  10051  clim2iser2  10052  iiserex  10053  iisermulc2  10054  iserile  10056  climserile  10059  climrecvg1n  10061  climcvg1nlem  10062  climcaucn  10064  serif0  10065  nndivdvds  10077  absdvdsb  10089  dvdsabsb  10090  dvds1  10128  dvdsfac  10135  zeneo  10145  odd2np1lem  10146  even2n  10148  oexpneg  10151  oddge22np1  10156  evennn02n  10157  evennn2n  10158  2tp1odd  10159  mulsucdiv2z  10160  ltoddhalfle  10168  halfleoddlt  10169  m1expo  10175  m1exp1  10176  nn0enne  10177  nn0ehalf  10178  nn0o1gt2  10180  nno  10181  nn0o  10182  nn0oddm1d2  10184  nnoddm1d2  10185  4dvdseven  10192  sqr2irrlem  10193  sqrt2irr  10194  pw2dvdslemn  10196  pw2dvdseulemle  10198  oddpwdclemxy  10200  oddpwdclemodd  10203  oddpwdclemdc  10204  oddpwdc  10205  nn0seqcvgd  10206  ialginv  10212  ialgcvg  10213  ialgcvga  10216  ialgfx  10217  2spim  10236  bj-sbimeh  10242  bj-rspgt  10255  cbvrald  10257  bdsepnft  10337  bj-om  10391  peano5setOLD  10395  bj-nntrans  10406  bj-nnelirr  10408  setindft  10420  qdencn  10454
  Copyright terms: Public domain W3C validator