Theorem mpbir 232

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 229	. 2 ⊢ (𝜓 → 𝜑)
4	1, 3	ax-mp 5	1 ⊢ 𝜑

Syntax hints:   ↔ wb 207

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 208

This theorem is referenced by:  pm5.74ri  273  con4bii  322  imnani  401  mpbir2an  717  imorri  861  orri  868  mpbir3an  1348  xorexmid  1534  tru  1551  had1  1610  nic-mpALT  1679  nic-ax  1680  nic-axALT  1681  nfi  1795  mpgbir  1806  nfxfr  1860  19.35ri  1886  ax5e  1919  ax6ev  1976  sbt  2077  equsb1v  2116  ax13  2383  ax13ALT  2433  moanmo  2626  axi12  2709  axbnd  2710  axexte  2712  axextmo  2715  nulmo  2716  vexw  2723  eqeltri  2835  nfcxfr  2899  neir  2937  neirr  2943  eqnetri  3004  nelir  3041  mprgbir  3060  issetri  3450  moeq  3648  rmoeq  3679  cdeqi  3706  eqsstri  3961  vn0  4273  rmo0  4290  ab0orv  4311  rabnc  4319  reuprg  4635  tpid1  4700  tpid2  4702  mosneq  4773  pwv  4835  uni0OLD  4867  int0  4892  eqbrtri  5093  tr0  5192  trv  5193  zfrep4  5215  axnulALT  5226  0ex  5229  inex1  5245  elpwi2  5263  0elpw  5284  axpow2  5296  dvdemo1  5302  vpwex  5306  zfpair2  5363  prex  5367  exss  5402  brv  5412  opwo0id  5438  moop2  5443  0sn0ep  5522  po0  5543  epse  5600  relxp  5636  rel0  5742  relopabiv  5763  relopabi  5765  relopabiALT  5766  eliunxp  5779  opeliunxp2  5780  dmi  5863  dmep  5865  xpidtr  6072  xpima  6133  dmsn0  6160  cnvsn0  6161  0elon  6365  funmpt  6523  funmpt2  6524  funcnv0  6551  isarep2  6575  fresaunres2  6699  f0  6708  f10d  6801  f1o00  6802  f1oi  6805  f1oiOLD  6806  f1osn  6808  brprcneu  6817  brprcneuALT  6818  opabiotafun  6907  fvopab3ig  6931  opabex  7164  eufnfv  7173  isof1oopb  7269  ncanth  7311  mpofun  7480  reldmmpo  7490  ovid  7497  ovidig  7498  ovidi  7499  ovig  7502  ov3  7519  caovmo  7593  relmptopab  7606  porpss  7670  uniex2  7681  tfinds2  7804  finds  7836  finds2  7838  oprabex  7918  oprabex3  7919  f1stres  7955  f2ndres  7956  relmpoopab  8033  fsplitfpar  8057  poseq  8098  opeliunxp2f  8150  tpos0  8196  issmo  8278  tfrlem6  8311  tfrlem8  8313  tfrlem16  8322  tfr1a  8323  tfr1  8326  tz7.44lem1  8334  seqomlem2  8380  seqomlem3  8381  seqomlem4  8382  fnseqom  8384  ord3  8410  0lt1o  8429  0we1  8431  naddf  8607  eqer  8670  ecopover  8758  mapsnf1o3  8833  ssdomg  8937  en0  8955  en0r  8957  ensn1  8958  0fi  8979  enrefnn  8983  xpcomf1o  8994  map2xp  9075  limensuci  9081  1sdom2  9148  sdom1  9150  unblem4  9195  fidomdm  9234  marypha1lem  9336  hartogslem1  9447  hartogs  9449  card2on  9459  nelaneqOLDOLD  9509  epinid0  9510  ruALT  9514  disjcsn  9515  elnanel  9519  cnvepnep  9520  inf2  9535  inf3lem6  9545  infeq5i  9548  zfinf2  9554  cantnflt  9584  cnfcom  9612  trcl  9640  tz9.1c  9642  tc2  9652  r1funlim  9681  r1fnon  9682  karden  9810  tskwe  9865  cardprclem  9894  pm54.43  9916  r0weon  9925  iunmapdisj  9936  alephfnon  9978  alephfplem4  10020  alephfp  10021  alephval3  10023  kmlem2  10065  dju1dif  10086  ackbij1  10150  ackbij2lem2  10152  ackbij2  10155  infpssrlem3  10218  hsmexlem4  10342  hsmexlem5  10343  ac2  10374  axac3  10377  ac6  10393  axdclem2  10433  dmct  10437  ondomon  10476  alephsucpw  10484  pwcfsdom  10497  cfpwsdom  10498  smobeth  10500  axpowndlem3  10513  zfcndun  10529  zfcndpow  10530  zfcndinf  10532  zfcndac  10533  wunex2  10652  uniwun  10654  wuncval2  10661  grur1  10734  axgroth5  10738  axgroth2  10739  axgroth6  10742  axgroth3  10745  grothtsk  10749  inaprc  10750  ltsopi  10802  dmaddpi  10804  dmmulpi  10805  1lt2pi  10819  nqerf  10844  addnqf  10862  mulnqf  10863  1lt2nq  10887  m1p1sr  11006  m1m1sr  11007  0lt1sr  11009  axaddf  11059  axmulf  11060  ax1cn  11063  subaddrii  11474  ixi  11770  recgt0ii  12053  nn1suc  12187  4div2e2  12337  arch  12425  un0mulcl  12462  pnf0xnn0  12508  3halfnz  12599  nummac  12680  indstr  12857  mnfltpnf  13068  ioof  13391  0nelfz1  13488  fzp1disj  13528  fzp1nel  13556  fzof  13601  fvf1tp  13739  om2uzrani  13905  om2uzf1oi  13906  uzrdglem  13910  uzrdgfni  13911  uzrdg0i  13912  ltwenn  13915  hashgf1o  13924  axdc4uzlem  13936  sq0  14145  irec  14154  facmapnn  14238  hashkf  14285  hashfxnn0  14290  hashf  14291  hash0  14320  prhash2ex  14352  hashsslei  14379  hashxplem  14386  hashbclem  14405  hashf1lem1  14408  tpf1ofv0  14449  tpfo  14453  s1dm  14562  eqs1  14566  ccat2s1p1  14583  cats1un  14674  revs1  14718  0csh0  14746  cshw1  14775  cats1fvn  14811  funcnvs1  14865  pfx2  14900  relexp0g  14975  relexpsucnnr  14978  rtrclreclem1  15010  dfrtrclrec2  15011  rtrclreclem2  15012  rtrclreclem4  15014  dfrtrcl2  15015  climmo  15510  fsumcom2  15727  ackbijnn  15784  incexclem  15792  infcvgaux1i  15813  fprodcom2  15940  bpolylem  16004  bpoly3  16014  bpoly4  16015  efcvgfsum  16042  cos1bnd  16145  cos2bnd  16146  znnen  16170  qnnen  16171  aleph1re  16203  3dvds  16291  n2dvdsm1  16329  divalglem5  16357  flodddiv4  16375  sadcaddlem  16417  sadadd2lem  16419  sadadd3  16421  sadaddlem  16426  lcmf0  16594  lcmfunsnlem2lem1  16598  lcmfunsnlem2  16600  coprmprod  16621  coprmproddvdslem  16622  2prm  16652  3lcm2e6  16693  phicl2  16729  pockthi  16869  unbenlem  16870  prmrec  16884  vdwlem13  16955  vdwnn  16960  ramcl2  16978  prmgapprmo  17024  mod2xnegi  17033  modsubi  17034  structcnvcnv  17114  strleun  17118  setsres  17139  strfv  17164  starvndxnbasendx  17258  starvndxnplusgndx  17259  starvndxnmulrndx  17260  scandxnbasendx  17270  scandxnplusgndx  17271  scandxnmulrndx  17272  vscandxnbasendx  17275  vscandxnplusgndx  17276  vscandxnmulrndx  17277  vscandxnscandx  17278  ipndxnbasendx  17286  ipndxnplusgndx  17287  ipndxnmulrndx  17288  slotsdifipndx  17289  tsetndxnplusgndx  17311  tsetndxnmulrndx  17312  tsetndxnstarvndx  17313  slotstnscsi  17314  plendxnplusgndx  17325  plendxnmulrndx  17326  plendxnscandx  17327  plendxnvscandx  17328  slotsdifplendx  17329  basendxnocndx  17337  plendxnocndx  17338  dsndxnplusgndx  17344  dsndxnmulrndx  17345  slotsdnscsi  17346  dsndxntsetndx  17347  slotsdifdsndx  17348  unifndxntsetndx  17354  slotsdifunifndx  17355  slotsdifplendx2  17370  slotsdifocndx  17371  0rest  17383  firest  17386  restid  17387  prdsval  17409  prdsbas  17411  prdsplusg  17412  prdsmulr  17413  prdsvsca  17414  imasaddfnlem  17483  imasvscafn  17492  2oppchomf  17681  0ssc  17795  0subcat  17796  idfucl  17839  homarel  17994  dmaf  18007  cdaf  18008  setc2ohom  18053  catcfuccl  18076  relxpchom  18138  catcxpccl  18164  oppchofcl  18217  oyoncl  18227  letsr  18550  nulchn  18576  s1chn  18577  chnub  18579  chninf  18592  ex-chn1  18594  mgmidmo  18619  efmndmgm  18844  smndex1ibas  18859  smndex1mgm  18869  smndex1mnd  18872  smndex2dbas  18876  smndex2dnrinv  18877  smndex2hbas  18878  pwmnd  18899  releqg  19141  ga0  19264  psgnunilem3  19462  psgnunilem4  19463  pmtrsn  19485  efgval  19683  efger  19684  efgsval2  19699  efgsp1  19703  efgsfo  19705  efgredleme  19709  efgredlem  19713  efgred  19714  cygctb  19858  gsum2d2lem  19939  gsum2d2  19940  gsumcom2  19941  dprd2d2  20012  pgpfaclem1  20049  gsumle  20111  reldvdsr  20331  fldhmsubc  20757  00lsp  20971  cnfldfun  21361  cnfldfunALT  21362  xrsmgm  21382  pzriprnglem8  21463  pzriprnglem13  21468  pzriprnglem14  21469  pzriprngALT  21470  resubdrg  21583  ocv0  21652  cssval  21657  islinds2  21788  psrvscafval  21923  psrbag0  22038  psdmvr  22157  00ply1bas  22224  ply1plusgfvi  22226  m2detleib  22614  tgdom  22961  tgidm  22963  indistps2ALT  22997  restbas  23141  resttopon  23144  rest0  23152  leordtval2  23195  iocpnfordt  23198  icomnfordt  23199  iooordt  23200  ist1-3  23332  1stcfb  23428  comppfsc  23515  1stckgen  23537  ptbasfi  23564  dfac14  23601  opnfbas  23825  hauspwpwf1  23970  alexsubALT  24034  ptcmplem5  24039  cnextrel  24046  ust0  24203  0met  24349  prdsdsf  24350  prdsxmetlem  24351  prdsmet  24353  prdsbl  24474  qtopbaslem  24741  xrtgioo  24790  xrsdsre  24794  zcld  24797  recld2  24798  reperflem  24802  retopconn  24813  iccpnfcnv  24929  bndth  24943  nmoleub2lem2  25101  zclmncvs  25133  recmet  25308  resscdrg  25343  ishl2  25355  recms  25365  volf  25514  iundisj2  25534  volsup  25541  icombl  25549  ioombl  25550  ismbf3d  25639  0plef  25657  0pledm  25658  itg1ge0  25671  mbfi1fseqlem5  25704  itg2addlem  25743  reldv  25855  limciun  25879  dvexp  25938  dveflem  25964  lhop1lem  25998  lhop  26001  elply2  26179  elplyd  26185  ply1term  26187  ply0  26191  plymullem  26199  qaa  26307  pserulm  26405  pserdvlem2  26411  efcn  26426  sincosq1lem  26479  tangtx  26487  sincos4thpi  26495  pigt3  26500  pige3ALT  26502  efif1olem4  26527  logf1o  26546  relogf1o  26548  log1  26567  loge  26568  logi  26569  relogiso  26580  dvrelog  26619  relogcn  26620  logcn  26629  cxpcn3  26730  resqrtcn  26731  rtprmirr  26742  2logb9irr  26777  leibpi  26924  log2ublem1  26928  birthday  26936  emcllem5  26981  harmonicbnd  26985  harmonicbnd2  26986  harmonicbnd3  26989  lgamgulm2  27017  lgamcvglem  27021  gamf  27024  ppiltx  27158  ppiublem1  27183  ppiub  27185  bclbnd  27261  bpos1lem  27263  bposlem8  27272  lgsquadlem2  27362  2sqlem9  27408  2sqlem10  27409  addsqnreup  27424  chebbnd1  27453  selberg2lem  27531  pntrsumo1  27546  selbergsb  27556  pntpbnd  27569  ltsval2  27638  noxp1o  27645  nosepnelem  27661  noetasuplem2  27716  noetainflem2  27720  0lt1s  27822  addsf  27992  precsexlem1  28217  precsexlem2  28218  precsexlem3  28219  precsexlem4  28220  precsexlem5  28221  precsexlem9  28225  precsexlem10  28226  precsexlem11  28227  elons2  28268  oncutlt  28274  oniso  28281  onswe  28282  onsse  28283  onaddscl  28287  onmulscl  28288  onsbnd  28291  eln0s  28371  0zs  28398  zseo  28432  twocut  28433  0reno  28506  1reno  28507  lngndxnitvndx  28529  istrkg2ld  28546  tgcgr4  28617  ax5seglem7  29022  axlowdimlem4  29032  axlowdimlem6  29034  axlowdimlem7  29035  axlowdimlem10  29038  axlowdimlem13  29041  axlowdimlem16  29044  uhgr0e  29158  uhgr0  29160  upgrbi  29180  umgrbi  29188  usgr0  29330  lfuhgr1v0e  29341  usgrexmpllem  29347  usgrexmpl  29350  griedg0prc  29351  cplgr0  29512  usgrexilem  29527  cffldtocusgr  29534  rgrusgrprc  29676  rusgrprc  29677  rgrprcx  29679  rgrx0ndm  29680  usgr2pthlem  29849  pthdlem2  29854  uspgrn2crct  29894  wwlksnext  29979  clwwlknondisj  30199  0ewlk  30202  0wlk  30204  0pth  30213  1pthdlem1  30223  1trld  30230  wlk2v2elem2  30244  wlk2v2e  30245  upgr3v3e3cycl  30268  upgr4cycl4dv4e  30273  dfconngr1  30276  0conngr  30280  konigsbergumgr  30339  2wspmdisj  30425  2clwwlk2clwwlk  30438  numclwwlk3lem2lem  30471  numclwwlk3lem2  30472  ex-dif  30511  ex-in  30513  ex-eprel  30521  ex-id  30522  ex-fl  30535  ex-mod  30537  ex-hash  30541  ex-fpar  30550  avril1  30551  2bornot2b  30552  0vfval  30695  vsfval  30722  ajmoi  30947  ajfuni  30948  normlem2  31200  norm3adifii  31237  hhip  31266  hlim0  31324  hlimcaui  31325  hlimf  31326  hhssnv  31353  shscli  31406  shsval2i  31476  h1de2i  31642  fh3i  31712  fh4i  31713  cm2mi  31715  qlaxr3i  31725  mayetes3i  31818  ho0f  31840  hoif  31843  hodidi  31876  ho0subi  31884  hosd1i  31911  adjmo  31921  nmopsetn0  31954  nmfnsetn0  31967  funadj  31975  funcnvadj  31982  nmcexi  32115  cnlnadjlem8  32163  nmoptri2i  32188  opsqrlem4  32232  hmopidmchi  32240  pjoci  32269  pjinvari  32280  abrexdomjm  32595  elim2ifim  32633  iundisj2f  32679  rinvf1o  32722  dfcnv2  32767  snct  32804  fzodif2  32883  iundisj2fi  32889  dp2lt10  32962  dp2ltc  32965  dplti  32983  dpgti  32984  dpexpp1  32986  xrge0slmod  33431  isconstr  33920  zarcls  34058  zartopn  34059  xrge0pluscn  34124  qqhre  34204  esumrnmpt2  34252  esumfsup  34254  esumpcvgval  34262  hasheuni  34269  esumcvg  34270  esumcvgsum  34272  esumsup  34273  esum2d  34277  dmsigagen  34328  ldgenpisyslem3  34349  measvuni  34398  voliune  34413  volfiniune  34414  br2base  34453  dya2iocuni  34467  eulerpartlem1  34551  eulerpartlemt  34555  eulerpartgbij  34556  fib0  34583  coinfliprv  34667  ballotlem2  34673  ballotlemic  34691  ballotlem7  34720  ballotth  34722  plymul02  34730  rpsqrtcn  34777  chtvalz  34813  circlemethnat  34825  circlevma  34826  circlemethhgt  34827  hgt750lem  34835  bnj226  34917  bnj1101  34967  bnj110  35040  bnj149  35057  bnj150  35058  bnj151  35059  bnj517  35067  bnj580  35095  bnj865  35105  bnj900  35111  bnj996  35138  bnj1110  35164  bnj1133  35171  bnj1128  35172  bnj1145  35175  bnj1137  35177  bnj1171  35182  bnj1176  35187  axnulALT2  35264  fineqvnttrclse  35305  setinds2regs  35312  tz9.1regs  35315  f1resfz0f1d  35342  subfacp1lem5  35412  subfacp1lem6  35413  kur14lem9  35442  cvmcov2  35503  cvmliftlem1  35513  cvmliftlem4  35516  cvmliftlem5  35517  gonanegoal  35580  satfv0  35586  satfv0fun  35599  fmlan0  35619  gonan0  35620  fmla0disjsuc  35626  ex-sategoelel12  35655  msrfo  35774  problem5  35897  brtpid1  35949  brtpid2  35950  brtpid3  35951  faclimlem1  35971  axextndbi  36030  txprel  36105  relsset  36114  relbigcup  36123  fvbigcup  36128  fnsingle  36145  fvsingle  36146  snelsingles  36148  funimage  36154  fullfunfnv  36174  imagesset  36181  funtransport  36259  colinrel  36285  funray  36368  funline  36370  0hf  36405  neibastop2lem  36588  filnetlem3  36608  nrmo  36638  waj-ax  36642  lukshef-ax2  36643  arg-ax  36644  limsucncmpi  36673  ttctr  36721  dfttc2g  36734  ttcuniun  36738  ttcuni  36741  dfttc4lem2  36757  regsfromregtco  36766  dnizeq0  36781  knoppcnlem8  36806  knoppcnlem11  36809  cnndvlem1  36843  bj-babylob  36915  bj-ax12ssb  36998  bj-nnfnth  37094  bj-snsetex  37316  bj-0eltag  37331  bj-2upln0  37376  bj-2upln1upl  37377  bj-snexg  37387  bj-unexg  37391  bj-adjg1  37396  bj-axseprep  37427  f1omptsnlem  37698  f1omptsn  37699  icoreresf  37714  relowlssretop  37725  relowlpssretop  37726  domalom  37766  matunitlindf  37985  poimirlem3  37990  poimirlem9  37996  poimirlem16  38003  poimirlem17  38004  poimirlem18  38005  poimirlem19  38006  poimirlem20  38007  poimirlem26  38013  mblfinlem1  38024  mblfinlem2  38025  ismblfin  38028  voliunnfl  38031  cnambfre  38035  abrexdom  38097  fdc  38112  cncfres  38132  heibor1lem  38176  grposnOLD  38249  bicontr  38447  an12i  38465  tsim1  38497  ac6s6f  38540  vvdifopab  38632  brcnvrabga  38709  opabf  38743  xrnrel  38749  relqmap  38819  dmsucmap  38835  mopre  38838  relcoels  38881  cnvcosseq  38894  refrelcoss3  38920  refrelcoss2  38921  symrelcoss2  38923  refrelcoss  38970  symrelcoss  39011  n0eldmqs  39099  ax13fromc9  39398  dedths  39454  renegclALT  39455  12gcd5e1  42488  60gcd7e1  42490  lcmineqlem23  42536  dvrelog2  42549  dvrelog3  42550  dvrelog2b  42551  aks4d1p1p6  42558  aks4d1p1p7  42559  aks4d1p1  42561  sticksstones22  42653  sn-axprlem3  42705  acos1half  42835  moxfr  43141  mapfzcons1  43166  diophrw  43208  0dioph  43227  vdioph  43228  rabren3dioph  43260  2nn0ind  43390  rpnnen3  43477  kelac2lem  43509  frlmpwfi  43543  oaordnrex  43740  omnord1ex  43749  oenord1ex  43760  oaomoencom  43762  ifpbiidcor2  43927  iscard4  43977  sqrtcval  44085  resqrtvalex  44089  eliunov2  44123  xphe  44225  0he  44226  he0  44228  snhesn  44230  idhe  44231  frege54cor1c  44359  clsk1independent  44490  neicvgnvor  44560  amgm2d  44642  amgm3d  44643  amgm4d  44644  ismnushort  44745  lhe4.4ex1a  44773  rusbcALT  44882  ipo0  44892  ifr0  44893  vk15.4j  44972  2sb5nd  45004  dfvd1ir  45017  dfvd2anir  45028  dfvd2ir  45030  dfvd3ir  45037  dfvd3anir  45040  iden2  45058  e0bir  45220  uun2221p1  45257  uun2221p2  45258  2sb5ndVD  45353  2sb5ndALT  45375  iunconnlem2  45378  trwf  45403  wfaxext  45437  wfaxpow  45441  wfaxinf2  45445  wfac8prim  45446  permaxinf2lem  45456  nregmodelf1o  45459  fnchoice  45477  unisn0  45502  eliincex  45557  icof  45664  fnmptif  45709  supminfxr  45907  rexanuz2nf  45935  fsumiunss  46020  climlimsupcex  46212  liminfltlimsupex  46224  liminflelimsupcex  46240  xlimrel  46263  xlimfun  46298  resincncf  46318  dvnprodlem3  46391  volioc  46415  volico  46426  dmvolss  46428  volioof  46430  stoweidlem13  46456  stoweidlem34  46477  stirlinglem5  46521  stirlinglem13  46529  stirlingr  46533  fourierdlem42  46592  fourierdlem62  46611  fouriersw  46674  etransc  46726  salexct  46777  salexct2  46782  salgencntex  46786  sge0rnn0  46811  gsumge0cl  46814  sge00  46819  sge0resplit  46849  sge0reuz  46890  omeiunle  46960  0ome  46972  icoresmbl  46986  ovn0lem  47008  ovnhoilem1  47044  hspmbl  47072  nsssmfmbf  47222  mbfpsssmf  47226  smfresal  47231  smfmullem4  47237  smfpimbor1lem1  47241  smfpimbor1lem2  47242  quantgodel  47317  nthrucw  47331  goldratmolem2  47349  lambert0  47350  lamberte  47351  cjnpoly  47352  tannpoly  47353  sinnpoly  47354  aistia  47360  aisfina  47361  aiffnbandciffatnotciffb  47367  axorbciffatcxorb  47368  abnotbtaxb  47378  abnotataxb  47379  eusnsn  47489  aiotaval  47558  aiota0ndef  47560  fundcmpsurinjimaid  47886  ichv  47924  ichf  47925  ichid  47926  icht  47927  ichcircshi  47929  icheq  47937  spr0nelg  47951  m3prm  48070  m7prm  48078  0noddALTV  48180  2noddALTV  48184  341fppr2  48225  9fppr8  48228  nfermltl8rev  48233  nfermltl2rev  48234  nfermltlrev  48235  sbgoldbo  48278  nnsum3primes4  48279  evengpop3  48289  stgr1  48452  usgrexmpl1lem  48512  usgrexmpl1  48513  usgrexmpl1tri  48516  usgrexmpl2lem  48517  usgrexmpl2  48518  usgrexmpl2nb0  48522  usgrexmpl2nb1  48523  usgrexmpl2nb2  48524  usgrexmpl2nb3  48525  usgrexmpl2nb4  48526  usgrexmpl2nb5  48527  gpgedg2ov  48557  gpgedg2iv  48558  gpg5nbgrvtx03starlem1  48559  gpg5nbgrvtx03starlem2  48560  gpg5nbgrvtx03starlem3  48561  gpg5nbgrvtx13starlem1  48562  gpg5nbgrvtx13starlem2  48563  gpg5nbgrvtx13starlem3  48564  gpg5grlim  48584  gpg5grlic  48585  gpgprismgr4cycllem2  48587  gpgprismgr4cycllem7  48592  pg4cyclnex  48618  gpg5edgnedg  48621  grlimedgnedg  48622  oddinmgm  48666  nn0mnd  48670  2zrngamgm  48736  2zrngaabl  48741  2zrngmmgm  48743  2zrngnring  48749  fldhmsubcALTV  48824  eliunxp2  48825  zlmodzxzldeplem  48989  zlmodzxzldep  48995  ldepslinc  49000  rrx2xpreen  49210  rrx2plordisom  49214  line2ylem  49242  line2  49243  line2x  49245  inlinecirc02plem  49277  mosn  49303  mof0  49328  mof0ALT  49330  tposrescnv  49369  tposres3  49371  tposideq2  49379  f1omoOLD  49384  nelsubc3  49561  reldmxpc  49736  reldmprcof1  49871  setc1onsubc  50092  reldmlmd2  50143  reldmcmd2  50144  rellmd  50149  relcmd  50150  ex-gte  50219  empty-surprise  50272  eximp-surprise2  50275  amgmw2d  50294