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  1342  xorexmid  1528  tru  1545  had1  1604  nic-mpALT  1673  nic-ax  1674  nic-axALT  1675  nfi  1789  mpgbir  1800  nfxfr  1854  19.35ri  1880  ax5e  1913  ax6ev  1970  sbt  2071  equsb1v  2110  ax13  2379  ax13ALT  2429  moanmo  2622  axi12  2706  axbnd  2707  axexte  2709  axextmo  2712  nulmo  2713  vexw  2720  eqeltri  2832  nfcxfr  2896  neir  2935  neirr  2941  eqnetri  3002  nelir  3039  mprgbir  3058  issetri  3459  moeq  3665  rmoeq  3696  cdeqi  3723  eqsstri  3980  vn0  4297  rmo0  4314  ab0orv  4335  rabnc  4343  reuprg  4660  tpid1  4725  tpid2  4727  mosneq  4798  pwv  4860  uni0OLD  4892  int0  4917  eqbrtri  5119  tr0  5217  trv  5218  zfrep4  5238  axnulALT  5249  0ex  5252  inex1  5262  elpwi2  5280  0elpw  5301  axpow2  5312  dvdemo1  5318  vpwex  5322  zfpair2  5378  exss  5411  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  7166  eufnfv  7175  isof1oopb  7271  ncanth  7313  mpofun  7482  reldmmpo  7492  ovid  7499  ovidig  7500  ovidi  7501  ovig  7504  ov3  7521  caovmo  7595  relmptopab  7608  porpss  7672  uniex2  7683  tfinds2  7806  finds  7838  finds2  7840  oprabex  7920  oprabex3  7921  f1stres  7957  f2ndres  7958  relmpoopab  8036  fsplitfpar  8060  poseq  8100  opeliunxp2f  8152  tpos0  8198  issmo  8280  tfrlem6  8313  tfrlem8  8315  tfrlem16  8324  tfr1a  8325  tfr1  8328  tz7.44lem1  8336  seqomlem2  8382  seqomlem3  8383  seqomlem4  8384  fnseqom  8386  ord3  8412  0lt1o  8431  0we1  8433  naddf  8609  eqer  8671  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  nelaneqOLD  9507  epinid0  9508  ruALT  9511  disjcsn  9512  elnanel  9516  cnvepnep  9517  inf2  9532  inf3lem6  9542  infeq5i  9545  zfinf2  9551  cantnflt  9581  cnfcom  9609  trcl  9637  tz9.1c  9639  tc2  9649  r1funlim  9678  r1fnon  9679  karden  9807  tskwe  9862  cardprclem  9891  pm54.43  9913  r0weon  9922  iunmapdisj  9933  alephfnon  9975  alephfplem4  10017  alephfp  10018  alephval3  10020  kmlem2  10062  dju1dif  10083  ackbij1  10147  ackbij2lem2  10149  ackbij2  10152  infpssrlem3  10215  hsmexlem4  10339  hsmexlem5  10340  ac2  10371  axac3  10374  ac6  10390  axdclem2  10430  dmct  10434  ondomon  10473  alephsucpw  10481  pwcfsdom  10494  cfpwsdom  10495  smobeth  10497  axpowndlem3  10510  zfcndun  10526  zfcndpow  10527  zfcndinf  10529  zfcndac  10530  wunex2  10649  uniwun  10651  wuncval2  10658  grur1  10731  axgroth5  10735  axgroth2  10736  axgroth6  10739  axgroth3  10742  grothtsk  10746  inaprc  10747  ltsopi  10799  dmaddpi  10801  dmmulpi  10802  1lt2pi  10816  nqerf  10841  addnqf  10859  mulnqf  10860  1lt2nq  10884  m1p1sr  11003  m1m1sr  11004  0lt1sr  11006  axaddf  11056  axmulf  11057  ax1cn  11060  subaddrii  11470  ixi  11766  recgt0ii  12048  nn1suc  12167  4div2e2  12310  arch  12398  un0mulcl  12435  pnf0xnn0  12481  3halfnz  12571  nummac  12652  indstr  12829  mnfltpnf  13040  ioof  13363  0nelfz1  13459  fzp1disj  13499  fzp1nel  13527  fzof  13572  fvf1tp  13709  om2uzrani  13875  om2uzf1oi  13876  uzrdglem  13880  uzrdgfni  13881  uzrdg0i  13882  ltwenn  13885  hashgf1o  13894  axdc4uzlem  13906  sq0  14115  irec  14124  facmapnn  14208  hashkf  14255  hashfxnn0  14260  hashf  14261  hash0  14290  prhash2ex  14322  hashsslei  14349  hashxplem  14356  hashbclem  14375  hashf1lem1  14378  tpf1ofv0  14419  tpfo  14423  s1dm  14532  eqs1  14536  ccat2s1p1  14553  cats1un  14644  revs1  14688  0csh0  14716  cshw1  14745  cats1fvn  14781  funcnvs1  14835  pfx2  14870  relexp0g  14945  relexpsucnnr  14948  rtrclreclem1  14980  dfrtrclrec2  14981  rtrclreclem2  14982  rtrclreclem4  14984  dfrtrcl2  14985  climmo  15480  fsumcom2  15697  ackbijnn  15751  incexclem  15759  infcvgaux1i  15780  fprodcom2  15907  bpolylem  15971  bpoly3  15981  bpoly4  15982  efcvgfsum  16009  cos1bnd  16112  cos2bnd  16113  znnen  16137  qnnen  16138  aleph1re  16170  3dvds  16258  n2dvdsm1  16296  divalglem5  16324  flodddiv4  16342  sadcaddlem  16384  sadadd2lem  16386  sadadd3  16388  sadaddlem  16393  lcmf0  16561  lcmfunsnlem2lem1  16565  lcmfunsnlem2  16567  coprmprod  16588  coprmproddvdslem  16589  2prm  16619  3lcm2e6  16659  phicl2  16695  pockthi  16835  unbenlem  16836  prmrec  16850  vdwlem13  16921  vdwnn  16926  ramcl2  16944  prmgapprmo  16990  mod2xnegi  16999  modsubi  17000  structcnvcnv  17080  strleun  17084  setsres  17105  strfv  17130  starvndxnbasendx  17224  starvndxnplusgndx  17225  starvndxnmulrndx  17226  scandxnbasendx  17236  scandxnplusgndx  17237  scandxnmulrndx  17238  vscandxnbasendx  17241  vscandxnplusgndx  17242  vscandxnmulrndx  17243  vscandxnscandx  17244  ipndxnbasendx  17252  ipndxnplusgndx  17253  ipndxnmulrndx  17254  slotsdifipndx  17255  tsetndxnplusgndx  17277  tsetndxnmulrndx  17278  tsetndxnstarvndx  17279  slotstnscsi  17280  plendxnplusgndx  17291  plendxnmulrndx  17292  plendxnscandx  17293  plendxnvscandx  17294  slotsdifplendx  17295  basendxnocndx  17303  plendxnocndx  17304  dsndxnplusgndx  17310  dsndxnmulrndx  17311  slotsdnscsi  17312  dsndxntsetndx  17313  slotsdifdsndx  17314  unifndxntsetndx  17320  slotsdifunifndx  17321  slotsdifplendx2  17336  slotsdifocndx  17337  0rest  17349  firest  17352  restid  17353  prdsval  17375  prdsbas  17377  prdsplusg  17378  prdsmulr  17379  prdsvsca  17380  imasaddfnlem  17449  imasvscafn  17458  2oppchomf  17647  0ssc  17761  0subcat  17762  idfucl  17805  homarel  17960  dmaf  17973  cdaf  17974  setc2ohom  18019  catcfuccl  18042  relxpchom  18104  catcxpccl  18130  oppchofcl  18183  oyoncl  18193  letsr  18516  nulchn  18542  s1chn  18543  chnub  18545  chninf  18558  ex-chn1  18560  mgmidmo  18585  efmndmgm  18810  smndex1ibas  18825  smndex1mgm  18832  smndex1mnd  18835  smndex2dbas  18839  smndex2dnrinv  18840  smndex2hbas  18841  pwmnd  18862  releqg  19104  ga0  19227  psgnunilem3  19425  psgnunilem4  19426  pmtrsn  19448  efgval  19646  efger  19647  efgsval2  19662  efgsp1  19666  efgsfo  19668  efgredleme  19672  efgredlem  19676  efgred  19677  cygctb  19821  gsum2d2lem  19902  gsum2d2  19903  gsumcom2  19904  dprd2d2  19975  pgpfaclem1  20012  gsumle  20074  reldvdsr  20296  fldhmsubc  20718  00lsp  20932  cnfldfun  21323  cnfldfunALT  21324  cnfldfunOLD  21336  cnfldfunALTOLD  21337  xrsmgm  21361  pzriprnglem8  21443  pzriprnglem13  21448  pzriprnglem14  21449  pzriprngALT  21450  resubdrg  21563  ocv0  21632  cssval  21637  islinds2  21768  psrvscafval  21904  psrbag0  22017  psdmvr  22112  00ply1bas  22180  ply1plusgfvi  22182  m2detleib  22575  tgdom  22922  tgidm  22924  indistps2ALT  22958  restbas  23102  resttopon  23105  rest0  23113  leordtval2  23156  iocpnfordt  23159  icomnfordt  23160  iooordt  23161  ist1-3  23293  1stcfb  23389  comppfsc  23476  1stckgen  23498  ptbasfi  23525  dfac14  23562  opnfbas  23786  hauspwpwf1  23931  alexsubALT  23995  ptcmplem5  24000  cnextrel  24007  ust0  24164  0met  24310  prdsdsf  24311  prdsxmetlem  24312  prdsmet  24314  prdsbl  24435  qtopbaslem  24702  xrtgioo  24751  xrsdsre  24755  zcld  24758  recld2  24759  reperflem  24763  retopconn  24774  iccpnfcnv  24898  bndth  24913  nmoleub2lem2  25072  zclmncvs  25104  recmet  25279  resscdrg  25314  ishl2  25326  recms  25336  volf  25486  iundisj2  25506  volsup  25513  icombl  25521  ioombl  25522  ismbf3d  25611  0plef  25629  0pledm  25630  itg1ge0  25643  mbfi1fseqlem5  25676  itg2addlem  25715  reldv  25827  limciun  25851  dvexp  25913  dveflem  25939  lhop1lem  25974  lhop  25977  elply2  26157  elplyd  26163  ply1term  26165  ply0  26169  plymullem  26177  qaa  26287  pserulm  26387  pserdvlem2  26394  efcn  26409  sincosq1lem  26462  tangtx  26470  sincos4thpi  26478  pigt3  26483  pige3ALT  26485  efif1olem4  26510  logf1o  26529  relogf1o  26531  log1  26550  loge  26551  logi  26552  relogiso  26563  dvrelog  26602  relogcn  26603  logcn  26612  cxpcn3  26714  resqrtcn  26715  rtprmirr  26726  2logb9irr  26761  leibpi  26908  log2ublem1  26912  birthday  26920  emcllem5  26966  harmonicbnd  26970  harmonicbnd2  26971  harmonicbnd3  26974  lgamgulm2  27002  lgamcvglem  27006  gamf  27009  ppiltx  27143  ppiublem1  27169  ppiub  27171  bclbnd  27247  bpos1lem  27249  bposlem8  27258  lgsquadlem2  27348  2sqlem9  27394  2sqlem10  27395  addsqnreup  27410  chebbnd1  27439  selberg2lem  27517  pntrsumo1  27532  selbergsb  27542  pntpbnd  27555  ltsval2  27624  noxp1o  27631  nosepnelem  27647  noetasuplem2  27702  noetainflem2  27706  0lt1s  27808  addsf  27978  precsexlem1  28203  precsexlem2  28204  precsexlem3  28205  precsexlem4  28206  precsexlem5  28207  precsexlem9  28211  precsexlem10  28212  precsexlem11  28213  elons2  28254  oncutlt  28260  oniso  28267  onswe  28268  onsse  28269  onaddscl  28273  onmulscl  28274  onsbnd  28277  eln0s  28357  0zs  28384  zseo  28418  twocut  28419  0reno  28492  1reno  28493  lngndxnitvndx  28515  istrkg2ld  28532  tgcgr4  28603  ax5seglem7  29008  axlowdimlem4  29018  axlowdimlem6  29020  axlowdimlem7  29021  axlowdimlem10  29024  axlowdimlem13  29027  axlowdimlem16  29030  uhgr0e  29144  uhgr0  29146  upgrbi  29166  umgrbi  29174  usgr0  29316  lfuhgr1v0e  29327  usgrexmpllem  29333  usgrexmpl  29336  griedg0prc  29337  cplgr0  29498  usgrexilem  29513  cffldtocusgr  29520  cffldtocusgrOLD  29521  rgrusgrprc  29663  rusgrprc  29664  rgrprcx  29666  rgrx0ndm  29667  usgr2pthlem  29836  pthdlem2  29841  uspgrn2crct  29881  wwlksnext  29966  clwwlknondisj  30186  0ewlk  30189  0wlk  30191  0pth  30200  1pthdlem1  30210  1trld  30217  wlk2v2elem2  30231  wlk2v2e  30232  upgr3v3e3cycl  30255  upgr4cycl4dv4e  30260  dfconngr1  30263  0conngr  30267  konigsbergumgr  30326  2wspmdisj  30412  2clwwlk2clwwlk  30425  numclwwlk3lem2lem  30458  numclwwlk3lem2  30459  ex-dif  30498  ex-in  30500  ex-eprel  30508  ex-id  30509  ex-fl  30522  ex-mod  30524  ex-hash  30528  ex-fpar  30537  avril1  30538  2bornot2b  30539  0vfval  30681  vsfval  30708  ajmoi  30933  ajfuni  30934  normlem2  31186  norm3adifii  31223  hhip  31252  hlim0  31310  hlimcaui  31311  hlimf  31312  hhssnv  31339  shscli  31392  shsval2i  31462  h1de2i  31628  fh3i  31698  fh4i  31699  cm2mi  31701  qlaxr3i  31711  mayetes3i  31804  ho0f  31826  hoif  31829  hodidi  31862  ho0subi  31870  hosd1i  31897  adjmo  31907  nmopsetn0  31940  nmfnsetn0  31953  funadj  31961  funcnvadj  31968  nmcexi  32101  cnlnadjlem8  32149  nmoptri2i  32174  opsqrlem4  32218  hmopidmchi  32226  pjoci  32255  pjinvari  32266  abrexdomjm  32582  elim2ifim  32620  iundisj2f  32665  rinvf1o  32708  dfcnv2  32754  snct  32791  fzodif2  32871  iundisj2fi  32877  dp2lt10  32965  dp2ltc  32968  dplti  32986  dpgti  32987  dpexpp1  32989  xrge0slmod  33429  isconstr  33893  zarcls  34031  zartopn  34032  xrge0pluscn  34097  qqhre  34177  esumrnmpt2  34225  esumfsup  34227  esumpcvgval  34235  hasheuni  34242  esumcvg  34243  esumcvgsum  34245  esumsup  34246  esum2d  34250  dmsigagen  34301  ldgenpisyslem3  34322  measvuni  34371  voliune  34386  volfiniune  34387  br2base  34426  dya2iocuni  34440  eulerpartlem1  34524  eulerpartlemt  34528  eulerpartgbij  34529  fib0  34556  coinfliprv  34640  ballotlem2  34646  ballotlemic  34664  ballotlem7  34693  ballotth  34695  plymul02  34703  rpsqrtcn  34750  chtvalz  34786  circlemethnat  34798  circlevma  34799  circlemethhgt  34800  hgt750lem  34808  bnj226  34890  bnj1101  34940  bnj110  35014  bnj149  35031  bnj150  35032  bnj151  35033  bnj517  35041  bnj580  35069  bnj865  35079  bnj900  35085  bnj996  35112  bnj1110  35138  bnj1133  35145  bnj1128  35146  bnj1145  35149  bnj1137  35151  bnj1171  35156  bnj1176  35161  fineqvnttrclse  35280  setinds2regs  35287  tz9.1regs  35290  f1resfz0f1d  35308  subfacp1lem5  35378  subfacp1lem6  35379  kur14lem9  35408  cvmcov2  35469  cvmliftlem1  35479  cvmliftlem4  35482  cvmliftlem5  35483  gonanegoal  35546  satfv0  35552  satfv0fun  35565  fmlan0  35585  gonan0  35586  fmla0disjsuc  35592  ex-sategoelel12  35621  msrfo  35740  problem5  35863  brtpid1  35915  brtpid2  35916  brtpid3  35917  faclimlem1  35937  axextndbi  35996  txprel  36071  relsset  36080  relbigcup  36089  fvbigcup  36094  fnsingle  36111  fvsingle  36112  snelsingles  36114  funimage  36120  fullfunfnv  36140  imagesset  36147  funtransport  36225  colinrel  36251  funray  36334  funline  36336  0hf  36371  neibastop2lem  36554  filnetlem3  36574  nrmo  36604  waj-ax  36608  lukshef-ax2  36609  arg-ax  36610  limsucncmpi  36639  regsfromregtr  36668  dnizeq0  36675  knoppcnlem8  36700  knoppcnlem11  36703  cnndvlem1  36737  bj-babylob  36804  bj-ax12ssb  36859  bj-nnfnth  36944  bj-snsetex  37164  bj-0eltag  37179  bj-2upln0  37224  bj-2upln1upl  37225  bj-snexg  37235  bj-unexg  37239  bj-adjg1  37244  f1omptsnlem  37541  f1omptsn  37542  icoreresf  37557  relowlssretop  37568  relowlpssretop  37569  domalom  37609  matunitlindf  37819  poimirlem3  37824  poimirlem9  37830  poimirlem16  37837  poimirlem17  37838  poimirlem18  37839  poimirlem19  37840  poimirlem20  37841  poimirlem26  37847  mblfinlem1  37858  mblfinlem2  37859  ismblfin  37862  voliunnfl  37865  cnambfre  37869  abrexdom  37931  fdc  37946  cncfres  37966  heibor1lem  38010  grposnOLD  38083  bicontr  38281  an12i  38299  tsim1  38331  ac6s6f  38374  vvdifopab  38458  brcnvrabga  38535  opabf  38561  xrnrel  38567  dmsucmap  38642  mopre  38645  relcoels  38687  cnvcosseq  38700  refrelcoss3  38726  refrelcoss2  38727  symrelcoss2  38729  refrelcoss  38776  symrelcoss  38817  n0eldmqs  38906  ax13fromc9  39166  dedths  39222  renegclALT  39223  12gcd5e1  42257  60gcd7e1  42259  lcmineqlem23  42305  dvrelog2  42318  dvrelog3  42319  dvrelog2b  42320  aks4d1p1p6  42327  aks4d1p1p7  42328  aks4d1p1  42330  sticksstones22  42422  sn-axprlem3  42474  acos1half  42613  moxfr  42934  mapfzcons1  42959  diophrw  43001  0dioph  43020  vdioph  43021  rabren3dioph  43057  2nn0ind  43187  rpnnen3  43274  kelac2lem  43306  frlmpwfi  43340  oaordnrex  43537  omnord1ex  43546  oenord1ex  43557  oaomoencom  43559  ifpbiidcor2  43724  iscard4  43774  sqrtcval  43882  resqrtvalex  43886  eliunov2  43920  xphe  44022  0he  44023  he0  44025  snhesn  44027  idhe  44028  frege54cor1c  44156  clsk1independent  44287  neicvgnvor  44357  amgm2d  44439  amgm3d  44440  amgm4d  44441  ismnushort  44542  lhe4.4ex1a  44570  rusbcALT  44679  ipo0  44689  ifr0  44690  vk15.4j  44769  2sb5nd  44801  dfvd1ir  44814  dfvd2anir  44825  dfvd2ir  44827  dfvd3ir  44834  dfvd3anir  44837  iden2  44855  e0bir  45017  uun2221p1  45054  uun2221p2  45055  2sb5ndVD  45150  2sb5ndALT  45172  iunconnlem2  45175  trwf  45200  wfaxext  45234  wfaxpow  45238  wfaxinf2  45242  wfac8prim  45243  permaxinf2lem  45253  nregmodelf1o  45256  fnchoice  45274  unisn0  45299  eliincex  45354  icof  45463  fnmptif  45509  supminfxr  45708  rexanuz2nf  45736  fsumiunss  45821  climlimsupcex  46013  liminfltlimsupex  46025  liminflelimsupcex  46041  xlimrel  46064  xlimfun  46099  resincncf  46119  dvnprodlem3  46192  volioc  46216  volico  46227  dmvolss  46229  volioof  46231  stoweidlem13  46257  stoweidlem34  46278  stirlinglem5  46322  stirlinglem13  46330  stirlingr  46334  fourierdlem42  46393  fourierdlem62  46412  fouriersw  46475  etransc  46527  salexct  46578  salexct2  46583  salgencntex  46587  sge0rnn0  46612  gsumge0cl  46615  sge00  46620  sge0resplit  46650  sge0reuz  46691  omeiunle  46761  0ome  46773  icoresmbl  46787  ovn0lem  46809  ovnhoilem1  46845  hspmbl  46873  nsssmfmbf  47023  mbfpsssmf  47027  smfresal  47032  smfmullem4  47038  smfpimbor1lem1  47042  smfpimbor1lem2  47043  nthrucw  47130  lambert0  47133  lamberte  47134  cjnpoly  47135  tannpoly  47136  sinnpoly  47137  aistia  47143  aisfina  47144  aiffnbandciffatnotciffb  47150  axorbciffatcxorb  47151  abnotbtaxb  47161  abnotataxb  47162  eusnsn  47272  aiotaval  47341  aiota0ndef  47343  fundcmpsurinjimaid  47657  ichv  47695  ichf  47696  ichid  47697  icht  47698  ichcircshi  47700  icheq  47708  spr0nelg  47722  m3prm  47838  m7prm  47846  0noddALTV  47935  2noddALTV  47939  341fppr2  47980  9fppr8  47983  nfermltl8rev  47988  nfermltl2rev  47989  nfermltlrev  47990  sbgoldbo  48033  nnsum3primes4  48034  evengpop3  48044  stgr1  48207  usgrexmpl1lem  48267  usgrexmpl1  48268  usgrexmpl1tri  48271  usgrexmpl2lem  48272  usgrexmpl2  48273  usgrexmpl2nb0  48277  usgrexmpl2nb1  48278  usgrexmpl2nb2  48279  usgrexmpl2nb3  48280  usgrexmpl2nb4  48281  usgrexmpl2nb5  48282  gpgedg2ov  48312  gpgedg2iv  48313  gpg5nbgrvtx03starlem1  48314  gpg5nbgrvtx03starlem2  48315  gpg5nbgrvtx03starlem3  48316  gpg5nbgrvtx13starlem1  48317  gpg5nbgrvtx13starlem2  48318  gpg5nbgrvtx13starlem3  48319  gpg5grlim  48339  gpg5grlic  48340  gpgprismgr4cycllem2  48342  gpgprismgr4cycllem7  48347  pg4cyclnex  48373  gpg5edgnedg  48376  grlimedgnedg  48377  oddinmgm  48421  nn0mnd  48425  2zrngamgm  48491  2zrngaabl  48496  2zrngmmgm  48498  2zrngnring  48504  fldhmsubcALTV  48579  eliunxp2  48580  zlmodzxzldeplem  48744  zlmodzxzldep  48750  ldepslinc  48755  rrx2xpreen  48965  rrx2plordisom  48969  line2ylem  48997  line2  48998  line2x  49000  inlinecirc02plem  49032  mosn  49058  mof0  49083  mof0ALT  49085  tposrescnv  49124  tposres3  49126  tposideq2  49134  f1omoOLD  49139  nelsubc3  49316  reldmxpc  49491  reldmprcof1  49626  setc1onsubc  49847  reldmlmd2  49898  reldmcmd2  49899  rellmd  49904  relcmd  49905  ex-gte  49974  empty-surprise  50027  eximp-surprise2  50030  amgmw2d  50049