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

Step	Hyp	Ref	Expression
1		a1i.1	. 2 ⊢ 𝜑
2		ax-1 5	. 2 ⊢ (𝜑 → (𝜓 → 𝜑))
3	1, 2	ax-mp 7	1 ⊢ (𝜓 → 𝜑)

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  414  mpan2  415  mpani  420  mpan2i  421  anbi2i  444  anbi1i  445  nsyl3  588  mt2  601  mt2i  605  mto  620  mtoi  622  sylnib  633  simprimdc  789  con1biimdc  800  pm2.54dc  823  pm5.17dc  843  pm5.21nd  858  pm5.71dc  902  dedlema  910  dedlemb  911  a1tru  1300  xorbi12i  1314  dfbi3dc  1328  hbth  1392  dfexdc  1430  a17d  1460  nfvd  1462  nfan  1497  nfim  1504  19.21ht  1513  nfbi  1521  alrimd  1541  19.32dc  1609  equsexd  1657  spime  1669  equveli  1682  sbieh  1713  dvelimfALT2  1738  cbvald  1841  cbvexdh  1842  nfsbxy  1859  sbcomxyyz  1887  dvelimALT  1927  dvelimfv  1928  hbsb4t  1930  dvelimor  1935  eubii  1950  nfeudv  1956  nfmo  1961  mobii  1978  moimv  2007  2euswapdc  2032  eqidd  2082  syl5eq  2125  syl6eq  2129  syl5eqel  2165  syl5eleq  2167  syl6eqel  2169  syl6eleq  2171  nfcvd  2220  dvelimc  2239  nnedc  2250  necon1idc  2298  ralbii  2372  rexbii  2373  nfraldxy  2398  nfrexdxy  2399  nfralxy  2402  nfrexxy  2403  nfralya  2404  nfrexya  2405  rgenw  2418  ralimi  2426  rexim  2455  reximi  2458  rexlimivw  2473  r19.29af2  2496  r19.32vdc  2503  nfreudxy  2527  nfreuxy  2528  reubii  2539  rmobii  2544  ceqsralt  2626  vtoclgft  2649  rr19.28v  2734  reu8  2788  cdeqth  2802  nfsbc1d  2831  nfsbc1  2832  nfsbc  2835  sbcbii  2873  sbc2iegf  2884  sbc2iedv  2886  sbc3ie  2887  sbcrext  2891  rmob  2906  sbcnel12g  2923  sbcne12g  2924  csbcomg  2929  csbeq2i  2932  nfcsb1  2937  nfcsb  2940  csbiebt  2942  csbief  2947  csbie2t  2950  sbcnestgf  2953  syl5ss  3010  syl6ss  3011  syl5sseqr  3048  syl6eqss  3049  difssd  3099  ssconb  3105  abvor0dc  3269  rabnc  3277  nfif  3377  disjpr2  3456  tpid3g  3505  neldifsnd  3520  diftpsn3  3527  preq12bg  3565  intmin  3656  int0el  3666  dfiun2  3712  dfiin2  3713  dfiunv2  3714  iunrab  3725  iunid  3733  iun0  3734  iinrabm  3740  iunin1  3742  2iunin  3744  iinin1m  3747  syl5breq  3820  ssbri  3827  nfbr  3829  opabbii  3845  mpteq2i  3865  mpteq12i  3866  opth1  3991  copsexg  3999  copsex4g  4002  epelg  4045  issod  4074  fr0  4106  frind  4107  trsucss  4178  bm2.5ii  4240  ordsucss  4248  onsucelsucr  4252  ordunisuc2r  4258  ordirr  4285  ordfr  4317  peano5  4339  finds1  4343  ordom  4347  0elnn  4358  csbcnvg  4537  dmxpinm  4574  dfiun3  4609  dfiin3  4610  dmcosseq  4621  resiun1  4648  resiun2  4649  resima2  4662  iss  4674  resiima  4703  relbrcnvg  4724  inimasn  4761  elxp4  4828  elxp5  4829  dfco2  4840  coiun  4850  relssdmrn  4861  unielrel  4865  relfld  4866  cnviinm  4879  cnvsom  4881  nfiotadxy  4890  nfiotaxy  4891  iota2df  4911  funssres  4962  fntp  4976  imadif  4999  imain  5001  sbcfng  5064  sbcfg  5065  fun  5083  fun11iun  5167  funcocnv2  5171  f1oprg  5188  sefvex  5216  tz6.12f  5223  dfimafn2  5244  fnsnfv  5253  ssimaex  5255  fvun1  5260  fvmptg  5269  fvmpt3i  5273  fvopab6  5285  fndmdifcom  5294  respreima  5316  fmptco  5351  fcoconst  5355  dfmpt  5361  fmptapd  5375  fmptpr  5376  isocnv2  5472  riotaexg  5492  nfriotadxy  5496  nfriota  5497  riota2f  5509  nfov  5555  oprabbii  5580  mpt2eq123i  5588  ovmpt4g  5643  ovmpt2dxf  5646  ovmpt2x  5649  ovmpt2ga  5650  ovi3  5657  ov6g  5658  ovelrn  5669  caovcom  5678  caovass  5681  caovdi  5700  caovimo  5714  ofc12  5751  oprabex3  5776  reldm  5832  oprabco  5858  oprab2co  5859  mpt2xopoveq  5878  sprmpt2  5880  brtpos2  5889  reldmtpos  5891  dmtpos  5894  dftpos4  5901  tposfn2  5904  smores  5930  tfrlemisucfn  5961  tfrlemiubacc  5967  tfri1  5974  frec0g  6006  frectfr  6008  oacl  6063  omcl  6064  oeicl  6065  oawordi  6072  nnsucelsuc  6093  nntri1  6097  nnsseleq  6102  nnaord  6105  nnmordi  6112  nnmord  6113  nnaordex  6123  nnm00  6125  swoer  6157  eqer  6161  0er  6163  uniqs  6187  xpiderm  6200  erinxp  6203  qliftf  6214  brecop  6219  ecopovtrn  6226  ecopover  6227  ecopoverg  6230  th3qlem1  6231  brdomg  6252  en2i  6273  en3i  6274  dom2  6278  dom3  6279  ener  6282  ensymb  6283  entr  6287  fundmen  6309  xpsnen  6318  xpassen  6327  nneneq  6343  phplem4dom  6348  phpelm  6352  phplem4on  6353  fidceq  6354  fiunsnnn  6365  fnfi  6388  supubti  6412  suplubti  6413  cnvinfex  6431  eqinfti  6433  infvalti  6435  inflbti  6437  ordiso2  6446  cardcl  6450  pm54.43  6459  elni2  6504  indpi  6532  enqeceq  6549  mulcanenqec  6576  ltnnnq  6613  enq0er  6625  enq0eceq  6627  nqnq0pi  6628  mulcanenq0ec  6635  nnnq0lem1  6636  addnq0mo  6637  mulnq0mo  6638  prarloclemlo  6684  prarloclem3  6687  genipv  6699  nqprrnd  6733  nqprdisj  6734  nqprloc  6735  1idprl  6780  1idpru  6781  recexprlemlol  6816  recexprlemupu  6818  cauappcvgprlemm  6835  cauappcvgprlemdisj  6841  cauappcvgprlemladdru  6846  cauappcvgprlemladdrl  6847  cauappcvgpr  6852  caucvgprlemm  6858  caucvgprlemcl  6866  caucvgprlemladdrl  6868  caucvgpr  6872  caucvgprprlemmu  6885  caucvgprprlemopu  6889  caucvgprprlemclphr  6895  enreceq  6913  prsrlem1  6919  addsrmo  6920  mulsrmo  6921  0idsr  6944  pn0sr  6948  recexgt0sr  6950  archsr  6958  srpospr  6959  prsradd  6962  prsrlt  6963  caucvgsrlemfv  6967  caucvgsrlembound  6970  caucvgsrlemoffval  6972  caucvgsrlemoffcau  6974  caucvgsrlemoffgt1  6975  caucvgsrlemoffres  6976  caucvgsr  6978  pitonnlem1p1  7014  pitoregt0  7017  recidpirqlemcalc  7025  recidpirq  7026  axcnex  7027  axmulcl  7034  axmulass  7039  axdistr  7040  ax0id  7044  axprecex  7046  axpre-ltirr  7048  axpre-lttrn  7050  axpre-ltadd  7052  axpre-mulgt0  7053  axpre-mulext  7054  axcaucvglemval  7063  axcaucvg  7066  0cnd  7112  0red  7120  1red  7134  1cnd  7135  ltxrlt  7178  1p1times  7242  nfneg  7305  negsub  7356  addlsub  7474  pncan1  7481  npcan1  7482  negf1o  7486  kcnktkm1cn  7487  mulsubfacd  7522  rereim  7686  cru  7702  apreim  7703  mulreim  7704  apadd1  7708  apneg  7711  muleqadd  7758  eqneg  7820  mulgt1  7941  suprlubex  8030  negiso  8033  dfinfre  8034  cju  8038  nn1suc  8058  2cnd  8112  avglt1  8269  avglt2  8270  add1p1  8280  sub1m1  8281  cnm2m1cnm3  8282  xp1d2m1eqxm1d2  8283  div4p1lem1div2  8284  nn0p1gt0  8317  un0addcl  8321  nn0ge2m1nn  8348  0zd  8363  elnn0z  8364  elznn0  8366  1zzd  8378  peano2z  8387  ztri3or0  8393  zlelttric  8396  zltnle  8397  zmulcl  8404  zltp1le  8405  zgt0ge1  8409  elz2  8419  zdceq  8423  zdclt  8425  nn0lt2  8429  zneo  8448  nneo  8450  zeo2  8453  uzind  8458  uzind2  8459  nn0ind  8461  zadd2cl  8476  uzm1  8649  uzin  8651  uz3m2nn  8661  uzind4i  8680  infrenegsupex  8682  supminfex  8685  eqreznegel  8699  nn01to3  8702  nn0ge2m1nnALT  8703  divfnzn  8706  cnref1o  8733  rpnegap  8766  divlt1lt  8801  divle1le  8802  ltxr  8849  xrre3  8889  ixxssixx  8925  elioc2  8959  elico2  8960  elicc2  8961  lincmb01cmp  9025  fzdcel  9059  ige3m2fz  9068  fz01en  9072  fzdifsuc  9098  elfz1b  9107  uzsplit  9109  fseq1p1m1  9111  elfzp1b  9114  ige2m1fz1  9126  ige2m1fz  9127  0elfz  9132  fz0tp  9135  fz0fzdiffz0  9141  nn0split  9147  fzoval  9158  fzouzsplit  9188  elfzom1elp1fzo  9211  elfzonlteqm1  9219  fzo0to3tp  9228  fzo0sn0fzo1  9230  fzosplitprm1  9243  fvinim0ffz  9250  qlelttric  9254  qltnle  9255  qdceq  9256  qbtwnrelemcalc  9264  qbtwnre  9265  ioo0  9268  ioom  9269  ico0  9270  ioc0  9271  2tnp1ge0ge0  9303  flhalf  9304  fldiv4p1lem1div2  9307  intfracq  9322  q0mod  9357  q1mod  9358  mulp1mod1  9367  modqnegd  9381  modsumfzodifsn  9398  frec2uzltd  9405  frec2uzlt2d  9406  frecuzrdgrrn  9410  frec2uzrdg  9411  frecfzennn  9419  iseqss  9446  iseqfveq2  9448  iseqshft2  9452  iserf  9453  iserfre  9454  monoord  9455  isermono  9457  iseqsplit  9458  iseqcaopr3  9460  iseradd  9463  isersub  9464  iseqid3s  9466  iseqhomo  9468  iseqz  9469  iser0  9471  iser0f  9472  serige0  9473  serile  9474  expivallem  9477  expival  9478  exp0  9480  exp1  9482  expp1  9483  expgt1  9514  ltexp2a  9528  leexp2a  9529  leexp2r  9530  exple1  9532  expubnd  9533  binom21  9586  zesq  9591  expnlbnd2  9598  sqeq0d  9604  sqoddm1div8  9625  expcanlem  9643  expcan  9644  nn0opthlem1d  9647  nn0opthlem2d  9648  facnn  9654  fac0  9655  fac1  9656  facp1  9657  faclbnd  9668  faclbnd2  9669  bc0k  9683  bcn1  9685  ibcval5  9690  bcn2  9691  bcn2m1  9696  bcn2p1  9697  shftuz  9705  ovshftex  9707  shftfn  9712  imval  9737  crre  9744  crim  9745  remim  9747  cjreb  9753  readd  9756  remullem  9758  imadd  9764  cjadd  9771  cjreim  9790  cjreim2  9791  cjap  9793  cnrecnv  9797  cvg1nlemcxze  9868  cvg1nlemres  9871  rexfiuz  9875  r19.29uz  9878  resqrexlem1arp  9891  resqrexlemf  9893  resqrexlemf1  9894  resqrexlemfp1  9895  resqrexlemover  9896  resqrexlemdec  9897  resqrexlemdecn  9898  resqrexlemlo  9899  resqrexlemcalc1  9900  resqrexlemcalc2  9901  resqrexlemcalc3  9902  resqrexlemnmsq  9903  resqrexlemnm  9904  resqrexlemcvg  9905  resqrexlemglsq  9908  resqrexlemga  9909  resqrexlemsqa  9910  sqrtgt0  9920  sqrtsq  9930  absimle  9970  abstri  9990  cau3lem  10000  amgm2  10004  maxabsle  10090  maxabslemab  10092  maxabslemlub  10093  maxltsup  10104  max0addsup  10105  fimaxre2  10109  clim  10120  climshft  10143  climle  10172  clim2iser  10175  clim2iser2  10176  iiserex  10177  iisermulc2  10178  iserile  10180  climserile  10183  climrecvg1n  10185  climcvg1nlem  10186  climcaucn  10188  serif0  10189  nndivdvds  10201  absdvdsb  10213  dvdsabsb  10214  dvds1  10253  dvdsfac  10260  zeneo  10270  odd2np1lem  10271  even2n  10273  oexpneg  10276  oddge22np1  10281  evennn02n  10282  evennn2n  10283  2tp1odd  10284  mulsucdiv2z  10285  ltoddhalfle  10293  halfleoddlt  10294  m1expo  10300  m1exp1  10301  nn0enne  10302  nn0ehalf  10303  nn0o1gt2  10305  nno  10306  nn0o  10307  nn0oddm1d2  10309  nnoddm1d2  10310  4dvdseven  10317  flodddiv4  10334  flodddiv4lt  10336  flodddiv4t2lthalf  10337  zsupcllemex  10342  zsupcl  10343  infssuzex  10345  infssuzcldc  10347  gcddvds  10355  zeqzmulgcd  10362  gcdcom  10365  gcdabs  10379  gcdabs1  10380  dfgcd3  10399  gcdass  10404  bezoutr1  10422  nn0seqcvgd  10423  ialginv  10429  ialgcvg  10430  ialgcvga  10433  ialgfx  10434  eucialgcvga  10440  eucialg  10441  lcmval  10445  lcmcom  10446  lcmabs  10458  lcmass  10467  ncoprmgcdne1b  10471  cncongr1  10485  prmind2  10502  dvdsnprmd  10507  prmgt1  10513  oddprmge3  10516  coprm  10523  sqrt2irrlem  10540  sqrt2irr  10541  pw2dvdslemn  10543  pw2dvdseulemle  10545  oddpwdclemxy  10547  oddpwdclemodd  10550  oddpwdclemdc  10551  oddpwdc  10552  sqpweven  10553  2sqpwodd  10554  sqrt2irraplemnn  10557  sqrt2irrap  10558  2spim  10577  bj-sbimeh  10583  bj-rspgt  10596  cbvrald  10598  bdsepnft  10678  bj-om  10732  bj-nntrans  10746  bj-nnelirr  10748  setindft  10760  qdencn  10785