Theorem mpbir 231

Description: An inference from a biconditional, related to modus ponens. (Contributed by NM, 28-Dec-1992.)

Hypotheses

Ref	Expression
mpbir.min	⊢ 𝜓
mpbir.maj	⊢ (𝜑 ↔ 𝜓)

Assertion

Ref	Expression
mpbir	⊢ 𝜑

Proof of Theorem mpbir

Step	Hyp	Ref	Expression
1		mpbir.min	. 2 ⊢ 𝜓
2		mpbir.maj	. . 3 ⊢ (𝜑 ↔ 𝜓)
3	2	biimpri 228	. 2 ⊢ (𝜓 → 𝜑)
4	1, 3	ax-mp 5	1 ⊢ 𝜑

Syntax hints:   ↔ wb 206

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 207

This theorem is referenced by:  pm5.74ri  272  con4bii  321  imnani  400  mpbir2an  712  imorri  856  orri  863  mpbir3an  1343  xorexmid  1529  tru  1546  had1  1605  nic-mpALT  1674  nic-ax  1675  nic-axALT  1676  nfi  1790  mpgbir  1801  nfxfr  1855  19.35ri  1881  ax5e  1914  ax6ev  1971  sbt  2072  equsb1v  2111  ax13  2380  ax13ALT  2430  moanmo  2623  axi12  2707  axbnd  2708  axexte  2710  axextmo  2713  nulmo  2714  vexw  2721  eqeltri  2833  nfcxfr  2897  neir  2936  neirr  2942  eqnetri  3003  nelir  3040  mprgbir  3059  issetri  3461  moeq  3667  rmoeq  3698  cdeqi  3725  eqsstri  3982  vn0  4299  rmo0  4316  ab0orv  4337  rabnc  4345  reuprg  4662  tpid1  4727  tpid2  4729  mosneq  4800  pwv  4862  uni0OLD  4894  int0  4919  eqbrtri  5121  tr0  5219  trv  5220  zfrep4  5240  axnulALT  5251  0ex  5254  inex1  5264  elpwi2  5282  0elpw  5303  axpow2  5314  dvdemo1  5320  vpwex  5324  zfpair2  5380  prex  5384  exss  5418  brv  5428  opwo0id  5453  moop2  5458  0sn0ep  5536  po0  5557  epse  5614  relxp  5650  rel0  5756  relopabiv  5777  relopabi  5779  relopabiALT  5780  eliunxp  5794  opeliunxp2  5795  dmi  5878  dmep  5880  xpidtr  6087  xpima  6148  dmsn0  6175  cnvsn0  6176  0elon  6380  funmpt  6538  funmpt2  6539  funcnv0  6566  isarep2  6590  fresaunres2  6714  f0  6723  f10d  6816  f1o00  6817  f1oi  6820  f1oiOLD  6821  f1osn  6823  brprcneu  6832  brprcneuALT  6833  opabiotafun  6922  fvopab3ig  6945  opabex  7176  eufnfv  7185  isof1oopb  7281  ncanth  7323  mpofun  7492  reldmmpo  7502  ovid  7509  ovidig  7510  ovidi  7511  ovig  7514  ov3  7531  caovmo  7605  relmptopab  7618  porpss  7682  uniex2  7693  tfinds2  7816  finds  7848  finds2  7850  oprabex  7930  oprabex3  7931  f1stres  7967  f2ndres  7968  relmpoopab  8046  fsplitfpar  8070  poseq  8110  opeliunxp2f  8162  tpos0  8208  issmo  8290  tfrlem6  8323  tfrlem8  8325  tfrlem16  8334  tfr1a  8335  tfr1  8338  tz7.44lem1  8346  seqomlem2  8392  seqomlem3  8393  seqomlem4  8394  fnseqom  8396  ord3  8422  0lt1o  8441  0we1  8443  naddf  8619  eqer  8682  ecopover  8770  mapsnf1o3  8845  ssdomg  8949  en0  8967  en0r  8969  ensn1  8970  0fi  8991  enrefnn  8995  xpcomf1o  9006  map2xp  9087  limensuci  9093  1sdom2  9160  sdom1  9162  unblem4  9207  fidomdm  9246  marypha1lem  9348  hartogslem1  9459  hartogs  9461  card2on  9471  nelaneqOLD  9519  epinid0  9520  ruALT  9523  disjcsn  9524  elnanel  9528  cnvepnep  9529  inf2  9544  inf3lem6  9554  infeq5i  9557  zfinf2  9563  cantnflt  9593  cnfcom  9621  trcl  9649  tz9.1c  9651  tc2  9661  r1funlim  9690  r1fnon  9691  karden  9819  tskwe  9874  cardprclem  9903  pm54.43  9925  r0weon  9934  iunmapdisj  9945  alephfnon  9987  alephfplem4  10029  alephfp  10030  alephval3  10032  kmlem2  10074  dju1dif  10095  ackbij1  10159  ackbij2lem2  10161  ackbij2  10164  infpssrlem3  10227  hsmexlem4  10351  hsmexlem5  10352  ac2  10383  axac3  10386  ac6  10402  axdclem2  10442  dmct  10446  ondomon  10485  alephsucpw  10493  pwcfsdom  10506  cfpwsdom  10507  smobeth  10509  axpowndlem3  10522  zfcndun  10538  zfcndpow  10539  zfcndinf  10541  zfcndac  10542  wunex2  10661  uniwun  10663  wuncval2  10670  grur1  10743  axgroth5  10747  axgroth2  10748  axgroth6  10751  axgroth3  10754  grothtsk  10758  inaprc  10759  ltsopi  10811  dmaddpi  10813  dmmulpi  10814  1lt2pi  10828  nqerf  10853  addnqf  10871  mulnqf  10872  1lt2nq  10896  m1p1sr  11015  m1m1sr  11016  0lt1sr  11018  axaddf  11068  axmulf  11069  ax1cn  11072  subaddrii  11482  ixi  11778  recgt0ii  12060  nn1suc  12179  4div2e2  12322  arch  12410  un0mulcl  12447  pnf0xnn0  12493  3halfnz  12583  nummac  12664  indstr  12841  mnfltpnf  13052  ioof  13375  0nelfz1  13471  fzp1disj  13511  fzp1nel  13539  fzof  13584  fvf1tp  13721  om2uzrani  13887  om2uzf1oi  13888  uzrdglem  13892  uzrdgfni  13893  uzrdg0i  13894  ltwenn  13897  hashgf1o  13906  axdc4uzlem  13918  sq0  14127  irec  14136  facmapnn  14220  hashkf  14267  hashfxnn0  14272  hashf  14273  hash0  14302  prhash2ex  14334  hashsslei  14361  hashxplem  14368  hashbclem  14387  hashf1lem1  14390  tpf1ofv0  14431  tpfo  14435  s1dm  14544  eqs1  14548  ccat2s1p1  14565  cats1un  14656  revs1  14700  0csh0  14728  cshw1  14757  cats1fvn  14793  funcnvs1  14847  pfx2  14882  relexp0g  14957  relexpsucnnr  14960  rtrclreclem1  14992  dfrtrclrec2  14993  rtrclreclem2  14994  rtrclreclem4  14996  dfrtrcl2  14997  climmo  15492  fsumcom2  15709  ackbijnn  15763  incexclem  15771  infcvgaux1i  15792  fprodcom2  15919  bpolylem  15983  bpoly3  15993  bpoly4  15994  efcvgfsum  16021  cos1bnd  16124  cos2bnd  16125  znnen  16149  qnnen  16150  aleph1re  16182  3dvds  16270  n2dvdsm1  16308  divalglem5  16336  flodddiv4  16354  sadcaddlem  16396  sadadd2lem  16398  sadadd3  16400  sadaddlem  16405  lcmf0  16573  lcmfunsnlem2lem1  16577  lcmfunsnlem2  16579  coprmprod  16600  coprmproddvdslem  16601  2prm  16631  3lcm2e6  16671  phicl2  16707  pockthi  16847  unbenlem  16848  prmrec  16862  vdwlem13  16933  vdwnn  16938  ramcl2  16956  prmgapprmo  17002  mod2xnegi  17011  modsubi  17012  structcnvcnv  17092  strleun  17096  setsres  17117  strfv  17142  starvndxnbasendx  17236  starvndxnplusgndx  17237  starvndxnmulrndx  17238  scandxnbasendx  17248  scandxnplusgndx  17249  scandxnmulrndx  17250  vscandxnbasendx  17253  vscandxnplusgndx  17254  vscandxnmulrndx  17255  vscandxnscandx  17256  ipndxnbasendx  17264  ipndxnplusgndx  17265  ipndxnmulrndx  17266  slotsdifipndx  17267  tsetndxnplusgndx  17289  tsetndxnmulrndx  17290  tsetndxnstarvndx  17291  slotstnscsi  17292  plendxnplusgndx  17303  plendxnmulrndx  17304  plendxnscandx  17305  plendxnvscandx  17306  slotsdifplendx  17307  basendxnocndx  17315  plendxnocndx  17316  dsndxnplusgndx  17322  dsndxnmulrndx  17323  slotsdnscsi  17324  dsndxntsetndx  17325  slotsdifdsndx  17326  unifndxntsetndx  17332  slotsdifunifndx  17333  slotsdifplendx2  17348  slotsdifocndx  17349  0rest  17361  firest  17364  restid  17365  prdsval  17387  prdsbas  17389  prdsplusg  17390  prdsmulr  17391  prdsvsca  17392  imasaddfnlem  17461  imasvscafn  17470  2oppchomf  17659  0ssc  17773  0subcat  17774  idfucl  17817  homarel  17972  dmaf  17985  cdaf  17986  setc2ohom  18031  catcfuccl  18054  relxpchom  18116  catcxpccl  18142  oppchofcl  18195  oyoncl  18205  letsr  18528  nulchn  18554  s1chn  18555  chnub  18557  chninf  18570  ex-chn1  18572  mgmidmo  18597  efmndmgm  18822  smndex1ibas  18837  smndex1mgm  18844  smndex1mnd  18847  smndex2dbas  18851  smndex2dnrinv  18852  smndex2hbas  18853  pwmnd  18874  releqg  19116  ga0  19239  psgnunilem3  19437  psgnunilem4  19438  pmtrsn  19460  efgval  19658  efger  19659  efgsval2  19674  efgsp1  19678  efgsfo  19680  efgredleme  19684  efgredlem  19688  efgred  19689  cygctb  19833  gsum2d2lem  19914  gsum2d2  19915  gsumcom2  19916  dprd2d2  19987  pgpfaclem1  20024  gsumle  20086  reldvdsr  20308  fldhmsubc  20730  00lsp  20944  cnfldfun  21335  cnfldfunALT  21336  cnfldfunOLD  21348  cnfldfunALTOLD  21349  xrsmgm  21373  pzriprnglem8  21455  pzriprnglem13  21460  pzriprnglem14  21461  pzriprngALT  21462  resubdrg  21575  ocv0  21644  cssval  21649  islinds2  21780  psrvscafval  21916  psrbag0  22029  psdmvr  22124  00ply1bas  22192  ply1plusgfvi  22194  m2detleib  22587  tgdom  22934  tgidm  22936  indistps2ALT  22970  restbas  23114  resttopon  23117  rest0  23125  leordtval2  23168  iocpnfordt  23171  icomnfordt  23172  iooordt  23173  ist1-3  23305  1stcfb  23401  comppfsc  23488  1stckgen  23510  ptbasfi  23537  dfac14  23574  opnfbas  23798  hauspwpwf1  23943  alexsubALT  24007  ptcmplem5  24012  cnextrel  24019  ust0  24176  0met  24322  prdsdsf  24323  prdsxmetlem  24324  prdsmet  24326  prdsbl  24447  qtopbaslem  24714  xrtgioo  24763  xrsdsre  24767  zcld  24770  recld2  24771  reperflem  24775  retopconn  24786  iccpnfcnv  24910  bndth  24925  nmoleub2lem2  25084  zclmncvs  25116  recmet  25291  resscdrg  25326  ishl2  25338  recms  25348  volf  25498  iundisj2  25518  volsup  25525  icombl  25533  ioombl  25534  ismbf3d  25623  0plef  25641  0pledm  25642  itg1ge0  25655  mbfi1fseqlem5  25688  itg2addlem  25727  reldv  25839  limciun  25863  dvexp  25925  dveflem  25951  lhop1lem  25986  lhop  25989  elply2  26169  elplyd  26175  ply1term  26177  ply0  26181  plymullem  26189  qaa  26299  pserulm  26399  pserdvlem2  26406  efcn  26421  sincosq1lem  26474  tangtx  26482  sincos4thpi  26490  pigt3  26495  pige3ALT  26497  efif1olem4  26522  logf1o  26541  relogf1o  26543  log1  26562  loge  26563  logi  26564  relogiso  26575  dvrelog  26614  relogcn  26615  logcn  26624  cxpcn3  26726  resqrtcn  26727  rtprmirr  26738  2logb9irr  26773  leibpi  26920  log2ublem1  26924  birthday  26932  emcllem5  26978  harmonicbnd  26982  harmonicbnd2  26983  harmonicbnd3  26986  lgamgulm2  27014  lgamcvglem  27018  gamf  27021  ppiltx  27155  ppiublem1  27181  ppiub  27183  bclbnd  27259  bpos1lem  27261  bposlem8  27270  lgsquadlem2  27360  2sqlem9  27406  2sqlem10  27407  addsqnreup  27422  chebbnd1  27451  selberg2lem  27529  pntrsumo1  27544  selbergsb  27554  pntpbnd  27567  ltsval2  27636  noxp1o  27643  nosepnelem  27659  noetasuplem2  27714  noetainflem2  27718  0lt1s  27820  addsf  27990  precsexlem1  28215  precsexlem2  28216  precsexlem3  28217  precsexlem4  28218  precsexlem5  28219  precsexlem9  28223  precsexlem10  28224  precsexlem11  28225  elons2  28266  oncutlt  28272  oniso  28279  onswe  28280  onsse  28281  onaddscl  28285  onmulscl  28286  onsbnd  28289  eln0s  28369  0zs  28396  zseo  28430  twocut  28431  0reno  28504  1reno  28505  lngndxnitvndx  28527  istrkg2ld  28544  tgcgr4  28615  ax5seglem7  29020  axlowdimlem4  29030  axlowdimlem6  29032  axlowdimlem7  29033  axlowdimlem10  29036  axlowdimlem13  29039  axlowdimlem16  29042  uhgr0e  29156  uhgr0  29158  upgrbi  29178  umgrbi  29186  usgr0  29328  lfuhgr1v0e  29339  usgrexmpllem  29345  usgrexmpl  29348  griedg0prc  29349  cplgr0  29510  usgrexilem  29525  cffldtocusgr  29532  cffldtocusgrOLD  29533  rgrusgrprc  29675  rusgrprc  29676  rgrprcx  29678  rgrx0ndm  29679  usgr2pthlem  29848  pthdlem2  29853  uspgrn2crct  29893  wwlksnext  29978  clwwlknondisj  30198  0ewlk  30201  0wlk  30203  0pth  30212  1pthdlem1  30222  1trld  30229  wlk2v2elem2  30243  wlk2v2e  30244  upgr3v3e3cycl  30267  upgr4cycl4dv4e  30272  dfconngr1  30275  0conngr  30279  konigsbergumgr  30338  2wspmdisj  30424  2clwwlk2clwwlk  30437  numclwwlk3lem2lem  30470  numclwwlk3lem2  30471  ex-dif  30510  ex-in  30512  ex-eprel  30520  ex-id  30521  ex-fl  30534  ex-mod  30536  ex-hash  30540  ex-fpar  30549  avril1  30550  2bornot2b  30551  0vfval  30694  vsfval  30721  ajmoi  30946  ajfuni  30947  normlem2  31199  norm3adifii  31236  hhip  31265  hlim0  31323  hlimcaui  31324  hlimf  31325  hhssnv  31352  shscli  31405  shsval2i  31475  h1de2i  31641  fh3i  31711  fh4i  31712  cm2mi  31714  qlaxr3i  31724  mayetes3i  31817  ho0f  31839  hoif  31842  hodidi  31875  ho0subi  31883  hosd1i  31910  adjmo  31920  nmopsetn0  31953  nmfnsetn0  31966  funadj  31974  funcnvadj  31981  nmcexi  32114  cnlnadjlem8  32162  nmoptri2i  32187  opsqrlem4  32231  hmopidmchi  32239  pjoci  32268  pjinvari  32279  abrexdomjm  32594  elim2ifim  32632  iundisj2f  32677  rinvf1o  32720  dfcnv2  32765  snct  32802  fzodif2  32882  iundisj2fi  32888  dp2lt10  32976  dp2ltc  32979  dplti  32997  dpgti  32998  dpexpp1  33000  xrge0slmod  33441  isconstr  33914  zarcls  34052  zartopn  34053  xrge0pluscn  34118  qqhre  34198  esumrnmpt2  34246  esumfsup  34248  esumpcvgval  34256  hasheuni  34263  esumcvg  34264  esumcvgsum  34266  esumsup  34267  esum2d  34271  dmsigagen  34322  ldgenpisyslem3  34343  measvuni  34392  voliune  34407  volfiniune  34408  br2base  34447  dya2iocuni  34461  eulerpartlem1  34545  eulerpartlemt  34549  eulerpartgbij  34550  fib0  34577  coinfliprv  34661  ballotlem2  34667  ballotlemic  34685  ballotlem7  34714  ballotth  34716  plymul02  34724  rpsqrtcn  34771  chtvalz  34807  circlemethnat  34819  circlevma  34820  circlemethhgt  34821  hgt750lem  34829  bnj226  34911  bnj1101  34961  bnj110  35034  bnj149  35051  bnj150  35052  bnj151  35053  bnj517  35061  bnj580  35089  bnj865  35099  bnj900  35105  bnj996  35132  bnj1110  35158  bnj1133  35165  bnj1128  35166  bnj1145  35169  bnj1137  35171  bnj1171  35176  bnj1176  35181  axnulALT2  35258  fineqvnttrclse  35302  setinds2regs  35309  tz9.1regs  35312  f1resfz0f1d  35330  subfacp1lem5  35400  subfacp1lem6  35401  kur14lem9  35430  cvmcov2  35491  cvmliftlem1  35501  cvmliftlem4  35504  cvmliftlem5  35505  gonanegoal  35568  satfv0  35574  satfv0fun  35587  fmlan0  35607  gonan0  35608  fmla0disjsuc  35614  ex-sategoelel12  35643  msrfo  35762  problem5  35885  brtpid1  35937  brtpid2  35938  brtpid3  35939  faclimlem1  35959  axextndbi  36018  txprel  36093  relsset  36102  relbigcup  36111  fvbigcup  36116  fnsingle  36133  fvsingle  36134  snelsingles  36136  funimage  36142  fullfunfnv  36162  imagesset  36169  funtransport  36247  colinrel  36273  funray  36356  funline  36358  0hf  36393  neibastop2lem  36576  filnetlem3  36596  nrmo  36626  waj-ax  36630  lukshef-ax2  36631  arg-ax  36632  limsucncmpi  36661  regsfromregtr  36690  dnizeq0  36697  knoppcnlem8  36722  knoppcnlem11  36725  cnndvlem1  36759  bj-babylob  36829  bj-ax12ssb  36903  bj-nnfnth  36994  bj-snsetex  37211  bj-0eltag  37226  bj-2upln0  37271  bj-2upln1upl  37272  bj-snexg  37282  bj-unexg  37286  bj-adjg1  37291  bj-axseprep  37322  f1omptsnlem  37591  f1omptsn  37592  icoreresf  37607  relowlssretop  37618  relowlpssretop  37619  domalom  37659  matunitlindf  37869  poimirlem3  37874  poimirlem9  37880  poimirlem16  37887  poimirlem17  37888  poimirlem18  37889  poimirlem19  37890  poimirlem20  37891  poimirlem26  37897  mblfinlem1  37908  mblfinlem2  37909  ismblfin  37912  voliunnfl  37915  cnambfre  37919  abrexdom  37981  fdc  37996  cncfres  38016  heibor1lem  38060  grposnOLD  38133  bicontr  38331  an12i  38349  tsim1  38381  ac6s6f  38424  vvdifopab  38516  brcnvrabga  38593  opabf  38627  xrnrel  38633  relqmap  38703  dmsucmap  38719  mopre  38722  relcoels  38765  cnvcosseq  38778  refrelcoss3  38804  refrelcoss2  38805  symrelcoss2  38807  refrelcoss  38854  symrelcoss  38895  n0eldmqs  38983  ax13fromc9  39282  dedths  39338  renegclALT  39339  12gcd5e1  42373  60gcd7e1  42375  lcmineqlem23  42421  dvrelog2  42434  dvrelog3  42435  dvrelog2b  42436  aks4d1p1p6  42443  aks4d1p1p7  42444  aks4d1p1  42446  sticksstones22  42538  sn-axprlem3  42590  acos1half  42728  moxfr  43049  mapfzcons1  43074  diophrw  43116  0dioph  43135  vdioph  43136  rabren3dioph  43172  2nn0ind  43302  rpnnen3  43389  kelac2lem  43421  frlmpwfi  43455  oaordnrex  43652  omnord1ex  43661  oenord1ex  43672  oaomoencom  43674  ifpbiidcor2  43839  iscard4  43889  sqrtcval  43997  resqrtvalex  44001  eliunov2  44035  xphe  44137  0he  44138  he0  44140  snhesn  44142  idhe  44143  frege54cor1c  44271  clsk1independent  44402  neicvgnvor  44472  amgm2d  44554  amgm3d  44555  amgm4d  44556  ismnushort  44657  lhe4.4ex1a  44685  rusbcALT  44794  ipo0  44804  ifr0  44805  vk15.4j  44884  2sb5nd  44916  dfvd1ir  44929  dfvd2anir  44940  dfvd2ir  44942  dfvd3ir  44949  dfvd3anir  44952  iden2  44970  e0bir  45132  uun2221p1  45169  uun2221p2  45170  2sb5ndVD  45265  2sb5ndALT  45287  iunconnlem2  45290  trwf  45315  wfaxext  45349  wfaxpow  45353  wfaxinf2  45357  wfac8prim  45358  permaxinf2lem  45368  nregmodelf1o  45371  fnchoice  45389  unisn0  45414  eliincex  45469  icof  45577  fnmptif  45623  supminfxr  45822  rexanuz2nf  45850  fsumiunss  45935  climlimsupcex  46127  liminfltlimsupex  46139  liminflelimsupcex  46155  xlimrel  46178  xlimfun  46213  resincncf  46233  dvnprodlem3  46306  volioc  46330  volico  46341  dmvolss  46343  volioof  46345  stoweidlem13  46371  stoweidlem34  46392  stirlinglem5  46436  stirlinglem13  46444  stirlingr  46448  fourierdlem42  46507  fourierdlem62  46526  fouriersw  46589  etransc  46641  salexct  46692  salexct2  46697  salgencntex  46701  sge0rnn0  46726  gsumge0cl  46729  sge00  46734  sge0resplit  46764  sge0reuz  46805  omeiunle  46875  0ome  46887  icoresmbl  46901  ovn0lem  46923  ovnhoilem1  46959  hspmbl  46987  nsssmfmbf  47137  mbfpsssmf  47141  smfresal  47146  smfmullem4  47152  smfpimbor1lem1  47156  smfpimbor1lem2  47157  nthrucw  47244  lambert0  47247  lamberte  47248  cjnpoly  47249  tannpoly  47250  sinnpoly  47251  aistia  47257  aisfina  47258  aiffnbandciffatnotciffb  47264  axorbciffatcxorb  47265  abnotbtaxb  47275  abnotataxb  47276  eusnsn  47386  aiotaval  47455  aiota0ndef  47457  fundcmpsurinjimaid  47771  ichv  47809  ichf  47810  ichid  47811  icht  47812  ichcircshi  47814  icheq  47822  spr0nelg  47836  m3prm  47952  m7prm  47960  0noddALTV  48049  2noddALTV  48053  341fppr2  48094  9fppr8  48097  nfermltl8rev  48102  nfermltl2rev  48103  nfermltlrev  48104  sbgoldbo  48147  nnsum3primes4  48148  evengpop3  48158  stgr1  48321  usgrexmpl1lem  48381  usgrexmpl1  48382  usgrexmpl1tri  48385  usgrexmpl2lem  48386  usgrexmpl2  48387  usgrexmpl2nb0  48391  usgrexmpl2nb1  48392  usgrexmpl2nb2  48393  usgrexmpl2nb3  48394  usgrexmpl2nb4  48395  usgrexmpl2nb5  48396  gpgedg2ov  48426  gpgedg2iv  48427  gpg5nbgrvtx03starlem1  48428  gpg5nbgrvtx03starlem2  48429  gpg5nbgrvtx03starlem3  48430  gpg5nbgrvtx13starlem1  48431  gpg5nbgrvtx13starlem2  48432  gpg5nbgrvtx13starlem3  48433  gpg5grlim  48453  gpg5grlic  48454  gpgprismgr4cycllem2  48456  gpgprismgr4cycllem7  48461  pg4cyclnex  48487  gpg5edgnedg  48490  grlimedgnedg  48491  oddinmgm  48535  nn0mnd  48539  2zrngamgm  48605  2zrngaabl  48610  2zrngmmgm  48612  2zrngnring  48618  fldhmsubcALTV  48693  eliunxp2  48694  zlmodzxzldeplem  48858  zlmodzxzldep  48864  ldepslinc  48869  rrx2xpreen  49079  rrx2plordisom  49083  line2ylem  49111  line2  49112  line2x  49114  inlinecirc02plem  49146  mosn  49172  mof0  49197  mof0ALT  49199  tposrescnv  49238  tposres3  49240  tposideq2  49248  f1omoOLD  49253  nelsubc3  49430  reldmxpc  49605  reldmprcof1  49740  setc1onsubc  49961  reldmlmd2  50012  reldmcmd2  50013  rellmd  50018  relcmd  50019  ex-gte  50088  empty-surprise  50141  eximp-surprise2  50144  amgmw2d  50163