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  3449  moeq  3654  rmoeq  3685  cdeqi  3712  eqsstri  3969  vn0  4286  rmo0  4303  ab0orv  4324  rabnc  4332  reuprg  4648  tpid1  4713  tpid2  4715  mosneq  4786  pwv  4848  uni0OLD  4880  int0  4905  eqbrtri  5107  tr0  5205  trv  5206  zfrep4  5228  axnulALT  5239  0ex  5242  inex1  5254  elpwi2  5272  0elpw  5293  axpow2  5304  dvdemo1  5310  vpwex  5314  zfpair2  5371  prex  5375  exss  5410  brv  5420  opwo0id  5445  moop2  5450  0sn0ep  5528  po0  5549  epse  5606  relxp  5642  rel0  5748  relopabiv  5769  relopabi  5771  relopabiALT  5772  eliunxp  5786  opeliunxp2  5787  dmi  5870  dmep  5872  xpidtr  6079  xpima  6140  dmsn0  6167  cnvsn0  6168  0elon  6372  funmpt  6530  funmpt2  6531  funcnv0  6558  isarep2  6582  fresaunres2  6706  f0  6715  f10d  6808  f1o00  6809  f1oi  6812  f1oiOLD  6813  f1osn  6815  brprcneu  6824  brprcneuALT  6825  opabiotafun  6914  fvopab3ig  6937  opabex  7168  eufnfv  7177  isof1oopb  7273  ncanth  7315  mpofun  7484  reldmmpo  7494  ovid  7501  ovidig  7502  ovidi  7503  ovig  7506  ov3  7523  caovmo  7597  relmptopab  7610  porpss  7674  uniex2  7685  tfinds2  7808  finds  7840  finds2  7842  oprabex  7922  oprabex3  7923  f1stres  7959  f2ndres  7960  relmpoopab  8037  fsplitfpar  8061  poseq  8101  opeliunxp2f  8153  tpos0  8199  issmo  8281  tfrlem6  8314  tfrlem8  8316  tfrlem16  8325  tfr1a  8326  tfr1  8329  tz7.44lem1  8337  seqomlem2  8383  seqomlem3  8384  seqomlem4  8385  fnseqom  8387  ord3  8413  0lt1o  8432  0we1  8434  naddf  8610  eqer  8673  ecopover  8761  mapsnf1o3  8836  ssdomg  8940  en0  8958  en0r  8960  ensn1  8961  0fi  8982  enrefnn  8986  xpcomf1o  8997  map2xp  9078  limensuci  9084  1sdom2  9151  sdom1  9153  unblem4  9198  fidomdm  9237  marypha1lem  9339  hartogslem1  9450  hartogs  9452  card2on  9462  nelaneqOLD  9510  epinid0  9511  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  20753  00lsp  20967  cnfldfun  21358  cnfldfunALT  21359  cnfldfunOLD  21371  cnfldfunALTOLD  21372  xrsmgm  21396  pzriprnglem8  21478  pzriprnglem13  21483  pzriprnglem14  21484  pzriprngALT  21485  resubdrg  21598  ocv0  21667  cssval  21672  islinds2  21803  psrvscafval  21937  psrbag0  22050  psdmvr  22145  00ply1bas  22213  ply1plusgfvi  22215  m2detleib  22606  tgdom  22953  tgidm  22955  indistps2ALT  22989  restbas  23133  resttopon  23136  rest0  23144  leordtval2  23187  iocpnfordt  23190  icomnfordt  23191  iooordt  23192  ist1-3  23324  1stcfb  23420  comppfsc  23507  1stckgen  23529  ptbasfi  23556  dfac14  23593  opnfbas  23817  hauspwpwf1  23962  alexsubALT  24026  ptcmplem5  24031  cnextrel  24038  ust0  24195  0met  24341  prdsdsf  24342  prdsxmetlem  24343  prdsmet  24345  prdsbl  24466  qtopbaslem  24733  xrtgioo  24782  xrsdsre  24786  zcld  24789  recld2  24790  reperflem  24794  retopconn  24805  iccpnfcnv  24921  bndth  24935  nmoleub2lem2  25093  zclmncvs  25125  recmet  25300  resscdrg  25335  ishl2  25347  recms  25357  volf  25506  iundisj2  25526  volsup  25533  icombl  25541  ioombl  25542  ismbf3d  25631  0plef  25649  0pledm  25650  itg1ge0  25663  mbfi1fseqlem5  25696  itg2addlem  25735  reldv  25847  limciun  25871  dvexp  25930  dveflem  25956  lhop1lem  25990  lhop  25993  elply2  26171  elplyd  26177  ply1term  26179  ply0  26183  plymullem  26191  qaa  26300  pserulm  26400  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  26725  resqrtcn  26726  rtprmirr  26737  2logb9irr  26772  leibpi  26919  log2ublem1  26923  birthday  26931  emcllem5  26977  harmonicbnd  26981  harmonicbnd2  26982  harmonicbnd3  26985  lgamgulm2  27013  lgamcvglem  27017  gamf  27020  ppiltx  27154  ppiublem1  27179  ppiub  27181  bclbnd  27257  bpos1lem  27259  bposlem8  27268  lgsquadlem2  27358  2sqlem9  27404  2sqlem10  27405  addsqnreup  27420  chebbnd1  27449  selberg2lem  27527  pntrsumo1  27542  selbergsb  27552  pntpbnd  27565  ltsval2  27634  noxp1o  27641  nosepnelem  27657  noetasuplem2  27712  noetainflem2  27716  0lt1s  27818  addsf  27988  precsexlem1  28213  precsexlem2  28214  precsexlem3  28215  precsexlem4  28216  precsexlem5  28217  precsexlem9  28221  precsexlem10  28222  precsexlem11  28223  elons2  28264  oncutlt  28270  oniso  28277  onswe  28278  onsse  28279  onaddscl  28283  onmulscl  28284  onsbnd  28287  eln0s  28367  0zs  28394  zseo  28428  twocut  28429  0reno  28502  1reno  28503  lngndxnitvndx  28525  istrkg2ld  28542  tgcgr4  28613  ax5seglem7  29018  axlowdimlem4  29028  axlowdimlem6  29030  axlowdimlem7  29031  axlowdimlem10  29034  axlowdimlem13  29037  axlowdimlem16  29040  uhgr0e  29154  uhgr0  29156  upgrbi  29176  umgrbi  29184  usgr0  29326  lfuhgr1v0e  29337  usgrexmpllem  29343  usgrexmpl  29346  griedg0prc  29347  cplgr0  29508  usgrexilem  29523  cffldtocusgr  29530  cffldtocusgrOLD  29531  rgrusgrprc  29673  rusgrprc  29674  rgrprcx  29676  rgrx0ndm  29677  usgr2pthlem  29846  pthdlem2  29851  uspgrn2crct  29891  wwlksnext  29976  clwwlknondisj  30196  0ewlk  30199  0wlk  30201  0pth  30210  1pthdlem1  30220  1trld  30227  wlk2v2elem2  30241  wlk2v2e  30242  upgr3v3e3cycl  30265  upgr4cycl4dv4e  30270  dfconngr1  30273  0conngr  30277  konigsbergumgr  30336  2wspmdisj  30422  2clwwlk2clwwlk  30435  numclwwlk3lem2lem  30468  numclwwlk3lem2  30469  ex-dif  30508  ex-in  30510  ex-eprel  30518  ex-id  30519  ex-fl  30532  ex-mod  30534  ex-hash  30538  ex-fpar  30547  avril1  30548  2bornot2b  30549  0vfval  30692  vsfval  30719  ajmoi  30944  ajfuni  30945  normlem2  31197  norm3adifii  31234  hhip  31263  hlim0  31321  hlimcaui  31322  hlimf  31323  hhssnv  31350  shscli  31403  shsval2i  31473  h1de2i  31639  fh3i  31709  fh4i  31710  cm2mi  31712  qlaxr3i  31722  mayetes3i  31815  ho0f  31837  hoif  31840  hodidi  31873  ho0subi  31881  hosd1i  31908  adjmo  31918  nmopsetn0  31951  nmfnsetn0  31964  funadj  31972  funcnvadj  31979  nmcexi  32112  cnlnadjlem8  32160  nmoptri2i  32185  opsqrlem4  32229  hmopidmchi  32237  pjoci  32266  pjinvari  32277  abrexdomjm  32592  elim2ifim  32630  iundisj2f  32675  rinvf1o  32718  dfcnv2  32763  snct  32800  fzodif2  32879  iundisj2fi  32885  dp2lt10  32958  dp2ltc  32961  dplti  32979  dpgti  32980  dpexpp1  32982  xrge0slmod  33423  isconstr  33896  zarcls  34034  zartopn  34035  xrge0pluscn  34100  qqhre  34180  esumrnmpt2  34228  esumfsup  34230  esumpcvgval  34238  hasheuni  34245  esumcvg  34246  esumcvgsum  34248  esumsup  34249  esum2d  34253  dmsigagen  34304  ldgenpisyslem3  34325  measvuni  34374  voliune  34389  volfiniune  34390  br2base  34429  dya2iocuni  34443  eulerpartlem1  34527  eulerpartlemt  34531  eulerpartgbij  34532  fib0  34559  coinfliprv  34643  ballotlem2  34649  ballotlemic  34667  ballotlem7  34696  ballotth  34698  plymul02  34706  rpsqrtcn  34753  chtvalz  34789  circlemethnat  34801  circlevma  34802  circlemethhgt  34803  hgt750lem  34811  bnj226  34893  bnj1101  34943  bnj110  35016  bnj149  35033  bnj150  35034  bnj151  35035  bnj517  35043  bnj580  35071  bnj865  35081  bnj900  35087  bnj996  35114  bnj1110  35140  bnj1133  35147  bnj1128  35148  bnj1145  35151  bnj1137  35153  bnj1171  35158  bnj1176  35163  axnulALT2  35240  fineqvnttrclse  35284  setinds2regs  35291  tz9.1regs  35294  f1resfz0f1d  35312  subfacp1lem5  35382  subfacp1lem6  35383  kur14lem9  35412  cvmcov2  35473  cvmliftlem1  35483  cvmliftlem4  35486  cvmliftlem5  35487  gonanegoal  35550  satfv0  35556  satfv0fun  35569  fmlan0  35589  gonan0  35590  fmla0disjsuc  35596  ex-sategoelel12  35625  msrfo  35744  problem5  35867  brtpid1  35919  brtpid2  35920  brtpid3  35921  faclimlem1  35941  axextndbi  36000  txprel  36075  relsset  36084  relbigcup  36093  fvbigcup  36098  fnsingle  36115  fvsingle  36116  snelsingles  36118  funimage  36124  fullfunfnv  36144  imagesset  36151  funtransport  36229  colinrel  36255  funray  36338  funline  36340  0hf  36375  neibastop2lem  36558  filnetlem3  36578  nrmo  36608  waj-ax  36612  lukshef-ax2  36613  arg-ax  36614  limsucncmpi  36643  ttctr  36691  dfttc2g  36704  ttcuniun  36708  ttcuni  36711  dfttc4lem2  36727  regsfromregtco  36736  dnizeq0  36751  knoppcnlem8  36776  knoppcnlem11  36779  cnndvlem1  36813  bj-babylob  36885  bj-ax12ssb  36968  bj-nnfnth  37064  bj-snsetex  37286  bj-0eltag  37301  bj-2upln0  37346  bj-2upln1upl  37347  bj-snexg  37357  bj-unexg  37361  bj-adjg1  37366  bj-axseprep  37397  f1omptsnlem  37666  f1omptsn  37667  icoreresf  37682  relowlssretop  37693  relowlpssretop  37694  domalom  37734  matunitlindf  37953  poimirlem3  37958  poimirlem9  37964  poimirlem16  37971  poimirlem17  37972  poimirlem18  37973  poimirlem19  37974  poimirlem20  37975  poimirlem26  37981  mblfinlem1  37992  mblfinlem2  37993  ismblfin  37996  voliunnfl  37999  cnambfre  38003  abrexdom  38065  fdc  38080  cncfres  38100  heibor1lem  38144  grposnOLD  38217  bicontr  38415  an12i  38433  tsim1  38465  ac6s6f  38508  vvdifopab  38600  brcnvrabga  38677  opabf  38711  xrnrel  38717  relqmap  38787  dmsucmap  38803  mopre  38806  relcoels  38849  cnvcosseq  38862  refrelcoss3  38888  refrelcoss2  38889  symrelcoss2  38891  refrelcoss  38938  symrelcoss  38979  n0eldmqs  39067  ax13fromc9  39366  dedths  39422  renegclALT  39423  12gcd5e1  42456  60gcd7e1  42458  lcmineqlem23  42504  dvrelog2  42517  dvrelog3  42518  dvrelog2b  42519  aks4d1p1p6  42526  aks4d1p1p7  42527  aks4d1p1  42529  sticksstones22  42621  sn-axprlem3  42673  acos1half  42804  moxfr  43138  mapfzcons1  43163  diophrw  43205  0dioph  43224  vdioph  43225  rabren3dioph  43261  2nn0ind  43391  rpnnen3  43478  kelac2lem  43510  frlmpwfi  43544  oaordnrex  43741  omnord1ex  43750  oenord1ex  43761  oaomoencom  43763  ifpbiidcor2  43928  iscard4  43978  sqrtcval  44086  resqrtvalex  44090  eliunov2  44124  xphe  44226  0he  44227  he0  44229  snhesn  44231  idhe  44232  frege54cor1c  44360  clsk1independent  44491  neicvgnvor  44561  amgm2d  44643  amgm3d  44644  amgm4d  44645  ismnushort  44746  lhe4.4ex1a  44774  rusbcALT  44883  ipo0  44893  ifr0  44894  vk15.4j  44973  2sb5nd  45005  dfvd1ir  45018  dfvd2anir  45029  dfvd2ir  45031  dfvd3ir  45038  dfvd3anir  45041  iden2  45059  e0bir  45221  uun2221p1  45258  uun2221p2  45259  2sb5ndVD  45354  2sb5ndALT  45376  iunconnlem2  45379  trwf  45404  wfaxext  45438  wfaxpow  45442  wfaxinf2  45446  wfac8prim  45447  permaxinf2lem  45457  nregmodelf1o  45460  fnchoice  45478  unisn0  45503  eliincex  45558  icof  45666  fnmptif  45712  supminfxr  45910  rexanuz2nf  45938  fsumiunss  46023  climlimsupcex  46215  liminfltlimsupex  46227  liminflelimsupcex  46243  xlimrel  46266  xlimfun  46301  resincncf  46321  dvnprodlem3  46394  volioc  46418  volico  46429  dmvolss  46431  volioof  46433  stoweidlem13  46459  stoweidlem34  46480  stirlinglem5  46524  stirlinglem13  46532  stirlingr  46536  fourierdlem42  46595  fourierdlem62  46614  fouriersw  46677  etransc  46729  salexct  46780  salexct2  46785  salgencntex  46789  sge0rnn0  46814  gsumge0cl  46817  sge00  46822  sge0resplit  46852  sge0reuz  46893  omeiunle  46963  0ome  46975  icoresmbl  46989  ovn0lem  47011  ovnhoilem1  47047  hspmbl  47075  nsssmfmbf  47225  mbfpsssmf  47229  smfresal  47234  smfmullem4  47240  smfpimbor1lem1  47244  smfpimbor1lem2  47245  nthrucw  47332  lambert0  47347  lamberte  47348  cjnpoly  47349  tannpoly  47350  sinnpoly  47351  aistia  47357  aisfina  47358  aiffnbandciffatnotciffb  47364  axorbciffatcxorb  47365  abnotbtaxb  47375  abnotataxb  47376  eusnsn  47486  aiotaval  47555  aiota0ndef  47557  fundcmpsurinjimaid  47883  ichv  47921  ichf  47922  ichid  47923  icht  47924  ichcircshi  47926  icheq  47934  spr0nelg  47948  m3prm  48067  m7prm  48075  0noddALTV  48177  2noddALTV  48181  341fppr2  48222  9fppr8  48225  nfermltl8rev  48230  nfermltl2rev  48231  nfermltlrev  48232  sbgoldbo  48275  nnsum3primes4  48276  evengpop3  48286  stgr1  48449  usgrexmpl1lem  48509  usgrexmpl1  48510  usgrexmpl1tri  48513  usgrexmpl2lem  48514  usgrexmpl2  48515  usgrexmpl2nb0  48519  usgrexmpl2nb1  48520  usgrexmpl2nb2  48521  usgrexmpl2nb3  48522  usgrexmpl2nb4  48523  usgrexmpl2nb5  48524  gpgedg2ov  48554  gpgedg2iv  48555  gpg5nbgrvtx03starlem1  48556  gpg5nbgrvtx03starlem2  48557  gpg5nbgrvtx03starlem3  48558  gpg5nbgrvtx13starlem1  48559  gpg5nbgrvtx13starlem2  48560  gpg5nbgrvtx13starlem3  48561  gpg5grlim  48581  gpg5grlic  48582  gpgprismgr4cycllem2  48584  gpgprismgr4cycllem7  48589  pg4cyclnex  48615  gpg5edgnedg  48618  grlimedgnedg  48619  oddinmgm  48663  nn0mnd  48667  2zrngamgm  48733  2zrngaabl  48738  2zrngmmgm  48740  2zrngnring  48746  fldhmsubcALTV  48821  eliunxp2  48822  zlmodzxzldeplem  48986  zlmodzxzldep  48992  ldepslinc  48997  rrx2xpreen  49207  rrx2plordisom  49211  line2ylem  49239  line2  49240  line2x  49242  inlinecirc02plem  49274  mosn  49300  mof0  49325  mof0ALT  49327  tposrescnv  49366  tposres3  49368  tposideq2  49376  f1omoOLD  49381  nelsubc3  49558  reldmxpc  49733  reldmprcof1  49868  setc1onsubc  50089  reldmlmd2  50140  reldmcmd2  50141  rellmd  50146  relcmd  50147  ex-gte  50216  empty-surprise  50269  eximp-surprise2  50272  amgmw2d  50291