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  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  3491  tpid3g  3540  neldifsnd  3556  diftpsn3  3563  preq12bg  3602  intmin  3693  int0el  3703  dfiun2  3749  dfiin2  3750  dfiunv2  3751  iunrab  3762  iunid  3770  iun0  3771  iinrabm  3777  iunin1  3779  2iunin  3781  iinin1m  3784  syl5breq  3857  ssbri  3864  nfbr  3866  opabbii  3882  mpteq2i  3902  mpteq12i  3903  opth1  4039  copsexg  4047  copsex4g  4050  epelg  4093  issod  4122  fr0  4154  frind  4155  trsucss  4226  bm2.5ii  4288  ordsucss  4296  onsucelsucr  4300  ordunisuc2r  4306  ordirr  4333  ordfr  4365  peano5  4388  finds1  4392  ordom  4396  0elnn  4407  omsinds  4410  csbcnvg  4590  dmxpinm  4627  dfiun3  4662  dfiin3  4663  dmcosseq  4674  resiun1  4701  resiun2  4702  resima2  4715  iss  4727  resiima  4759  relbrcnvg  4780  inimasn  4817  elxp4  4886  elxp5  4887  dfco2  4898  coiun  4908  relssdmrn  4919  unielrel  4926  relfld  4927  cnviinm  4940  cnvsom  4942  nfiotadxy  4951  nfiotaxy  4952  iota2df  4972  funssres  5023  fntp  5038  imadif  5061  imain  5063  sbcfng  5126  sbcfg  5127  fun  5149  fun11iun  5239  funcocnv2  5243  f1oprg  5260  sefvex  5291  tz6.12f  5298  dfimafn2  5319  fnsnfv  5328  ssimaex  5330  fvun1  5335  fvmptg  5345  fvmpt3i  5349  fvopab6  5361  fndmdifcom  5370  respreima  5392  fmptco  5429  fcoconst  5433  dfmpt  5439  fmptapd  5453  fmptpr  5454  isocnv2  5554  riotaexg  5575  nfriotadxy  5579  nfriota  5580  riota2f  5592  nfov  5638  oprabbii  5663  mpt2eq123i  5671  ovmpt4g  5726  ovmpt2dxf  5729  ovmpt2x  5732  ovmpt2ga  5733  ovi3  5740  ov6g  5741  ovelrn  5752  caovcom  5761  caovass  5764  caovdi  5783  caovimo  5797  ofc12  5834  oprabex3  5859  reldm  5915  oprabco  5941  oprab2co  5942  mpt2xopoveq  5961  sprmpt2  5963  brtpos2  5972  reldmtpos  5974  dmtpos  5977  dftpos4  5984  tposfn2  5987  smores  6013  tfrlemisucfn  6045  tfrlemiubacc  6051  tfri1dALT  6072  tfrcl  6085  tfri1  6086  rdgon  6107  frec0g  6118  frectfr  6121  freccllem  6123  frecfcllem  6125  frecsuclem  6127  oacl  6177  omcl  6178  oeicl  6179  oawordi  6186  nnsucelsuc  6208  nntri1  6213  nnsseleq  6218  nnaord  6222  nnmordi  6229  nnmord  6230  nnaordex  6240  nnm00  6242  swoer  6274  eqer  6278  0er  6280  uniqs  6304  xpiderm  6317  erinxp  6320  qliftf  6331  brecop  6336  ecopovtrn  6343  ecopover  6344  ecopoverg  6347  th3qlem1  6348  elpmg  6375  brdomg  6419  en2i  6441  en3i  6442  dom2  6446  dom3  6447  ener  6450  ensymb  6451  entr  6455  fundmen  6477  mapsnen  6482  map1  6483  xpsnen  6491  xpassen  6500  ssenen  6521  nneneq  6527  phplem4dom  6532  phpelm  6536  phplem4on  6537  fidceq  6539  fiunsnnn  6551  finexdc  6572  infm  6574  exmidpw  6578  unfidisj  6586  undifdc  6588  unfiin  6590  xpfi  6593  fisseneq  6595  ssfirab  6596  fnfi  6599  f1finf1o  6608  supubti  6641  suplubti  6642  cnvinfex  6660  eqinfti  6662  infvalti  6664  inflbti  6666  ordiso2  6675  djuex  6683  djuss  6708  1stinl  6712  2ndinl  6713  1stinr  6714  2ndinr  6715  updjudhcoinlf  6718  updjudhcoinrg  6719  casefun  6723  djufun  6731  finomni  6743  fodjuomnilemdc  6746  fodjuomnilemf  6747  fodjuomnilemm  6748  fodjuomnilem0  6749  nnnninf  6753  cardcl  6756  pm54.43  6765  en2other2  6769  exmidfodomrlemr  6775  exmidfodomrlemrALT  6776  elni2  6820  indpi  6848  enqeceq  6865  mulcanenqec  6892  ltnnnq  6929  enq0er  6941  enq0eceq  6943  nqnq0pi  6944  mulcanenq0ec  6951  nnnq0lem1  6952  addnq0mo  6953  mulnq0mo  6954  prarloclemlo  7000  prarloclem3  7003  genipv  7015  nqprrnd  7049  nqprdisj  7050  nqprloc  7051  1idprl  7096  1idpru  7097  recexprlemlol  7132  recexprlemupu  7134  cauappcvgprlemm  7151  cauappcvgprlemdisj  7157  cauappcvgprlemladdru  7162  cauappcvgprlemladdrl  7163  cauappcvgpr  7168  caucvgprlemm  7174  caucvgprlemcl  7182  caucvgprlemladdrl  7184  caucvgpr  7188  caucvgprprlemml  7200  caucvgprprlemmu  7201  caucvgprprlemopu  7205  caucvgprprlemclphr  7211  enreceq  7229  prsrlem1  7235  addsrmo  7236  mulsrmo  7237  0idsr  7260  pn0sr  7264  recexgt0sr  7266  archsr  7274  srpospr  7275  prsradd  7278  prsrlt  7279  caucvgsrlemfv  7283  caucvgsrlembound  7286  caucvgsrlemoffval  7288  caucvgsrlemoffcau  7290  caucvgsrlemoffgt1  7291  caucvgsrlemoffres  7292  caucvgsr  7294  pitonnlem1p1  7330  pitoregt0  7333  recidpirqlemcalc  7341  recidpirq  7342  axcnex  7343  axmulcl  7350  axmulass  7355  axdistr  7356  ax0id  7360  axprecex  7362  axpre-ltirr  7364  axpre-lttrn  7366  axpre-ltadd  7368  axpre-mulgt0  7369  axpre-mulext  7370  axcaucvglemval  7379  axcaucvg  7382  0cnd  7428  0red  7436  1red  7450  1cnd  7451  ltxrlt  7499  1p1times  7563  nfneg  7626  negsub  7677  addlsub  7795  pncan1  7802  npcan1  7803  negf1o  7807  kcnktkm1cn  7808  mulsubfacd  7843  rereim  8007  cru  8023  apreim  8024  mulreim  8025  apadd1  8029  apneg  8032  muleqadd  8079  eqneg  8141  mulgt1  8262  suprlubex  8351  negiso  8354  dfinfre  8355  cju  8359  nn1suc  8379  2cnd  8433  avglt1  8590  avglt2  8591  add1p1  8601  sub1m1  8602  cnm2m1cnm3  8603  xp1d2m1eqxm1d2  8604  div4p1lem1div2  8605  nn0p1gt0  8638  un0addcl  8642  nn0ge2m1nn  8669  0zd  8698  elnn0z  8699  elznn0  8701  1zzd  8713  peano2z  8722  ztri3or0  8728  zlelttric  8731  zltnle  8732  zmulcl  8739  zltp1le  8740  zgt0ge1  8744  elz2  8754  zdceq  8758  zdclt  8760  nn0lt2  8764  zneo  8783  nneo  8785  zeo2  8788  uzind  8793  uzind2  8794  nn0ind  8796  zadd2cl  8811  uzm1  8984  uzin  8986  uz3m2nn  8996  uzind4i  9015  infrenegsupex  9017  supminfex  9020  eqreznegel  9034  nn01to3  9037  nn0ge2m1nnALT  9038  divfnzn  9041  cnref1o  9068  rpnegap  9101  divlt1lt  9136  divle1le  9137  ltxr  9181  xrre3  9219  ixxssixx  9255  elioc2  9289  elico2  9290  elicc2  9291  lincmb01cmp  9355  fzdcel  9389  ige3m2fz  9398  fz01en  9402  fzdifsuc  9428  elfz1b  9437  uzsplit  9439  fseq1p1m1  9441  elfzp1b  9444  ige2m1fz1  9456  ige2m1fz  9457  0elfz  9463  fz0tp  9466  fz0fzdiffz0  9472  nn0split  9478  nnsplit  9479  fzoval  9490  fzouzsplit  9521  elfzom1elp1fzo  9544  elfzonlteqm1  9552  fzo0to3tp  9561  fzo0sn0fzo1  9563  fzosplitprm1  9576  fvinim0ffz  9583  qlelttric  9587  qltnle  9588  qdceq  9589  qbtwnrelemcalc  9598  qbtwnre  9599  ioo0  9602  ioom  9603  ico0  9604  ioc0  9605  2tnp1ge0ge0  9639  flhalf  9640  fldiv4p1lem1div2  9643  intfracq  9658  q0mod  9693  q1mod  9694  mulp1mod1  9703  modqnegd  9717  modsumfzodifsn  9734  frec2uzltd  9741  frec2uzlt2d  9742  frecfzennn  9764  1tonninf  9777  iseqvalcbv  9792  iseqfclt  9797  iseqclt  9801  iseqss  9803  iseqsst  9804  monoord  9813  iseqcaopr3  9818  iseqf1olemp  9839  iseradd  9842  isersub  9843  iseqid3s  9845  iseqhomo  9848  iseqz  9849  iser0  9851  serige0  9854  serile  9855  expival  9859  exp0  9861  expgt1  9895  ltexp2a  9909  leexp2a  9910  leexp2r  9911  exple1  9913  expubnd  9914  binom21  9967  zesq  9972  expnlbnd2  9979  sqeq0d  9985  sqoddm1div8  10006  expcanlem  10024  expcan  10025  nn0opthlem1d  10028  nn0opthlem2d  10029  faclbnd  10049  faclbnd2  10050  bc0k  10064  bcn1  10066  ibcval5  10071  bcn2  10072  bcn2m1  10077  bcn2p1  10078  fihashen1  10107  hashunlem  10112  1elfz0hash  10114  hashprg  10116  hashdifpr  10128  hashxp  10134  zfz1isolem1  10145  iseqcoll  10147  shftuz  10151  ovshftex  10153  shftfn  10158  imval  10183  crre  10190  crim  10191  remim  10193  cjreb  10199  readd  10202  remullem  10204  imadd  10210  cjadd  10217  cjreim  10236  cjreim2  10237  cjap  10239  cnrecnv  10243  cvg1nlemcxze  10314  cvg1nlemres  10317  rexfiuz  10321  r19.29uz  10324  resqrexlem1arp  10337  resqrexlemfp1  10341  resqrexlemover  10342  resqrexlemdec  10343  resqrexlemdecn  10344  resqrexlemlo  10345  resqrexlemcalc1  10346  resqrexlemcalc2  10347  resqrexlemcalc3  10348  resqrexlemnmsq  10349  resqrexlemnm  10350  resqrexlemcvg  10351  resqrexlemglsq  10354  resqrexlemga  10355  resqrexlemsqa  10356  sqrtgt0  10366  sqrtsq  10376  absimle  10416  abstri  10436  cau3lem  10446  amgm2  10450  maxabsle  10536  maxabslemab  10538  maxabslemlub  10539  maxltsup  10550  max0addsup  10551  fimaxre2  10556  clim  10567  climshft  10590  climle  10619  clim2iser  10622  clim2iser2  10623  iiserex  10624  iisermulc2  10625  iserile  10627  climserile  10630  climrecvg1n  10632  climcvg1nlem  10633  climcaucn  10635  isumrblem  10660  fisumcvg  10661  isummolem2a  10665  sum0  10671  fisumss  10675  fsumrecl  10683  fsumzcl  10684  fsumnn0cl  10685  fsumrpcl  10686  fsumadd  10688  fsumsplitf  10690  sumsnf  10691  sumpr  10694  sumtp  10695  nndivdvds  10708  absdvdsb  10720  dvdsabsb  10721  dvds1  10760  dvdsfac  10767  zeneo  10777  odd2np1lem  10778  even2n  10780  oexpneg  10783  oddge22np1  10787  evennn02n  10788  evennn2n  10789  2tp1odd  10790  mulsucdiv2z  10791  ltoddhalfle  10799  halfleoddlt  10800  m1expo  10806  m1exp1  10807  nn0enne  10808  nn0ehalf  10809  nn0o1gt2  10811  nno  10812  nn0o  10813  nn0oddm1d2  10815  nnoddm1d2  10816  4dvdseven  10823  flodddiv4  10840  flodddiv4lt  10842  flodddiv4t2lthalf  10843  zsupcllemex  10848  zsupcl  10849  infssuzex  10851  infssuzcldc  10853  gcddvds  10861  zeqzmulgcd  10868  gcdcom  10871  gcdabs  10885  gcdabs1  10886  dfgcd3  10905  gcdass  10910  bezoutr1  10928  nn0seqcvgd  10929  ialginv  10935  ialgcvg  10936  ialgcvga  10939  ialgfx  10940  eucialgcvga  10946  eucialg  10947  lcmval  10951  lcmcom  10952  lcmabs  10964  lcmass  10973  ncoprmgcdne1b  10977  cncongr1  10991  prmind2  11008  dvdsnprmd  11013  prmgt1  11019  oddprmge3  11022  coprm  11029  sqrt2irrlem  11046  sqrt2irr  11047  pw2dvdslemn  11049  pw2dvdseulemle  11051  oddpwdclemxy  11053  oddpwdclemodd  11056  oddpwdclemdc  11057  oddpwdc  11058  sqpweven  11059  2sqpwodd  11060  sqrt2irraplemnn  11063  sqrt2irrap  11064  divdenle  11081  nn0gcdsq  11084  numdensq  11086  nn0sqrtelqelz  11090  dfphi2  11102  phimullem  11107  oddennn  11111  evenennn  11112  unennn  11116  2spim  11136  bj-sbimeh  11142  bj-rspgt  11155  cbvrald  11157  bdsepnft  11247  bj-om  11301  bj-nntrans  11315  bj-nnelirr  11317  setindft  11329  nnsf  11364  peano4nninf  11365  peano3nninf  11366  nninfalllemn  11367  nninfsellemcl  11372  nninfself  11374  nninfsellemeq  11375  nninfsellemeqinf  11377  exmidsbthrlem  11381  qdencn  11384
  Copyright terms: Public domain W3C validator