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  711  imorri  855  orri  862  mpbir3an  1340  xorexmid  1523  tru  1540  had1  1599  nic-mpALT  1668  nic-ax  1669  nic-axALT  1670  nfi  1784  mpgbir  1795  nfxfr  1849  19.35ri  1876  ax5e  1909  ax6ev  1966  sbt  2063  equsb1v  2102  ax13  2377  ax13ALT  2427  moanmo  2619  axi12  2703  axbnd  2704  axexte  2706  axextmo  2709  nulmo  2710  vexw  2717  eqeltri  2834  nfcxfr  2900  neir  2940  neirr  2946  eqnetri  3008  nelir  3046  mprgbir  3065  cbvrexdva2OLD  3347  issetri  3496  moeq  3715  rmoeq  3746  cdeqi  3773  eqsstri  4029  3sstr4i  4038  rmo0  4367  rabnc  4396  reuprg  4707  tpid1  4772  tpid2  4774  mosneq  4846  pwv  4908  uni0  4939  int0  4966  eqbrtri  5168  tr0  5277  trv  5278  zfrep4  5298  axnulALT  5309  0ex  5312  inex1  5322  elpwi2  5340  0elpw  5361  axpow2  5372  axpow3  5373  dvdemo1  5378  vpwex  5382  zfpair2  5438  exss  5473  brv  5482  opwo0id  5506  moop2  5511  0sn0ep  5592  po0  5613  epse  5670  relxp  5706  rel0  5811  relopabiv  5832  relopabi  5834  relopabiALT  5835  eliunxp  5850  opeliunxp2  5851  dmi  5934  dmep  5936  xpidtr  6144  xpima  6203  dmsn0  6230  cnvsn0  6231  0elon  6439  funmpt  6605  funmpt2  6606  funcnv0  6633  isarep2  6658  fresaunres2  6780  f0  6789  f10d  6882  f1o00  6883  f1oi  6886  f1osn  6888  brprcneu  6896  brprcneuALT  6897  opabiotafun  6988  fvopab3ig  7011  opabex  7239  eufnfv  7248  isof1oopb  7344  ncanth  7385  mpofun  7556  reldmmpo  7566  ovid  7573  ovidig  7574  ovidi  7575  ovig  7578  ov3  7595  caovmo  7669  relmptopab  7682  porpss  7745  uniex2  7756  tfinds2  7884  finds  7918  finds2  7920  oprabex  7999  oprabex3  8000  f1stres  8036  f2ndres  8037  relmpoopab  8117  fsplitfpar  8141  poseq  8181  opeliunxp2f  8233  tpos0  8279  wfrrelOLD  8352  wfrlem14OLD  8360  wfrlem16OLD  8362  issmo  8386  tfrlem6  8420  tfrlem8  8422  tfrlem16  8431  tfr1a  8432  tfr1  8435  tz7.44lem1  8443  seqomlem2  8489  seqomlem3  8490  seqomlem4  8491  fnseqom  8493  ord3  8521  0lt1o  8540  0we1  8542  naddf  8717  eqer  8779  ecopover  8859  mapsnf1o3  8933  ssdomg  9038  en0  9056  en0r  9058  ensn1  9059  0fi  9080  snfiOLD  9082  enrefnn  9085  xpcomf1o  9099  map2xp  9185  limensuci  9191  1sdom2  9273  sdom1  9275  sdom1OLD  9276  unblem4  9328  fidomdm  9371  marypha1lem  9470  hartogslem1  9579  hartogs  9581  card2on  9591  nelaneq  9636  epinid0  9637  ruALT  9640  disjcsn  9641  elnanel  9644  cnvepnep  9645  inf2  9660  inf3lem6  9670  infeq5i  9673  zfinf2  9679  cantnflt  9709  cnfcom  9737  trcl  9765  tz9.1c  9767  tc2  9779  r1funlim  9803  r1fnon  9804  karden  9932  tskwe  9987  cardprclem  10016  pm54.43  10038  r0weon  10049  iunmapdisj  10060  alephfnon  10102  alephfplem4  10144  alephfp  10145  alephval3  10147  kmlem2  10189  dju1dif  10210  ackbij1  10274  ackbij2lem2  10276  ackbij2  10279  infpssrlem3  10342  hsmexlem4  10466  hsmexlem5  10467  ac2  10498  axac3  10501  ac6  10517  axdclem2  10557  dmct  10561  ondomon  10600  alephsucpw  10607  pwcfsdom  10620  cfpwsdom  10621  smobeth  10623  axpowndlem3  10636  zfcndun  10652  zfcndpow  10653  zfcndinf  10655  zfcndac  10656  wunex2  10775  uniwun  10777  wuncval2  10784  grur1  10857  axgroth5  10861  axgroth2  10862  axgroth6  10865  axgroth3  10868  grothtsk  10872  inaprc  10873  ltsopi  10925  dmaddpi  10927  dmmulpi  10928  1lt2pi  10942  nqerf  10967  addnqf  10985  mulnqf  10986  1lt2nq  11010  m1p1sr  11129  m1m1sr  11130  0lt1sr  11132  axaddf  11182  axmulf  11183  ax1cn  11186  subaddrii  11595  ixi  11889  recgt0ii  12171  nn1suc  12285  neg1lt0  12380  4d2e2  12433  arch  12520  un0mulcl  12557  pnf0xnn0  12603  3halfnz  12694  nummac  12775  indstr  12955  mnfltpnf  13165  ioof  13483  0nelfz1  13579  fzp1disj  13619  fzp1nel  13647  fzof  13692  fvf1tp  13825  om2uzrani  13989  om2uzf1oi  13990  uzrdglem  13994  uzrdgfni  13995  uzrdg0i  13996  ltwenn  13999  hashgf1o  14008  axdc4uzlem  14020  sq0  14227  irec  14236  facmapnn  14320  hashkf  14367  hashfxnn0  14372  hashf  14373  hash0  14402  prhash2ex  14434  hashsslei  14461  hashxplem  14468  hashbclem  14487  hashf1lem1  14490  tpf1ofv0  14531  tpfo  14535  s1dm  14642  eqs1  14646  ccat2s1p1  14663  cats1un  14755  revs1  14799  0csh0  14827  cshw1  14856  cats1fvn  14893  funcnvs1  14947  pfx2  14982  relexp0g  15057  relexpsucnnr  15060  rtrclreclem1  15092  dfrtrclrec2  15093  rtrclreclem2  15094  rtrclreclem4  15096  dfrtrcl2  15097  climmo  15589  fsumcom2  15806  ackbijnn  15860  incexclem  15868  infcvgaux1i  15889  fprodcom2  16016  bpolylem  16080  bpoly3  16090  bpoly4  16091  efcvgfsum  16118  cos1bnd  16219  cos2bnd  16220  znnen  16244  qnnen  16245  aleph1re  16277  3dvds  16364  n2dvdsm1  16402  divalglem5  16430  flodddiv4  16448  sadcaddlem  16490  sadadd2lem  16492  sadadd3  16494  sadaddlem  16499  lcmf0  16667  lcmfunsnlem2lem1  16671  lcmfunsnlem2  16673  coprmprod  16694  coprmproddvdslem  16695  2prm  16725  3lcm2e6  16765  phicl2  16801  pockthi  16940  unbenlem  16941  prmrec  16955  vdwlem13  17026  vdwnn  17031  ramcl2  17049  prmgapprmo  17095  mod2xnegi  17104  modsubi  17105  structcnvcnv  17186  strleun  17190  setsres  17211  strfv  17237  starvndxnbasendx  17349  starvndxnplusgndx  17350  starvndxnmulrndx  17351  scandxnbasendx  17361  scandxnplusgndx  17362  scandxnmulrndx  17363  vscandxnbasendx  17366  vscandxnplusgndx  17367  vscandxnmulrndx  17368  vscandxnscandx  17369  ipndxnbasendx  17377  ipndxnplusgndx  17378  ipndxnmulrndx  17379  slotsdifipndx  17380  tsetndxnplusgndx  17402  tsetndxnmulrndx  17403  tsetndxnstarvndx  17404  slotstnscsi  17405  plendxnplusgndx  17416  plendxnmulrndx  17417  plendxnscandx  17418  plendxnvscandx  17419  slotsdifplendx  17420  basendxnocndx  17428  plendxnocndx  17429  dsndxnplusgndx  17435  dsndxnmulrndx  17436  slotsdnscsi  17437  dsndxntsetndx  17438  slotsdifdsndx  17439  unifndxntsetndx  17445  slotsdifunifndx  17446  slotsdifplendx2  17462  slotsdifocndx  17463  0rest  17475  firest  17478  restid  17479  prdsval  17501  prdsbas  17503  prdsplusg  17504  prdsmulr  17505  prdsvsca  17506  imasaddfnlem  17574  imasvscafn  17583  oppchomfvalOLD  17759  oppcbasOLD  17764  2oppchomf  17770  rescbasOLD  17877  resccoOLD  17881  rescabsOLD  17883  0ssc  17887  0subcat  17888  idfucl  17931  homarel  18089  dmaf  18102  cdaf  18103  setc2ohom  18148  catcfuccl  18172  catcfucclOLD  18173  relxpchom  18236  catcxpccl  18262  catcxpcclOLD  18263  oppchofcl  18316  oyoncl  18326  odubasOLD  18348  letsr  18650  mgmidmo  18685  efmndmgm  18910  smndex1ibas  18925  smndex1mgm  18932  smndex1mnd  18935  smndex2dbas  18939  smndex2dnrinv  18940  smndex2hbas  18941  pwmnd  18962  releqg  19205  ga0  19328  oppglemOLD  19381  psgnunilem3  19528  psgnunilem4  19529  pmtrsn  19551  efgval  19749  efger  19750  efgsval2  19765  efgsp1  19769  efgsfo  19771  efgredleme  19775  efgredlem  19779  efgred  19780  cygctb  19924  gsum2d2lem  20005  gsum2d2  20006  gsumcom2  20007  dprd2d2  20078  pgpfaclem1  20115  mgplemOLD  20156  mgpressOLD  20167  opprlemOLD  20356  reldvdsr  20376  fldhmsubc  20802  00lsp  20996  sralemOLD  21193  srascaOLD  21201  sravscaOLD  21203  cnfldfun  21395  cnfldfunALT  21396  cnfldfunOLD  21408  cnfldfunALTOLD  21409  cnfldfunALTOLDOLD  21410  xrsmgm  21436  pzriprnglem8  21516  pzriprnglem13  21521  pzriprnglem14  21522  pzriprngALT  21523  znbaslemOLD  21571  resubdrg  21643  ocv0  21712  cssval  21717  thlbasOLD  21732  thlleOLD  21734  islinds2  21850  psrvscafval  21985  opsrbaslemOLD  22085  psrbag0  22103  00ply1bas  22256  ply1plusgfvi  22258  matscaOLD  22435  m2detleib  22652  tgdom  23000  tgidm  23002  indistps2ALT  23037  restbas  23181  resttopon  23184  rest0  23192  leordtval2  23235  iocpnfordt  23238  icomnfordt  23239  iooordt  23240  ist1-3  23372  1stcfb  23468  comppfsc  23555  1stckgen  23577  ptbasfi  23604  dfac14  23641  opnfbas  23865  hauspwpwf1  24010  alexsubALT  24074  ptcmplem5  24079  cnextrel  24086  ust0  24243  tuslemOLD  24291  0met  24391  prdsdsf  24392  prdsxmetlem  24393  prdsmet  24395  setsmsbasOLD  24501  setsmsdsOLD  24503  prdsbl  24519  tngdsOLD  24684  qtopbaslem  24794  xrtgioo  24841  xrsdsre  24845  zcld  24848  recld2  24849  reperflem  24853  retopconn  24864  iccpnfcnv  24988  bndth  25003  nmoleub2lem2  25162  zclmncvs  25195  recmet  25370  resscdrg  25405  ishl2  25417  recms  25427  volf  25577  iundisj2  25597  volsup  25604  icombl  25612  ioombl  25613  ismbf3d  25702  0plef  25720  0pledm  25721  itg1ge0  25734  mbfi1fseqlem5  25768  itg2addlem  25807  reldv  25919  limciun  25943  dvexp  26005  dveflem  26031  lhop1lem  26066  lhop  26069  elply2  26249  elplyd  26255  ply1term  26257  ply0  26261  plymullem  26269  qaa  26379  pserulm  26479  pserdvlem2  26486  efcn  26501  sincosq1lem  26553  tangtx  26561  sincos4thpi  26569  pigt3  26574  pige3ALT  26576  efif1olem4  26601  logf1o  26620  relogf1o  26622  log1  26641  loge  26642  logi  26643  relogiso  26654  dvrelog  26693  relogcn  26694  logcn  26703  cxpcn3  26805  resqrtcn  26806  rtprmirr  26817  2logb9irr  26852  leibpi  26999  log2ublem1  27003  birthday  27011  emcllem5  27057  harmonicbnd  27061  harmonicbnd2  27062  harmonicbnd3  27065  lgamgulm2  27093  lgamcvglem  27097  gamf  27100  ppiltx  27234  ppiublem1  27260  ppiub  27262  bclbnd  27338  bpos1lem  27340  bposlem8  27349  lgsquadlem2  27439  2sqlem9  27485  2sqlem10  27486  addsqnreup  27501  chebbnd1  27530  selberg2lem  27608  pntrsumo1  27623  selbergsb  27633  pntpbnd  27646  sltval2  27715  noxp1o  27722  nosepnelem  27738  noetasuplem2  27793  noetainflem2  27797  0slt1s  27888  addsf  28029  precsexlem1  28245  precsexlem2  28246  precsexlem3  28247  precsexlem4  28248  precsexlem5  28249  precsexlem9  28253  precsexlem10  28254  precsexlem11  28255  elons2  28295  onaddscl  28300  onmulscl  28301  eln0s  28372  0zs  28388  zseo  28420  nohalf  28421  lngndxnitvndx  28465  istrkg2ld  28482  tgcgr4  28553  ttgvalOLD  28898  ttglemOLD  28900  cchhllemOLD  28916  ax5seglem7  28964  axlowdimlem4  28974  axlowdimlem6  28976  axlowdimlem7  28977  axlowdimlem10  28980  axlowdimlem13  28983  axlowdimlem16  28986  uhgr0e  29102  uhgr0  29104  upgrbi  29124  umgrbi  29132  usgr0  29274  lfuhgr1v0e  29285  usgrexmpllem  29291  usgrexmpl  29294  griedg0prc  29295  cplgr0  29456  usgrexilem  29471  cffldtocusgr  29478  cffldtocusgrOLD  29479  rgrusgrprc  29621  rusgrprc  29622  rgrprcx  29624  rgrx0ndm  29625  usgr2pthlem  29795  pthdlem2  29800  uspgrn2crct  29837  wwlksnext  29922  clwwlknondisj  30139  0ewlk  30142  0wlk  30144  0pth  30153  1pthdlem1  30163  1trld  30170  wlk2v2elem2  30184  wlk2v2e  30185  upgr3v3e3cycl  30208  upgr4cycl4dv4e  30213  dfconngr1  30216  0conngr  30220  konigsbergumgr  30279  2wspmdisj  30365  2clwwlk2clwwlk  30378  numclwwlk3lem2lem  30411  numclwwlk3lem2  30412  ex-dif  30451  ex-in  30453  ex-eprel  30461  ex-id  30462  ex-fl  30475  ex-mod  30477  ex-hash  30481  ex-fpar  30490  avril1  30491  2bornot2b  30492  0vfval  30634  vsfval  30661  ajmoi  30886  ajfuni  30887  normlem2  31139  norm3adifii  31176  hhip  31205  hlim0  31263  hlimcaui  31264  hlimf  31265  hhssnv  31292  shscli  31345  shsval2i  31415  h1de2i  31581  fh3i  31651  fh4i  31652  cm2mi  31654  qlaxr3i  31664  mayetes3i  31757  ho0f  31779  hoif  31782  hodidi  31815  ho0subi  31823  hosd1i  31850  adjmo  31860  nmopsetn0  31893  nmfnsetn0  31906  funadj  31914  funcnvadj  31921  nmcexi  32054  cnlnadjlem8  32102  nmoptri2i  32127  opsqrlem4  32171  hmopidmchi  32179  pjoci  32208  pjinvari  32219  abrexdomjm  32534  elim2ifim  32565  iundisj2f  32609  rinvf1o  32646  dfcnv2  32692  snct  32730  fzodif2  32799  iundisj2fi  32804  dp2lt10  32850  dp2ltc  32853  dplti  32871  dpgti  32872  dpexpp1  32874  chnub  32985  gsumle  33083  xrge0slmod  33355  zarcls  33834  zartopn  33835  xrge0pluscn  33900  zlmdsOLD  33923  zlmtsetOLD  33925  qqhre  33982  esumrnmpt2  34048  esumfsup  34050  esumpcvgval  34058  hasheuni  34065  esumcvg  34066  esumcvgsum  34068  esumsup  34069  esum2d  34073  dmsigagen  34124  ldgenpisyslem3  34145  measvuni  34194  voliune  34209  volfiniune  34210  br2base  34250  dya2iocuni  34264  eulerpartlem1  34348  eulerpartlemt  34352  eulerpartgbij  34353  fib0  34380  coinfliprv  34463  ballotlem2  34469  ballotlemic  34487  ballotlem7  34516  ballotth  34518  plymul02  34539  rpsqrtcn  34586  chtvalz  34622  circlemethnat  34634  circlevma  34635  circlemethhgt  34636  hgt750lem  34644  bnj226  34726  bnj1101  34776  bnj110  34850  bnj149  34867  bnj150  34868  bnj151  34869  bnj517  34877  bnj580  34905  bnj865  34915  bnj900  34921  bnj996  34948  bnj1110  34974  bnj1133  34981  bnj1128  34982  bnj1145  34985  bnj1137  34987  bnj1171  34992  bnj1176  34997  f1resfz0f1d  35097  subfacp1lem5  35168  subfacp1lem6  35169  kur14lem9  35198  cvmcov2  35259  cvmliftlem1  35269  cvmliftlem4  35272  cvmliftlem5  35273  gonanegoal  35336  satfv0  35342  satfv0fun  35355  fmlan0  35375  gonan0  35376  fmla0disjsuc  35382  ex-sategoelel12  35411  msrfo  35530  problem5  35653  brtpid1  35700  brtpid2  35701  brtpid3  35702  faclimlem1  35722  axextndbi  35785  txprel  35860  relsset  35869  relbigcup  35878  fvbigcup  35883  fnsingle  35900  fvsingle  35901  snelsingles  35903  funimage  35909  fullfunfnv  35927  imagesset  35934  funtransport  36012  colinrel  36038  funray  36121  funline  36123  0hf  36158  neibastop2lem  36342  filnetlem3  36362  nrmo  36392  waj-ax  36396  lukshef-ax2  36397  arg-ax  36398  limsucncmpi  36427  dnizeq0  36457  knoppcnlem8  36482  knoppcnlem11  36485  cnndvlem1  36519  bj-babylob  36586  bj-ax12ssb  36640  bj-nnfnth  36725  bj-snsetex  36945  bj-0eltag  36960  bj-2upln0  37005  bj-2upln1upl  37006  bj-snexg  37016  bj-unexg  37020  bj-adjg1  37025  f1omptsnlem  37318  f1omptsn  37319  icoreresf  37334  relowlssretop  37345  relowlpssretop  37346  domalom  37386  matunitlindf  37604  poimirlem3  37609  poimirlem9  37615  poimirlem16  37622  poimirlem17  37623  poimirlem18  37624  poimirlem19  37625  poimirlem20  37626  poimirlem26  37632  mblfinlem1  37643  mblfinlem2  37644  ismblfin  37647  voliunnfl  37650  cnambfre  37654  abrexdom  37716  fdc  37731  cncfres  37751  heibor1lem  37795  grposnOLD  37868  bicontr  38066  an12i  38084  tsim1  38116  ac6s6f  38159  vvdifopab  38241  brcnvrabga  38323  opabf  38349  xrnrel  38354  relcoels  38405  cnvcosseq  38418  refrelcoss3  38444  refrelcoss2  38445  symrelcoss2  38447  refrelcoss  38504  symrelcoss  38541  n0eldmqs  38629  ax13fromc9  38887  dedths  38943  renegclALT  38944  hlhilslemOLD  41921  12gcd5e1  41984  60gcd7e1  41986  lcmineqlem23  42032  dvrelog2  42045  dvrelog3  42046  dvrelog2b  42047  aks4d1p1p6  42054  aks4d1p1p7  42055  aks4d1p1  42057  sticksstones22  42149  2xp3dxp2ge1d  42222  sn-axprlem3  42234  acos1half  42366  moxfr  42679  mapfzcons1  42704  diophrw  42746  0dioph  42765  vdioph  42766  rabren3dioph  42802  2nn0ind  42933  rpnnen3  43020  kelac2lem  43052  frlmpwfi  43086  oaordnrex  43284  omnord1ex  43293  oenord1ex  43304  oaomoencom  43306  ifpbiidcor2  43472  iscard4  43522  sqrtcval  43630  resqrtvalex  43634  eliunov2  43668  xphe  43770  0he  43771  he0  43773  snhesn  43775  idhe  43776  frege54cor1c  43904  clsk1independent  44035  neicvgnvor  44105  amgm2d  44187  amgm3d  44188  amgm4d  44189  ismnushort  44296  lhe4.4ex1a  44324  rusbcALT  44434  ipo0  44444  ifr0  44445  vk15.4j  44525  2sb5nd  44557  dfvd1ir  44570  dfvd2anir  44581  dfvd2ir  44583  dfvd3ir  44590  dfvd3anir  44593  iden2  44611  e0bir  44774  uun2221p1  44811  uun2221p2  44812  2sb5ndVD  44907  2sb5ndALT  44929  iunconnlem2  44932  trwf  44936  wfaxext  44948  fnchoice  44966  unisn0  44993  eliincex  45049  icof  45161  fnmptif  45210  supminfxr  45413  rexanuz2nf  45442  fsumiunss  45530  climlimsupcex  45724  liminfltlimsupex  45736  liminflelimsupcex  45752  xlimrel  45775  xlimfun  45810  resincncf  45830  dvnprodlem3  45903  volioc  45927  volico  45938  dmvolss  45940  volioof  45942  stoweidlem13  45968  stoweidlem34  45989  stirlinglem5  46033  stirlinglem13  46041  stirlingr  46045  fourierdlem42  46104  fourierdlem62  46123  fouriersw  46186  etransc  46238  salexct  46289  salexct2  46294  salgencntex  46298  sge0rnn0  46323  gsumge0cl  46326  sge00  46331  sge0resplit  46361  sge0reuz  46402  omeiunle  46472  0ome  46484  icoresmbl  46498  ovn0lem  46520  ovnhoilem1  46556  hspmbl  46584  nsssmfmbf  46734  mbfpsssmf  46738  smfresal  46743  smfmullem4  46749  smfpimbor1lem1  46753  smfpimbor1lem2  46754  aistia  46846  aisfina  46847  aiffnbandciffatnotciffb  46853  axorbciffatcxorb  46854  abnotbtaxb  46864  abnotataxb  46865  eusnsn  46975  aiotaval  47044  aiota0ndef  47046  fundcmpsurinjimaid  47335  ichv  47373  ichf  47374  ichid  47375  icht  47376  ichcircshi  47378  icheq  47386  spr0nelg  47400  m3prm  47516  m7prm  47524  0noddALTV  47613  2noddALTV  47617  341fppr2  47658  9fppr8  47661  nfermltl8rev  47666  nfermltl2rev  47667  nfermltlrev  47668  sbgoldbo  47711  nnsum3primes4  47712  evengpop3  47722  stgr1  47863  usgrexmpl1lem  47915  usgrexmpl1  47916  usgrexmpl1tri  47919  usgrexmpl2lem  47920  usgrexmpl2  47921  usgrexmpl2nb0  47925  usgrexmpl2nb1  47926  usgrexmpl2nb2  47927  usgrexmpl2nb3  47928  usgrexmpl2nb4  47929  usgrexmpl2nb5  47930  gpg5nbgrvtx03starlem1  47958  gpg5nbgrvtx03starlem2  47959  gpg5nbgrvtx03starlem3  47960  gpg5nbgrvtx13starlem1  47961  gpg5nbgrvtx13starlem2  47962  gpg5nbgrvtx13starlem3  47963  gpg5grlic  47974  oddinmgm  48018  nn0mnd  48022  2zrngamgm  48088  2zrngaabl  48093  2zrngmmgm  48095  2zrngnring  48101  fldhmsubcALTV  48176  eliunxp2  48178  zlmodzxzldeplem  48343  zlmodzxzldep  48349  ldepslinc  48354  rrx2xpreen  48568  rrx2plordisom  48572  line2ylem  48600  line2  48601  line2x  48603  inlinecirc02plem  48635  mosn  48660  mof0  48667  mof0ALT  48669  f1omo  48690  prstclevalOLD  48869  prstcocvalOLD  48872  ex-gte  48959  empty-surprise  49012  eximp-surprise2  49015  amgmw2d  49034