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  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  3276  rabnc  3284  nfif  3385  disjpr2  3464  tpid3g  3513  neldifsnd  3528  diftpsn3  3535  preq12bg  3573  intmin  3664  int0el  3674  dfiun2  3720  dfiin2  3721  dfiunv2  3722  iunrab  3733  iunid  3741  iun0  3742  iinrabm  3748  iunin1  3750  2iunin  3752  iinin1m  3755  syl5breq  3828  ssbri  3835  nfbr  3837  opabbii  3853  mpteq2i  3873  mpteq12i  3874  opth1  3999  copsexg  4007  copsex4g  4010  epelg  4053  issod  4082  fr0  4114  frind  4115  trsucss  4186  bm2.5ii  4248  ordsucss  4256  onsucelsucr  4260  ordunisuc2r  4266  ordirr  4293  ordfr  4325  peano5  4347  finds1  4351  ordom  4355  0elnn  4366  csbcnvg  4547  dmxpinm  4584  dfiun3  4619  dfiin3  4620  dmcosseq  4631  resiun1  4658  resiun2  4659  resima2  4672  iss  4684  resiima  4713  relbrcnvg  4734  inimasn  4771  elxp4  4838  elxp5  4839  dfco2  4850  coiun  4860  relssdmrn  4871  unielrel  4875  relfld  4876  cnviinm  4889  cnvsom  4891  nfiotadxy  4900  nfiotaxy  4901  iota2df  4921  funssres  4972  fntp  4987  imadif  5010  imain  5012  sbcfng  5075  sbcfg  5076  fun  5094  fun11iun  5178  funcocnv2  5182  f1oprg  5199  sefvex  5227  tz6.12f  5234  dfimafn2  5255  fnsnfv  5264  ssimaex  5266  fvun1  5271  fvmptg  5280  fvmpt3i  5284  fvopab6  5296  fndmdifcom  5305  respreima  5327  fmptco  5362  fcoconst  5366  dfmpt  5372  fmptapd  5386  fmptpr  5387  isocnv2  5483  riotaexg  5503  nfriotadxy  5507  nfriota  5508  riota2f  5520  nfov  5566  oprabbii  5591  mpt2eq123i  5599  ovmpt4g  5654  ovmpt2dxf  5657  ovmpt2x  5660  ovmpt2ga  5661  ovi3  5668  ov6g  5669  ovelrn  5680  caovcom  5689  caovass  5692  caovdi  5711  caovimo  5725  ofc12  5762  oprabex3  5787  reldm  5843  oprabco  5869  oprab2co  5870  mpt2xopoveq  5889  sprmpt2  5891  brtpos2  5900  reldmtpos  5902  dmtpos  5905  dftpos4  5912  tposfn2  5915  smores  5941  tfrlemisucfn  5973  tfrlemiubacc  5979  tfri1dALT  6000  tfrcl  6013  tfri1  6014  rdgon  6035  frec0g  6046  frectfr  6049  freccllem  6051  frecfcllem  6053  frecsuclem  6055  oacl  6104  omcl  6105  oeicl  6106  oawordi  6113  nnsucelsuc  6135  nntri1  6140  nnsseleq  6145  nnaord  6148  nnmordi  6155  nnmord  6156  nnaordex  6166  nnm00  6168  swoer  6200  eqer  6204  0er  6206  uniqs  6230  xpiderm  6243  erinxp  6246  qliftf  6257  brecop  6262  ecopovtrn  6269  ecopover  6270  ecopoverg  6273  th3qlem1  6274  brdomg  6295  en2i  6317  en3i  6318  dom2  6322  dom3  6323  ener  6326  ensymb  6327  entr  6331  fundmen  6353  xpsnen  6365  xpassen  6374  nneneq  6392  phplem4dom  6397  phpelm  6401  phplem4on  6402  fidceq  6404  fiunsnnn  6415  infm  6432  unfidisj  6442  undiffi  6443  unfiin  6444  fnfi  6446  supubti  6471  suplubti  6472  cnvinfex  6490  eqinfti  6492  infvalti  6494  inflbti  6496  ordiso2  6505  cardcl  6509  pm54.43  6518  en2other2  6522  elni2  6566  indpi  6594  enqeceq  6611  mulcanenqec  6638  ltnnnq  6675  enq0er  6687  enq0eceq  6689  nqnq0pi  6690  mulcanenq0ec  6697  nnnq0lem1  6698  addnq0mo  6699  mulnq0mo  6700  prarloclemlo  6746  prarloclem3  6749  genipv  6761  nqprrnd  6795  nqprdisj  6796  nqprloc  6797  1idprl  6842  1idpru  6843  recexprlemlol  6878  recexprlemupu  6880  cauappcvgprlemm  6897  cauappcvgprlemdisj  6903  cauappcvgprlemladdru  6908  cauappcvgprlemladdrl  6909  cauappcvgpr  6914  caucvgprlemm  6920  caucvgprlemcl  6928  caucvgprlemladdrl  6930  caucvgpr  6934  caucvgprprlemmu  6947  caucvgprprlemopu  6951  caucvgprprlemclphr  6957  enreceq  6975  prsrlem1  6981  addsrmo  6982  mulsrmo  6983  0idsr  7006  pn0sr  7010  recexgt0sr  7012  archsr  7020  srpospr  7021  prsradd  7024  prsrlt  7025  caucvgsrlemfv  7029  caucvgsrlembound  7032  caucvgsrlemoffval  7034  caucvgsrlemoffcau  7036  caucvgsrlemoffgt1  7037  caucvgsrlemoffres  7038  caucvgsr  7040  pitonnlem1p1  7076  pitoregt0  7079  recidpirqlemcalc  7087  recidpirq  7088  axcnex  7089  axmulcl  7096  axmulass  7101  axdistr  7102  ax0id  7106  axprecex  7108  axpre-ltirr  7110  axpre-lttrn  7112  axpre-ltadd  7114  axpre-mulgt0  7115  axpre-mulext  7116  axcaucvglemval  7125  axcaucvg  7128  0cnd  7174  0red  7182  1red  7196  1cnd  7197  ltxrlt  7245  1p1times  7309  nfneg  7372  negsub  7423  addlsub  7541  pncan1  7548  npcan1  7549  negf1o  7553  kcnktkm1cn  7554  mulsubfacd  7589  rereim  7753  cru  7769  apreim  7770  mulreim  7771  apadd1  7775  apneg  7778  muleqadd  7825  eqneg  7887  mulgt1  8008  suprlubex  8097  negiso  8100  dfinfre  8101  cju  8105  nn1suc  8125  2cnd  8179  avglt1  8336  avglt2  8337  add1p1  8347  sub1m1  8348  cnm2m1cnm3  8349  xp1d2m1eqxm1d2  8350  div4p1lem1div2  8351  nn0p1gt0  8384  un0addcl  8388  nn0ge2m1nn  8415  0zd  8444  elnn0z  8445  elznn0  8447  1zzd  8459  peano2z  8468  ztri3or0  8474  zlelttric  8477  zltnle  8478  zmulcl  8485  zltp1le  8486  zgt0ge1  8490  elz2  8500  zdceq  8504  zdclt  8506  nn0lt2  8510  zneo  8529  nneo  8531  zeo2  8534  uzind  8539  uzind2  8540  nn0ind  8542  zadd2cl  8557  uzm1  8730  uzin  8732  uz3m2nn  8742  uzind4i  8761  infrenegsupex  8763  supminfex  8766  eqreznegel  8780  nn01to3  8783  nn0ge2m1nnALT  8784  divfnzn  8787  cnref1o  8814  rpnegap  8847  divlt1lt  8882  divle1le  8883  ltxr  8927  xrre3  8965  ixxssixx  9001  elioc2  9035  elico2  9036  elicc2  9037  lincmb01cmp  9101  fzdcel  9135  ige3m2fz  9144  fz01en  9148  fzdifsuc  9174  elfz1b  9183  uzsplit  9185  fseq1p1m1  9187  elfzp1b  9190  ige2m1fz1  9202  ige2m1fz  9203  0elfz  9209  fz0tp  9212  fz0fzdiffz0  9218  nn0split  9224  fzoval  9235  fzouzsplit  9265  elfzom1elp1fzo  9288  elfzonlteqm1  9296  fzo0to3tp  9305  fzo0sn0fzo1  9307  fzosplitprm1  9320  fvinim0ffz  9327  qlelttric  9331  qltnle  9332  qdceq  9333  qbtwnrelemcalc  9342  qbtwnre  9343  ioo0  9346  ioom  9347  ico0  9348  ioc0  9349  2tnp1ge0ge0  9383  flhalf  9384  fldiv4p1lem1div2  9387  intfracq  9402  q0mod  9437  q1mod  9438  mulp1mod1  9447  modqnegd  9461  modsumfzodifsn  9478  frec2uzltd  9485  frec2uzlt2d  9486  frecfzennn  9508  iseqvalcbv  9531  iseqfclt  9536  iseqss  9541  iseqsst  9542  monoord  9551  iseqcaopr3  9556  iseradd  9559  isersub  9560  iseqid3s  9562  iseqhomo  9565  iseqz  9566  iser0  9568  serige0  9570  serile  9571  expival  9575  exp0  9577  expgt1  9611  ltexp2a  9625  leexp2a  9626  leexp2r  9627  exple1  9629  expubnd  9630  binom21  9683  zesq  9688  expnlbnd2  9695  sqeq0d  9701  sqoddm1div8  9722  expcanlem  9740  expcan  9741  nn0opthlem1d  9744  nn0opthlem2d  9745  faclbnd  9765  faclbnd2  9766  bc0k  9780  bcn1  9782  ibcval5  9787  bcn2  9788  bcn2m1  9793  bcn2p1  9794  sizeen1  9823  sizeunlem  9828  1elfz0size  9830  sizeprg  9832  shftuz  9843  ovshftex  9845  shftfn  9850  imval  9875  crre  9882  crim  9883  remim  9885  cjreb  9891  readd  9894  remullem  9896  imadd  9902  cjadd  9909  cjreim  9928  cjreim2  9929  cjap  9931  cnrecnv  9935  cvg1nlemcxze  10006  cvg1nlemres  10009  rexfiuz  10013  r19.29uz  10016  resqrexlem1arp  10029  resqrexlemfp1  10033  resqrexlemover  10034  resqrexlemdec  10035  resqrexlemdecn  10036  resqrexlemlo  10037  resqrexlemcalc1  10038  resqrexlemcalc2  10039  resqrexlemcalc3  10040  resqrexlemnmsq  10041  resqrexlemnm  10042  resqrexlemcvg  10043  resqrexlemglsq  10046  resqrexlemga  10047  resqrexlemsqa  10048  sqrtgt0  10058  sqrtsq  10068  absimle  10108  abstri  10128  cau3lem  10138  amgm2  10142  maxabsle  10228  maxabslemab  10230  maxabslemlub  10231  maxltsup  10242  max0addsup  10243  fimaxre2  10247  clim  10258  climshft  10281  climle  10310  clim2iser  10313  clim2iser2  10314  iiserex  10315  iisermulc2  10316  iserile  10318  climserile  10321  climrecvg1n  10323  climcvg1nlem  10324  climcaucn  10326  isumrblem  10337  fisumcvg  10338  nndivdvds  10346  absdvdsb  10358  dvdsabsb  10359  dvds1  10398  dvdsfac  10405  zeneo  10415  odd2np1lem  10416  even2n  10418  oexpneg  10421  oddge22np1  10425  evennn02n  10426  evennn2n  10427  2tp1odd  10428  mulsucdiv2z  10429  ltoddhalfle  10437  halfleoddlt  10438  m1expo  10444  m1exp1  10445  nn0enne  10446  nn0ehalf  10447  nn0o1gt2  10449  nno  10450  nn0o  10451  nn0oddm1d2  10453  nnoddm1d2  10454  4dvdseven  10461  flodddiv4  10478  flodddiv4lt  10480  flodddiv4t2lthalf  10481  zsupcllemex  10486  zsupcl  10487  infssuzex  10489  infssuzcldc  10491  gcddvds  10499  zeqzmulgcd  10506  gcdcom  10509  gcdabs  10523  gcdabs1  10524  dfgcd3  10543  gcdass  10548  bezoutr1  10566  nn0seqcvgd  10567  ialginv  10573  ialgcvg  10574  ialgcvga  10577  ialgfx  10578  eucialgcvga  10584  eucialg  10585  lcmval  10589  lcmcom  10590  lcmabs  10602  lcmass  10611  ncoprmgcdne1b  10615  cncongr1  10629  prmind2  10646  dvdsnprmd  10651  prmgt1  10657  oddprmge3  10660  coprm  10667  sqrt2irrlem  10684  sqrt2irr  10685  pw2dvdslemn  10687  pw2dvdseulemle  10689  oddpwdclemxy  10691  oddpwdclemodd  10694  oddpwdclemdc  10695  oddpwdc  10696  sqpweven  10697  2sqpwodd  10698  sqrt2irraplemnn  10701  sqrt2irrap  10702  oddennn  10703  evenennn  10704  unennn  10708  2spim  10728  bj-sbimeh  10734  bj-rspgt  10747  cbvrald  10749  bdsepnft  10836  bj-om  10890  bj-nntrans  10904  bj-nnelirr  10906  setindft  10918  qdencn  10943
  Copyright terms: Public domain W3C validator