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  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  3448  moeq  3653  rmoeq  3684  cdeqi  3711  eqsstri  3968  vn0  4285  rmo0  4302  ab0orv  4323  rabnc  4331  reuprg  4647  tpid1  4712  tpid2  4714  mosneq  4785  pwv  4847  uni0OLD  4879  int0  4904  eqbrtri  5106  tr0  5205  trv  5206  zfrep4  5228  axnulALT  5239  0ex  5242  inex1  5258  elpwi2  5276  0elpw  5297  axpow2  5309  dvdemo1  5315  vpwex  5319  zfpair2  5376  prex  5380  exss  5415  brv  5425  opwo0id  5451  moop2  5456  0sn0ep  5535  po0  5556  epse  5613  relxp  5649  rel0  5755  relopabiv  5776  relopabi  5778  relopabiALT  5779  eliunxp  5792  opeliunxp2  5793  dmi  5876  dmep  5878  xpidtr  6085  xpima  6146  dmsn0  6173  cnvsn0  6174  0elon  6378  funmpt  6536  funmpt2  6537  funcnv0  6564  isarep2  6588  fresaunres2  6712  f0  6721  f10d  6814  f1o00  6815  f1oi  6818  f1oiOLD  6819  f1osn  6821  brprcneu  6830  brprcneuALT  6831  opabiotafun  6920  fvopab3ig  6943  opabex  7175  eufnfv  7184  isof1oopb  7280  ncanth  7322  mpofun  7491  reldmmpo  7501  ovid  7508  ovidig  7509  ovidi  7510  ovig  7513  ov3  7530  caovmo  7604  relmptopab  7617  porpss  7681  uniex2  7692  tfinds2  7815  finds  7847  finds2  7849  oprabex  7929  oprabex3  7930  f1stres  7966  f2ndres  7967  relmpoopab  8044  fsplitfpar  8068  poseq  8108  opeliunxp2f  8160  tpos0  8206  issmo  8288  tfrlem6  8321  tfrlem8  8323  tfrlem16  8332  tfr1a  8333  tfr1  8336  tz7.44lem1  8344  seqomlem2  8390  seqomlem3  8391  seqomlem4  8392  fnseqom  8394  ord3  8420  0lt1o  8439  0we1  8441  naddf  8617  eqer  8680  ecopover  8768  mapsnf1o3  8843  ssdomg  8947  en0  8965  en0r  8967  ensn1  8968  0fi  8989  enrefnn  8993  xpcomf1o  9004  map2xp  9085  limensuci  9091  1sdom2  9158  sdom1  9160  unblem4  9205  fidomdm  9244  marypha1lem  9346  hartogslem1  9457  hartogs  9459  card2on  9469  nelaneqOLDOLD  9518  epinid0  9519  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  11483  ixi  11779  recgt0ii  12062  nn1suc  12196  4div2e2  12346  arch  12434  un0mulcl  12471  pnf0xnn0  12517  3halfnz  12608  nummac  12689  indstr  12866  mnfltpnf  13077  ioof  13400  0nelfz1  13497  fzp1disj  13537  fzp1nel  13565  fzof  13610  fvf1tp  13748  om2uzrani  13914  om2uzf1oi  13915  uzrdglem  13919  uzrdgfni  13920  uzrdg0i  13921  ltwenn  13924  hashgf1o  13933  axdc4uzlem  13945  sq0  14154  irec  14163  facmapnn  14247  hashkf  14294  hashfxnn0  14299  hashf  14300  hash0  14329  prhash2ex  14361  hashsslei  14388  hashxplem  14395  hashbclem  14414  hashf1lem1  14417  tpf1ofv0  14458  tpfo  14462  s1dm  14571  eqs1  14575  ccat2s1p1  14592  cats1un  14683  revs1  14727  0csh0  14755  cshw1  14784  cats1fvn  14820  funcnvs1  14874  pfx2  14909  relexp0g  14984  relexpsucnnr  14987  rtrclreclem1  15019  dfrtrclrec2  15020  rtrclreclem2  15021  rtrclreclem4  15023  dfrtrcl2  15024  climmo  15519  fsumcom2  15736  ackbijnn  15793  incexclem  15801  infcvgaux1i  15822  fprodcom2  15949  bpolylem  16013  bpoly3  16023  bpoly4  16024  efcvgfsum  16051  cos1bnd  16154  cos2bnd  16155  znnen  16179  qnnen  16180  aleph1re  16212  3dvds  16300  n2dvdsm1  16338  divalglem5  16366  flodddiv4  16384  sadcaddlem  16426  sadadd2lem  16428  sadadd3  16430  sadaddlem  16435  lcmf0  16603  lcmfunsnlem2lem1  16607  lcmfunsnlem2  16609  coprmprod  16630  coprmproddvdslem  16631  2prm  16661  3lcm2e6  16702  phicl2  16738  pockthi  16878  unbenlem  16879  prmrec  16893  vdwlem13  16964  vdwnn  16969  ramcl2  16987  prmgapprmo  17033  mod2xnegi  17042  modsubi  17043  structcnvcnv  17123  strleun  17127  setsres  17148  strfv  17173  starvndxnbasendx  17267  starvndxnplusgndx  17268  starvndxnmulrndx  17269  scandxnbasendx  17279  scandxnplusgndx  17280  scandxnmulrndx  17281  vscandxnbasendx  17284  vscandxnplusgndx  17285  vscandxnmulrndx  17286  vscandxnscandx  17287  ipndxnbasendx  17295  ipndxnplusgndx  17296  ipndxnmulrndx  17297  slotsdifipndx  17298  tsetndxnplusgndx  17320  tsetndxnmulrndx  17321  tsetndxnstarvndx  17322  slotstnscsi  17323  plendxnplusgndx  17334  plendxnmulrndx  17335  plendxnscandx  17336  plendxnvscandx  17337  slotsdifplendx  17338  basendxnocndx  17346  plendxnocndx  17347  dsndxnplusgndx  17353  dsndxnmulrndx  17354  slotsdnscsi  17355  dsndxntsetndx  17356  slotsdifdsndx  17357  unifndxntsetndx  17363  slotsdifunifndx  17364  slotsdifplendx2  17379  slotsdifocndx  17380  0rest  17392  firest  17395  restid  17396  prdsval  17418  prdsbas  17420  prdsplusg  17421  prdsmulr  17422  prdsvsca  17423  imasaddfnlem  17492  imasvscafn  17501  2oppchomf  17690  0ssc  17804  0subcat  17805  idfucl  17848  homarel  18003  dmaf  18016  cdaf  18017  setc2ohom  18062  catcfuccl  18085  relxpchom  18147  catcxpccl  18173  oppchofcl  18226  oyoncl  18236  letsr  18559  nulchn  18585  s1chn  18586  chnub  18588  chninf  18601  ex-chn1  18603  mgmidmo  18628  efmndmgm  18853  smndex1ibas  18868  smndex1mgm  18878  smndex1mnd  18881  smndex2dbas  18885  smndex2dnrinv  18886  smndex2hbas  18887  pwmnd  18908  releqg  19150  ga0  19273  psgnunilem3  19471  psgnunilem4  19472  pmtrsn  19494  efgval  19692  efger  19693  efgsval2  19708  efgsp1  19712  efgsfo  19714  efgredleme  19718  efgredlem  19722  efgred  19723  cygctb  19867  gsum2d2lem  19948  gsum2d2  19949  gsumcom2  19950  dprd2d2  20021  pgpfaclem1  20058  gsumle  20120  reldvdsr  20340  fldhmsubc  20762  00lsp  20976  cnfldfun  21366  cnfldfunALT  21367  xrsmgm  21387  pzriprnglem8  21468  pzriprnglem13  21473  pzriprnglem14  21474  pzriprngALT  21475  resubdrg  21588  ocv0  21657  cssval  21662  islinds2  21793  psrvscafval  21927  psrbag0  22040  psdmvr  22135  00ply1bas  22203  ply1plusgfvi  22205  m2detleib  22596  tgdom  22943  tgidm  22945  indistps2ALT  22979  restbas  23123  resttopon  23126  rest0  23134  leordtval2  23177  iocpnfordt  23180  icomnfordt  23181  iooordt  23182  ist1-3  23314  1stcfb  23410  comppfsc  23497  1stckgen  23519  ptbasfi  23546  dfac14  23583  opnfbas  23807  hauspwpwf1  23952  alexsubALT  24016  ptcmplem5  24021  cnextrel  24028  ust0  24185  0met  24331  prdsdsf  24332  prdsxmetlem  24333  prdsmet  24335  prdsbl  24456  qtopbaslem  24723  xrtgioo  24772  xrsdsre  24776  zcld  24779  recld2  24780  reperflem  24784  retopconn  24795  iccpnfcnv  24911  bndth  24925  nmoleub2lem2  25083  zclmncvs  25115  recmet  25290  resscdrg  25325  ishl2  25337  recms  25347  volf  25496  iundisj2  25516  volsup  25523  icombl  25531  ioombl  25532  ismbf3d  25621  0plef  25639  0pledm  25640  itg1ge0  25653  mbfi1fseqlem5  25686  itg2addlem  25725  reldv  25837  limciun  25861  dvexp  25920  dveflem  25946  lhop1lem  25980  lhop  25983  elply2  26161  elplyd  26167  ply1term  26169  ply0  26173  plymullem  26181  qaa  26289  pserulm  26387  pserdvlem2  26393  efcn  26408  sincosq1lem  26461  tangtx  26469  sincos4thpi  26477  pigt3  26482  pige3ALT  26484  efif1olem4  26509  logf1o  26528  relogf1o  26530  log1  26549  loge  26550  logi  26551  relogiso  26562  dvrelog  26601  relogcn  26602  logcn  26611  cxpcn3  26712  resqrtcn  26713  rtprmirr  26724  2logb9irr  26759  leibpi  26906  log2ublem1  26910  birthday  26918  emcllem5  26963  harmonicbnd  26967  harmonicbnd2  26968  harmonicbnd3  26971  lgamgulm2  26999  lgamcvglem  27003  gamf  27006  ppiltx  27140  ppiublem1  27165  ppiub  27167  bclbnd  27243  bpos1lem  27245  bposlem8  27254  lgsquadlem2  27344  2sqlem9  27390  2sqlem10  27391  addsqnreup  27406  chebbnd1  27435  selberg2lem  27513  pntrsumo1  27528  selbergsb  27538  pntpbnd  27551  ltsval2  27620  noxp1o  27627  nosepnelem  27643  noetasuplem2  27698  noetainflem2  27702  0lt1s  27804  addsf  27974  precsexlem1  28199  precsexlem2  28200  precsexlem3  28201  precsexlem4  28202  precsexlem5  28203  precsexlem9  28207  precsexlem10  28208  precsexlem11  28209  elons2  28250  oncutlt  28256  oniso  28263  onswe  28264  onsse  28265  onaddscl  28269  onmulscl  28270  onsbnd  28273  eln0s  28353  0zs  28380  zseo  28414  twocut  28415  0reno  28488  1reno  28489  lngndxnitvndx  28511  istrkg2ld  28528  tgcgr4  28599  ax5seglem7  29004  axlowdimlem4  29014  axlowdimlem6  29016  axlowdimlem7  29017  axlowdimlem10  29020  axlowdimlem13  29023  axlowdimlem16  29026  uhgr0e  29140  uhgr0  29142  upgrbi  29162  umgrbi  29170  usgr0  29312  lfuhgr1v0e  29323  usgrexmpllem  29329  usgrexmpl  29332  griedg0prc  29333  cplgr0  29494  usgrexilem  29509  cffldtocusgr  29516  rgrusgrprc  29658  rusgrprc  29659  rgrprcx  29661  rgrx0ndm  29662  usgr2pthlem  29831  pthdlem2  29836  uspgrn2crct  29876  wwlksnext  29961  clwwlknondisj  30181  0ewlk  30184  0wlk  30186  0pth  30195  1pthdlem1  30205  1trld  30212  wlk2v2elem2  30226  wlk2v2e  30227  upgr3v3e3cycl  30250  upgr4cycl4dv4e  30255  dfconngr1  30258  0conngr  30262  konigsbergumgr  30321  2wspmdisj  30407  2clwwlk2clwwlk  30420  numclwwlk3lem2lem  30453  numclwwlk3lem2  30454  ex-dif  30493  ex-in  30495  ex-eprel  30503  ex-id  30504  ex-fl  30517  ex-mod  30519  ex-hash  30523  ex-fpar  30532  avril1  30533  2bornot2b  30534  0vfval  30677  vsfval  30704  ajmoi  30929  ajfuni  30930  normlem2  31182  norm3adifii  31219  hhip  31248  hlim0  31306  hlimcaui  31307  hlimf  31308  hhssnv  31335  shscli  31388  shsval2i  31458  h1de2i  31624  fh3i  31694  fh4i  31695  cm2mi  31697  qlaxr3i  31707  mayetes3i  31800  ho0f  31822  hoif  31825  hodidi  31858  ho0subi  31866  hosd1i  31893  adjmo  31903  nmopsetn0  31936  nmfnsetn0  31949  funadj  31957  funcnvadj  31964  nmcexi  32097  cnlnadjlem8  32145  nmoptri2i  32170  opsqrlem4  32214  hmopidmchi  32222  pjoci  32251  pjinvari  32262  abrexdomjm  32577  elim2ifim  32615  iundisj2f  32660  rinvf1o  32703  dfcnv2  32748  snct  32785  fzodif2  32864  iundisj2fi  32870  dp2lt10  32943  dp2ltc  32946  dplti  32964  dpgti  32965  dpexpp1  32967  xrge0slmod  33408  isconstr  33880  zarcls  34018  zartopn  34019  xrge0pluscn  34084  qqhre  34164  esumrnmpt2  34212  esumfsup  34214  esumpcvgval  34222  hasheuni  34229  esumcvg  34230  esumcvgsum  34232  esumsup  34233  esum2d  34237  dmsigagen  34288  ldgenpisyslem3  34309  measvuni  34358  voliune  34373  volfiniune  34374  br2base  34413  dya2iocuni  34427  eulerpartlem1  34511  eulerpartlemt  34515  eulerpartgbij  34516  fib0  34543  coinfliprv  34627  ballotlem2  34633  ballotlemic  34651  ballotlem7  34680  ballotth  34682  plymul02  34690  rpsqrtcn  34737  chtvalz  34773  circlemethnat  34785  circlevma  34786  circlemethhgt  34787  hgt750lem  34795  bnj226  34877  bnj1101  34927  bnj110  35000  bnj149  35017  bnj150  35018  bnj151  35019  bnj517  35027  bnj580  35055  bnj865  35065  bnj900  35071  bnj996  35098  bnj1110  35124  bnj1133  35131  bnj1128  35132  bnj1145  35135  bnj1137  35137  bnj1171  35142  bnj1176  35147  axnulALT2  35224  fineqvnttrclse  35268  setinds2regs  35275  tz9.1regs  35278  f1resfz0f1d  35296  subfacp1lem5  35366  subfacp1lem6  35367  kur14lem9  35396  cvmcov2  35457  cvmliftlem1  35467  cvmliftlem4  35470  cvmliftlem5  35471  gonanegoal  35534  satfv0  35540  satfv0fun  35553  fmlan0  35573  gonan0  35574  fmla0disjsuc  35580  ex-sategoelel12  35609  msrfo  35728  problem5  35851  brtpid1  35903  brtpid2  35904  brtpid3  35905  faclimlem1  35925  axextndbi  35984  txprel  36059  relsset  36068  relbigcup  36077  fvbigcup  36082  fnsingle  36099  fvsingle  36100  snelsingles  36102  funimage  36108  fullfunfnv  36128  imagesset  36135  funtransport  36213  colinrel  36239  funray  36322  funline  36324  0hf  36359  neibastop2lem  36542  filnetlem3  36562  nrmo  36592  waj-ax  36596  lukshef-ax2  36597  arg-ax  36598  limsucncmpi  36627  ttctr  36675  dfttc2g  36688  ttcuniun  36692  ttcuni  36695  dfttc4lem2  36711  regsfromregtco  36720  dnizeq0  36735  knoppcnlem8  36760  knoppcnlem11  36763  cnndvlem1  36797  bj-babylob  36869  bj-ax12ssb  36952  bj-nnfnth  37048  bj-snsetex  37270  bj-0eltag  37285  bj-2upln0  37330  bj-2upln1upl  37331  bj-snexg  37341  bj-unexg  37345  bj-adjg1  37350  bj-axseprep  37381  f1omptsnlem  37652  f1omptsn  37653  icoreresf  37668  relowlssretop  37679  relowlpssretop  37680  domalom  37720  matunitlindf  37939  poimirlem3  37944  poimirlem9  37950  poimirlem16  37957  poimirlem17  37958  poimirlem18  37959  poimirlem19  37960  poimirlem20  37961  poimirlem26  37967  mblfinlem1  37978  mblfinlem2  37979  ismblfin  37982  voliunnfl  37985  cnambfre  37989  abrexdom  38051  fdc  38066  cncfres  38086  heibor1lem  38130  grposnOLD  38203  bicontr  38401  an12i  38419  tsim1  38451  ac6s6f  38494  vvdifopab  38586  brcnvrabga  38663  opabf  38697  xrnrel  38703  relqmap  38773  dmsucmap  38789  mopre  38792  relcoels  38835  cnvcosseq  38848  refrelcoss3  38874  refrelcoss2  38875  symrelcoss2  38877  refrelcoss  38924  symrelcoss  38965  n0eldmqs  39053  ax13fromc9  39352  dedths  39408  renegclALT  39409  12gcd5e1  42442  60gcd7e1  42444  lcmineqlem23  42490  dvrelog2  42503  dvrelog3  42504  dvrelog2b  42505  aks4d1p1p6  42512  aks4d1p1p7  42513  aks4d1p1  42515  sticksstones22  42607  sn-axprlem3  42659  acos1half  42790  moxfr  43124  mapfzcons1  43149  diophrw  43191  0dioph  43210  vdioph  43211  rabren3dioph  43243  2nn0ind  43373  rpnnen3  43460  kelac2lem  43492  frlmpwfi  43526  oaordnrex  43723  omnord1ex  43732  oenord1ex  43743  oaomoencom  43745  ifpbiidcor2  43910  iscard4  43960  sqrtcval  44068  resqrtvalex  44072  eliunov2  44106  xphe  44208  0he  44209  he0  44211  snhesn  44213  idhe  44214  frege54cor1c  44342  clsk1independent  44473  neicvgnvor  44543  amgm2d  44625  amgm3d  44626  amgm4d  44627  ismnushort  44728  lhe4.4ex1a  44756  rusbcALT  44865  ipo0  44875  ifr0  44876  vk15.4j  44955  2sb5nd  44987  dfvd1ir  45000  dfvd2anir  45011  dfvd2ir  45013  dfvd3ir  45020  dfvd3anir  45023  iden2  45041  e0bir  45203  uun2221p1  45240  uun2221p2  45241  2sb5ndVD  45336  2sb5ndALT  45358  iunconnlem2  45361  trwf  45386  wfaxext  45420  wfaxpow  45424  wfaxinf2  45428  wfac8prim  45429  permaxinf2lem  45439  nregmodelf1o  45442  fnchoice  45460  unisn0  45485  eliincex  45540  icof  45648  fnmptif  45694  supminfxr  45892  rexanuz2nf  45920  fsumiunss  46005  climlimsupcex  46197  liminfltlimsupex  46209  liminflelimsupcex  46225  xlimrel  46248  xlimfun  46283  resincncf  46303  dvnprodlem3  46376  volioc  46400  volico  46411  dmvolss  46413  volioof  46415  stoweidlem13  46441  stoweidlem34  46462  stirlinglem5  46506  stirlinglem13  46514  stirlingr  46518  fourierdlem42  46577  fourierdlem62  46596  fouriersw  46659  etransc  46711  salexct  46762  salexct2  46767  salgencntex  46771  sge0rnn0  46796  gsumge0cl  46799  sge00  46804  sge0resplit  46834  sge0reuz  46875  omeiunle  46945  0ome  46957  icoresmbl  46971  ovn0lem  46993  ovnhoilem1  47029  hspmbl  47057  nsssmfmbf  47207  mbfpsssmf  47211  smfresal  47216  smfmullem4  47222  smfpimbor1lem1  47226  smfpimbor1lem2  47227  quantgodel  47302  nthrucw  47316  goldratmolem2  47334  lambert0  47335  lamberte  47336  cjnpoly  47337  tannpoly  47338  sinnpoly  47339  aistia  47345  aisfina  47346  aiffnbandciffatnotciffb  47352  axorbciffatcxorb  47353  abnotbtaxb  47363  abnotataxb  47364  eusnsn  47474  aiotaval  47543  aiota0ndef  47545  fundcmpsurinjimaid  47871  ichv  47909  ichf  47910  ichid  47911  icht  47912  ichcircshi  47914  icheq  47922  spr0nelg  47936  m3prm  48055  m7prm  48063  0noddALTV  48165  2noddALTV  48169  341fppr2  48210  9fppr8  48213  nfermltl8rev  48218  nfermltl2rev  48219  nfermltlrev  48220  sbgoldbo  48263  nnsum3primes4  48264  evengpop3  48274  stgr1  48437  usgrexmpl1lem  48497  usgrexmpl1  48498  usgrexmpl1tri  48501  usgrexmpl2lem  48502  usgrexmpl2  48503  usgrexmpl2nb0  48507  usgrexmpl2nb1  48508  usgrexmpl2nb2  48509  usgrexmpl2nb3  48510  usgrexmpl2nb4  48511  usgrexmpl2nb5  48512  gpgedg2ov  48542  gpgedg2iv  48543  gpg5nbgrvtx03starlem1  48544  gpg5nbgrvtx03starlem2  48545  gpg5nbgrvtx03starlem3  48546  gpg5nbgrvtx13starlem1  48547  gpg5nbgrvtx13starlem2  48548  gpg5nbgrvtx13starlem3  48549  gpg5grlim  48569  gpg5grlic  48570  gpgprismgr4cycllem2  48572  gpgprismgr4cycllem7  48577  pg4cyclnex  48603  gpg5edgnedg  48606  grlimedgnedg  48607  oddinmgm  48651  nn0mnd  48655  2zrngamgm  48721  2zrngaabl  48726  2zrngmmgm  48728  2zrngnring  48734  fldhmsubcALTV  48809  eliunxp2  48810  zlmodzxzldeplem  48974  zlmodzxzldep  48980  ldepslinc  48985  rrx2xpreen  49195  rrx2plordisom  49199  line2ylem  49227  line2  49228  line2x  49230  inlinecirc02plem  49262  mosn  49288  mof0  49313  mof0ALT  49315  tposrescnv  49354  tposres3  49356  tposideq2  49364  f1omoOLD  49369  nelsubc3  49546  reldmxpc  49721  reldmprcof1  49856  setc1onsubc  50077  reldmlmd2  50128  reldmcmd2  50129  rellmd  50134  relcmd  50135  ex-gte  50204  empty-surprise  50257  eximp-surprise2  50260  amgmw2d  50279