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  790  con1biimdc  801  pm2.54dc  824  pm5.17dc  844  pm5.21nd  859  pm5.71dc  903  dedlema  911  dedlemb  912  a1tru  1301  xorbi12i  1315  dfbi3dc  1329  hbth  1393  dfexdc  1431  a17d  1461  nfvd  1463  nfan  1498  nfim  1505  19.21ht  1514  nfbi  1522  alrimd  1542  19.32dc  1610  equsexd  1658  spime  1670  equveli  1683  sbieh  1714  dvelimfALT2  1739  cbvald  1842  cbvexdh  1843  nfsbxy  1860  sbcomxyyz  1888  dvelimALT  1928  dvelimfv  1929  hbsb4t  1931  dvelimor  1936  eubii  1951  nfeudv  1957  nfmo  1962  mobii  1979  moimv  2008  2euswapdc  2033  eqidd  2083  syl5eq  2126  syl6eq  2130  syl5eqel  2166  syl5eleq  2168  syl6eqel  2170  syl6eleq  2172  nfcvd  2221  dvelimc  2240  nnedc  2251  necon1idc  2299  ralbii  2373  rexbii  2374  nfraldxy  2399  nfrexdxy  2400  nfralxy  2403  nfrexxy  2404  nfralya  2405  nfrexya  2406  rgenw  2419  ralimi  2427  rexim  2456  reximi  2459  rexlimivw  2474  r19.29af2  2497  r19.32vdc  2504  nfreudxy  2528  nfreuxy  2529  reubii  2540  rmobii  2545  ceqsralt  2627  vtoclgft  2650  rr19.28v  2735  reu8  2789  cdeqth  2803  nfsbc1d  2832  nfsbc1  2833  nfsbc  2836  sbcbii  2874  sbc2iegf  2885  sbc2iedv  2887  sbc3ie  2888  sbcrext  2892  rmob  2907  sbcnel12g  2924  sbcne12g  2925  csbcomg  2930  csbeq2i  2933  nfcsb1  2938  nfcsb  2941  csbiebt  2943  csbief  2948  csbie2t  2951  sbcnestgf  2954  syl5ss  3011  syl6ss  3012  syl5sseqr  3049  syl6eqss  3050  difssd  3100  ssconb  3106  abvor0dc  3270  rabnc  3278  nfif  3379  disjpr2  3458  tpid3g  3507  neldifsnd  3522  diftpsn3  3529  preq12bg  3567  intmin  3658  int0el  3668  dfiun2  3714  dfiin2  3715  dfiunv2  3716  iunrab  3727  iunid  3735  iun0  3736  iinrabm  3742  iunin1  3744  2iunin  3746  iinin1m  3749  syl5breq  3822  ssbri  3829  nfbr  3831  opabbii  3847  mpteq2i  3867  mpteq12i  3868  opth1  3993  copsexg  4001  copsex4g  4004  epelg  4047  issod  4076  fr0  4108  frind  4109  trsucss  4180  bm2.5ii  4242  ordsucss  4250  onsucelsucr  4254  ordunisuc2r  4260  ordirr  4287  ordfr  4319  peano5  4341  finds1  4345  ordom  4349  0elnn  4360  csbcnvg  4541  dmxpinm  4578  dfiun3  4613  dfiin3  4614  dmcosseq  4625  resiun1  4652  resiun2  4653  resima2  4666  iss  4678  resiima  4707  relbrcnvg  4728  inimasn  4765  elxp4  4832  elxp5  4833  dfco2  4844  coiun  4854  relssdmrn  4865  unielrel  4869  relfld  4870  cnviinm  4883  cnvsom  4885  nfiotadxy  4894  nfiotaxy  4895  iota2df  4915  funssres  4966  fntp  4981  imadif  5004  imain  5006  sbcfng  5069  sbcfg  5070  fun  5088  fun11iun  5172  funcocnv2  5176  f1oprg  5193  sefvex  5221  tz6.12f  5228  dfimafn2  5249  fnsnfv  5258  ssimaex  5260  fvun1  5265  fvmptg  5274  fvmpt3i  5278  fvopab6  5290  fndmdifcom  5299  respreima  5321  fmptco  5356  fcoconst  5360  dfmpt  5366  fmptapd  5380  fmptpr  5381  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  5967  tfrlemiubacc  5973  tfri1dALT  5994  tfrcl  6007  tfri1  6008  rdgon  6029  frec0g  6040  frectfr  6043  freccllem  6045  frecfcllem  6047  frecsuclem  6049  oacl  6098  omcl  6099  oeicl  6100  oawordi  6107  nnsucelsuc  6128  nntri1  6133  nnsseleq  6138  nnaord  6141  nnmordi  6148  nnmord  6149  nnaordex  6159  nnm00  6161  swoer  6193  eqer  6197  0er  6199  uniqs  6223  xpiderm  6236  erinxp  6239  qliftf  6250  brecop  6255  ecopovtrn  6262  ecopover  6263  ecopoverg  6266  th3qlem1  6267  brdomg  6288  en2i  6309  en3i  6310  dom2  6314  dom3  6315  ener  6318  ensymb  6319  entr  6323  fundmen  6345  xpsnen  6355  xpassen  6364  nneneq  6382  phplem4dom  6387  phpelm  6391  phplem4on  6392  fidceq  6394  fiunsnnn  6405  infm  6422  unfidisj  6432  undiffi  6433  unfiin  6434  fnfi  6436  supubti  6461  suplubti  6462  cnvinfex  6480  eqinfti  6482  infvalti  6484  inflbti  6486  ordiso2  6495  cardcl  6499  pm54.43  6508  en2other2  6512  elni2  6555  indpi  6583  enqeceq  6600  mulcanenqec  6627  ltnnnq  6664  enq0er  6676  enq0eceq  6678  nqnq0pi  6679  mulcanenq0ec  6686  nnnq0lem1  6687  addnq0mo  6688  mulnq0mo  6689  prarloclemlo  6735  prarloclem3  6738  genipv  6750  nqprrnd  6784  nqprdisj  6785  nqprloc  6786  1idprl  6831  1idpru  6832  recexprlemlol  6867  recexprlemupu  6869  cauappcvgprlemm  6886  cauappcvgprlemdisj  6892  cauappcvgprlemladdru  6897  cauappcvgprlemladdrl  6898  cauappcvgpr  6903  caucvgprlemm  6909  caucvgprlemcl  6917  caucvgprlemladdrl  6919  caucvgpr  6923  caucvgprprlemmu  6936  caucvgprprlemopu  6940  caucvgprprlemclphr  6946  enreceq  6964  prsrlem1  6970  addsrmo  6971  mulsrmo  6972  0idsr  6995  pn0sr  6999  recexgt0sr  7001  archsr  7009  srpospr  7010  prsradd  7013  prsrlt  7014  caucvgsrlemfv  7018  caucvgsrlembound  7021  caucvgsrlemoffval  7023  caucvgsrlemoffcau  7025  caucvgsrlemoffgt1  7026  caucvgsrlemoffres  7027  caucvgsr  7029  pitonnlem1p1  7065  pitoregt0  7068  recidpirqlemcalc  7076  recidpirq  7077  axcnex  7078  axmulcl  7085  axmulass  7090  axdistr  7091  ax0id  7095  axprecex  7097  axpre-ltirr  7099  axpre-lttrn  7101  axpre-ltadd  7103  axpre-mulgt0  7104  axpre-mulext  7105  axcaucvglemval  7114  axcaucvg  7117  0cnd  7163  0red  7171  1red  7185  1cnd  7186  ltxrlt  7234  1p1times  7298  nfneg  7361  negsub  7412  addlsub  7530  pncan1  7537  npcan1  7538  negf1o  7542  kcnktkm1cn  7543  mulsubfacd  7578  rereim  7742  cru  7758  apreim  7759  mulreim  7760  apadd1  7764  apneg  7767  muleqadd  7814  eqneg  7876  mulgt1  7997  suprlubex  8086  negiso  8089  dfinfre  8090  cju  8094  nn1suc  8114  2cnd  8168  avglt1  8325  avglt2  8326  add1p1  8336  sub1m1  8337  cnm2m1cnm3  8338  xp1d2m1eqxm1d2  8339  div4p1lem1div2  8340  nn0p1gt0  8373  un0addcl  8377  nn0ge2m1nn  8404  0zd  8433  elnn0z  8434  elznn0  8436  1zzd  8448  peano2z  8457  ztri3or0  8463  zlelttric  8466  zltnle  8467  zmulcl  8474  zltp1le  8475  zgt0ge1  8479  elz2  8489  zdceq  8493  zdclt  8495  nn0lt2  8499  zneo  8518  nneo  8520  zeo2  8523  uzind  8528  uzind2  8529  nn0ind  8531  zadd2cl  8546  uzm1  8719  uzin  8721  uz3m2nn  8731  uzind4i  8750  infrenegsupex  8752  supminfex  8755  eqreznegel  8769  nn01to3  8772  nn0ge2m1nnALT  8773  divfnzn  8776  cnref1o  8803  rpnegap  8836  divlt1lt  8871  divle1le  8872  ltxr  8916  xrre3  8954  ixxssixx  8990  elioc2  9024  elico2  9025  elicc2  9026  lincmb01cmp  9090  fzdcel  9124  ige3m2fz  9133  fz01en  9137  fzdifsuc  9163  elfz1b  9172  uzsplit  9174  fseq1p1m1  9176  elfzp1b  9179  ige2m1fz1  9191  ige2m1fz  9192  0elfz  9198  fz0tp  9201  fz0fzdiffz0  9207  nn0split  9213  fzoval  9224  fzouzsplit  9254  elfzom1elp1fzo  9277  elfzonlteqm1  9285  fzo0to3tp  9294  fzo0sn0fzo1  9296  fzosplitprm1  9309  fvinim0ffz  9316  qlelttric  9320  qltnle  9321  qdceq  9322  qbtwnrelemcalc  9331  qbtwnre  9332  ioo0  9335  ioom  9336  ico0  9337  ioc0  9338  2tnp1ge0ge0  9372  flhalf  9373  fldiv4p1lem1div2  9376  intfracq  9391  q0mod  9426  q1mod  9427  mulp1mod1  9436  modqnegd  9450  modsumfzodifsn  9467  frec2uzltd  9474  frec2uzlt2d  9475  frecfzennn  9497  iseqvalcbv  9520  iseqfclt  9525  iseqss  9530  iseqsst  9531  monoord  9540  iseqcaopr3  9545  iseradd  9548  isersub  9549  iseqid3s  9551  iseqhomo  9554  iseqz  9555  iser0  9557  serige0  9559  serile  9560  expival  9564  exp0  9566  expgt1  9600  ltexp2a  9614  leexp2a  9615  leexp2r  9616  exple1  9618  expubnd  9619  binom21  9672  zesq  9677  expnlbnd2  9684  sqeq0d  9690  sqoddm1div8  9711  expcanlem  9729  expcan  9730  nn0opthlem1d  9733  nn0opthlem2d  9734  faclbnd  9754  faclbnd2  9755  bc0k  9769  bcn1  9771  ibcval5  9776  bcn2  9777  bcn2m1  9782  bcn2p1  9783  sizeen1  9812  sizeunlem  9817  1elfz0size  9819  sizeprg  9821  shftuz  9832  ovshftex  9834  shftfn  9839  imval  9864  crre  9871  crim  9872  remim  9874  cjreb  9880  readd  9883  remullem  9885  imadd  9891  cjadd  9898  cjreim  9917  cjreim2  9918  cjap  9920  cnrecnv  9924  cvg1nlemcxze  9995  cvg1nlemres  9998  rexfiuz  10002  r19.29uz  10005  resqrexlem1arp  10018  resqrexlemfp1  10022  resqrexlemover  10023  resqrexlemdec  10024  resqrexlemdecn  10025  resqrexlemlo  10026  resqrexlemcalc1  10027  resqrexlemcalc2  10028  resqrexlemcalc3  10029  resqrexlemnmsq  10030  resqrexlemnm  10031  resqrexlemcvg  10032  resqrexlemglsq  10035  resqrexlemga  10036  resqrexlemsqa  10037  sqrtgt0  10047  sqrtsq  10057  absimle  10097  abstri  10117  cau3lem  10127  amgm2  10131  maxabsle  10217  maxabslemab  10219  maxabslemlub  10220  maxltsup  10231  max0addsup  10232  fimaxre2  10236  clim  10247  climshft  10270  climle  10299  clim2iser  10302  clim2iser2  10303  iiserex  10304  iisermulc2  10305  iserile  10307  climserile  10310  climrecvg1n  10312  climcvg1nlem  10313  climcaucn  10315  isumrblem  10326  fisumcvg  10327  nndivdvds  10335  absdvdsb  10347  dvdsabsb  10348  dvds1  10387  dvdsfac  10394  zeneo  10404  odd2np1lem  10405  even2n  10407  oexpneg  10410  oddge22np1  10414  evennn02n  10415  evennn2n  10416  2tp1odd  10417  mulsucdiv2z  10418  ltoddhalfle  10426  halfleoddlt  10427  m1expo  10433  m1exp1  10434  nn0enne  10435  nn0ehalf  10436  nn0o1gt2  10438  nno  10439  nn0o  10440  nn0oddm1d2  10442  nnoddm1d2  10443  4dvdseven  10450  flodddiv4  10467  flodddiv4lt  10469  flodddiv4t2lthalf  10470  zsupcllemex  10475  zsupcl  10476  infssuzex  10478  infssuzcldc  10480  gcddvds  10488  zeqzmulgcd  10495  gcdcom  10498  gcdabs  10512  gcdabs1  10513  dfgcd3  10532  gcdass  10537  bezoutr1  10555  nn0seqcvgd  10556  ialginv  10562  ialgcvg  10563  ialgcvga  10566  ialgfx  10567  eucialgcvga  10573  eucialg  10574  lcmval  10578  lcmcom  10579  lcmabs  10591  lcmass  10600  ncoprmgcdne1b  10604  cncongr1  10618  prmind2  10635  dvdsnprmd  10640  prmgt1  10646  oddprmge3  10649  coprm  10656  sqrt2irrlem  10673  sqrt2irr  10674  pw2dvdslemn  10676  pw2dvdseulemle  10678  oddpwdclemxy  10680  oddpwdclemodd  10683  oddpwdclemdc  10684  oddpwdc  10685  sqpweven  10686  2sqpwodd  10687  sqrt2irraplemnn  10690  sqrt2irrap  10691  oddennn  10692  2spim  10713  bj-sbimeh  10719  bj-rspgt  10732  cbvrald  10734  bdsepnft  10821  bj-om  10875  bj-nntrans  10889  bj-nnelirr  10891  setindft  10903  qdencn  10928
  Copyright terms: Public domain W3C validator