Theorem a1i 8

Description: Inference derived from axiom ax-1 4. See a1d 12 for an explanation of our informal use of the terms "inference" and "deduction."

Hypothesis

Ref	Expression
a1i.1	⊢ φ

Assertion

Ref	Expression
a1i	⊢ (ψ → φ)

Proof of Theorem a1i

Step	Hyp	Ref	Expression
1		a1i.1	. 2 ⊢ φ
2		ax-1 4	. 2 ⊢ (φ → (ψ → φ))
3	1, 2	ax-mp 7	1 ⊢ (ψ → φ)

Syntax hints:   → wi 3

This theorem is referenced by:  syl 10  imim2i 17  mpi 44  mpdi 48  syl9 57  idd 61  pm2.21i 77  pm2.24i 104  pm2.61d1 128  pm2.61d2 129  pm4.2i 171  jctl 290  jctr 291  jctil 292  jctir 293  adantl 388  adantlll 396  sylani 464  sylan2i 465  impbid1 516  impbid2 517  syl5bb 531  syl6bb 535  2th 717  biass 743  dedlemb 762  hbth 999  19.21t 1113  dvelimfALT 1151  cbv3 1162  cbval 1163  sbt 1190  sbie 1194  hbsb4 1246  sbidm 1252  sbco2 1253  sbcom2 1332  dvelimALT 1351  ax11eq 1361  ax11f 1363  ax11indalem 1366  ax11inda2ALT 1367  a12lem1 1374  eubii 1385  hbeu 1387  mobii 1403  moimv 1417  euor2 1435  2euswap 1443  syl5eq 1516  syl6eq 1520  3eqtr4a 1529  syl5eqel 1549  syl5eleq 1551  syl6eqel 1553  syl6eleq 1555  ralbii 1664  rexbii 1665  r19.20si 1703  r19.22si 1731  ralcom2 1773  reubii 1779  hbeqd 1909  hbeld 1910  reu8 1932  sbcieg 1957  sbcbii 1974  hbsbc1gd 1979  hbsbcgd 1980  sbcralt 1986  sbcralgf 1988  hbcsb1gd 2023  hbcsbgd 2024  csbnestglem 2031  csbnest1g 2033  ssconb 2166  reuun1 2273  difsn 2460  snsspr 2466  sspr 2471  hbopd 2493  int0el 2556  eliun 2565  dfiun2 2582  iunab 2592  iun0 2599  syl5breq 2645  ssbri 2652  hbbrd 2654  sbcbrg 2657  opabbii 2666  csbopabg 2673  axrep4 2692  axsep 2697  dfid3 2831  reuuni2f 2878  reuuni2 2879  reuuni4 2882  reuxfr2 2898  reuunixfr 2901  ordtr2 2997  oneqmini 3012  bm2.5ii 3014  trsucss 3051  suceloni 3057  onuninsuc 3103  nlimsucg 3107  orduninsuc 3109  ordunisuc2 3110  onzsl 3112  dfom2 3128  limom 3141  peano3 3146  peano5 3148  finds1 3154  ssrel 3242  ssxp 3251  relopab 3261  hbimad 3404  csbima12g 3405  resiima 3411  ssxpr 3467  relssdr 3505  unielrel 3506  relfld 3507  funssres 3544  opabex2 3602  fnopab2 3610  fun 3632  hbfvd 3721  hbfvd2 3722  tz6.12f 3729  csbfv12g 3733  fvelrnb 3751  dfimafn2 3753  fvelimab 3756  fnsnfv 3758  ssimaex 3759  fvopab4g 3770  eqfnfv 3788  elrnopab 3792  fimacnv 3801  fconst4 3842  iunex 3854  funiunfv 3857  cbvfo 3876  isomin 3890  isoini 3891  f1oweALT 3897  tfrlem4 3905  tfrlem10 3911  tz7.49 3950  abianfplem 3952  abianfp 3953  hboprd 3973  csboprg 3977  oprabbii 3988  oprabex2g 4011  oprabex3 4013  oprabval2gf 4017  oprabval3 4021  oprabval6g 4023  oprvalelrn 4030  1st2val 4085  2nd2val 4086  1stcof 4091  dfoprab5 4105  fnoprab2 4112  elrnoprab 4115  df1st2 4116  df2nd2 4117  oev2 4152  om0r 4164  oaordi 4170  oaord 4171  oaordex 4182  oarec 4186  omordi 4187  omord2 4188  oeord 4205  oewordri 4209  oeworde 4210  oelim2 4212  nnaordex 4239  nnawordex 4240  nneob 4245  omsmolem 4246  brecop 4296  mapsspw 4331  mapss 4336  en2 4389  en3 4390  dom2 4392  fundmen 4415  mapsnen 4416  map1 4417  xpsnen 4421  xpcomen 4425  xpassen 4427  pw2en 4432  sbthbg 4444  canth2 4470  mapdom2lem 4479  mapdom2 4480  mapxpen 4481  xpmapenlem5 4486  mapunen 4488  ssenen 4490  phplem4 4497  nneneq 4498  php3 4501  pssnn 4519  domfi 4522  unfilem1 4530  unfi 4534  unifi 4538  fiint 4540  fodomfib 4547  iunfi 4549  pwfi 4551  pm54.43 4552  inf0 4586  inf3lem3 4595  inf3lem4 4596  dfom3 4610  infensuc 4618  r1lim 4633  r1ord3 4637  ranksn 4669  rankuni2 4670  rankval4 4682  rankc2 4686  rankxpl 4690  rankxpsuc 4695  scott0 4697  cplem1 4700  karden 4706  hta 4708  aceq3lem 4712  aceq5lem4 4718  aceq5lem5 4719  ac6lem 4734  kmlem3 4747  zorn2lem6 4773  zorn2lem7 4774  zorn 4777  fodomb 4780  brdom7disj 4784  brdom6disj 4785  unidom 4788  carden 4811  cardlim 4831  cardiun 4839  alephlim 4844  alephnbtwn2 4849  alephord 4855  alephord3 4858  cardaleph 4865  cardalephex 4866  cardinfima 4871  alephfplem3 4878  alephval3 4883  cfeq0 4894  cfsuc 4895  axextnd 4923  axrepndlem1 4924  axrepndlem2 4925  axunndlem1 4927  axunnd 4928  axpowndlem2 4930  axpowndlem4 4932  axpownd 4933  axregnd 4936  axinfndlem1 4937  axacndlem4 4942  zfcndrep 4946  indpi 5014  ltsopq 5055  prlem934a 5117  prlem936a 5133  reclem4pr 5139  suplem1pr 5141  ltsosr 5183  sqgt0sr 5195  suppsr2 5203  suppsr3 5204  pre-axltadd 5269  pre-axmulgt0 5270  pre-axsup 5271  hbnegd 5343  ltxrt 5475  lelttrt 5504  ltletrt 5505  xrlelttrt 5543  xrltletrt 5544  muleqaddt 5677  divdivmult 5759  lemul12itOLD 5807  mulgt1t 5809  lediv12it 5852  squeeze0 5880  nn1suc 5895  nnleltp1t 5909  nnsub 5911  nnaddm1clt 5913  sup2 6006  dfinfmr 6022  infmsup 6023  xrsupexmnf 6029  xrinfmexpnf 6030  xrsupsslem 6031  xrinfmsslem 6032  xrub 6035  supxrre 6038  supxrmnf 6042  elznn0 6104  nn0subt 6116  zaddclt 6120  zmulclt 6135  zltp1let 6136  dfuz 6158  uzind 6161  uzind2 6162  uzindOLD 6164  nn0ind 6168  flval3t 6190  flhalft 6197  elq 6203  om2uzlt 6243  om2uzlt2 6244  om2uzran 6245  iooval2t 6312  elioc2t 6330  elico2t 6331  elicc2t 6332  ioossre 6336  iccf 6342  uzssz 6370  uzind4i 6394  uzwo 6395  uzwoOLD 6396  elfz2nn0t 6435  fsequb 6463  limsupclt 6470  expordit 6539  expwordit 6542  expubndt 6547  sqlecant 6580  expnbndt 6593  sqrlem6 6616  sqrlem12 6622  cjclt 6704  reret 6742  cjreimt 6771  cjreim2t 6772  absdivz 6802  leabst 6807  abssubne0t 6828  cjdiv 6834  seq1ublem 6856  cau5i 6862  cvg3 6868  faclbnd 6890  faclbnd4lem1 6893  faclbnd4lem4 6896  bcn0t 6909  bcnp11t 6911  fsum1s 6955  fsump1s 6959  fsum1p 6965  fsummulc1 6979  fsumconst 6984  fsumcmp 6986  fsumcmp0 6987  fsumcmpndx2 6988  fsumabs 6989  ser1ser0 6994  binomlem1 7012  binomlem2 7013  binomlem4 7015  bcxmas 7022  climconst 7039  climmullem3 7066  climmulc2 7073  iserzshft 7088  clim2serz 7089  caucvglem2 7102  caucvg3lem 7110  caucvg3t 7112  ser1f0 7114  ser1clim0 7117  cvgcmp2lem 7124  cvgcmpub 7129  isumclim3t 7143  isumnul 7146  fnsmnt 7169  expcnvlem6 7175  geolimilem 7178  georeclim 7183  cvgratlem1ALT 7190  fsum0diag 7201  elcncf1i 7214  mulc1cncf 7222  ivthlem6 7229  ivthlem7 7230  ivthlem6OLD 7238  ivthlem7OLD 7239  ef0lem 7260  efaddlem2 7289  efaddlem10 7297  efaddlem13 7300  efaddlem15 7302  efaddlem16 7303  efaddlem18 7305  efaddlem19 7306  efaddlem23 7310  efaddlem25 7312  ef1tllem 7331  ef01tllem1 7333  ef01tllem2 7334  eirrlem2 7339  abspef01tlub 7344  efcnlem2 7368  reeff1o 7376  efi4pt 7385  subcost 7410  abseft 7433  acdc3lem 7436  acdc2lem2 7439  acdc5lem2 7442  acdclem 7444  acdcALT 7446  infxpidmlem7 7509  infxpidmlem8 7510  infxpdom 7522  infmap2 7531  alephsuc3 7535  subbas2 7595  subtop 7596  indistop 7598  distop 7599  fctop 7600  cctop 7602  iooretop 7609  iincld 7629  clscld 7633  clsval2 7635  sscls 7639  ntrss2 7640  ssnei 7674  idcn 7716  cnpco 7719  iscncl 7720  cncnplem4 7727  cnconst 7730  sncld 7737  metdmdm 7758  blssm 7802  ssblex 7808  opnfss 7810  opnin 7821  tgioolem 7866  dscmet 7870  lmconst 7886  iscau3 7890  iscau4 7892  caussi 7905  xplmi 7923  fsumcnlem 7939  lmcau 7946  bcthlem8 7956  bcthlem14 7962  bcthlem18 7966  grpidinv2 8010  grpinv 8019  grpsn 8076  cnid 8079  vc0 8140  vcm 8142  vsfval 8206  nvm 8214  nvnncan 8235  nvdif 8245  nmcnc 8289  sm1cnilem 8294  ipfval 8299  ipval2 8304  ipid 8310  ssps 8336  lno0 8364  nmoxr 8374  nmoge0 8375  nmolb 8379  nmoubi 8380  nmoub3i 8381  nmlnoubi 8401  nmblolbii 8403  isblo3i 8405  blocni 8409  phpar 8427  ubthlem5 8477  minveclem9 8497  minveclem35 8523  minvecdist 8529  htthlem11 8573  pslem 8590  psdmrn 8591  spwval2 8595  spwval3 8596  spwnex3 8597  sinperlem1 8624  sinperlem2 8625  coshalfpip 8637  efifolem5 8660  eff1o 8687  hial0 8907  hial02 8908  bcseq 8925  hlim0 9044  hlimreu 9049  occllem6 9117  occllem7 9118  pjthlem7 9163  pjthlem13 9169  fh1t 9501  osumlem3 9520  osum 9526  hosubid1t 9664  honegnegt 9672  hoeq2t 9697  eigpos 9702  nmopxrt 9733  nmfnxrt 9746  specclt 9765  hhblo 9768  nmoplbt 9771  nmopubt 9772  nmfnlbt 9787  nmfnleubt 9788  elnlfn2t 9792  0cnop 9842  0cnfn 9843  nmopunt 9877  nmbdoplb 9887  nmcopexlem5 9893  nmcoplb 9896  nmophm 9899  lnopcon 9901  nmbdfnlb 9916  nmcfnexlem5 9922  nmcfnlb 9925  lnfncon 9928  cnlnadjlem5 9942  cnlnssadj 9951  adjbdlnt 9954  adjbdlnb 9955  nmopadjlem 9960  adjeq0 9962  nmoptri 9965  nmopco 9966  nmopcoadj 9972  branmfnt 9976  bra11 9979  kbass2t 9988  leop3t 9996  leopmult 10005  leopnmidt 10009  pjbdln 10014  stadd 10111  stadd3 10113  ssmd1 10175  ssmd2 10176  mdslj1 10183  mdslj2 10184  mdslmd1lem1 10189  mdslmd1lem2 10190  csmdsym 10198  elat2 10204  shatomistic 10225  atcvat4 10261  mdsymlem3 10269  mdsymlem6 10272  mdsymlem8 10274  cdj1 10294  infi1 10383  fine 10384  11st22nd 10390  moec 10393  clsrebb 10416  cdrci 10417  homeofval 10439  idhme 10445  hmphsyma 10451  hmphre 10453  hmeogrp 10461  homcard 10462  subsp 10465  qusp 10466  oefil2 10477  fgsb 10480  infi 10484  fgsb2 10485  cnfilca 10487  dtt2 10498  clicls 10502  msr3 10505  msr4 10506  mslb1 10509  2wsms 10510  msra3 10511  cnvtr 10518  1ded 10551  aidm 10563  aidmold 10564  1cat 10572  ishomb 10596  imonclem 10619  ismonc 10620  isfuna 10628

This theorem was proved from axioms:  ax-1 4  ax-mp 7

Copyright terms: Public domain