Theorem mpbir 234

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

Syntax hints:   ↔ wb 209

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 210

This theorem is referenced by:  pm5.74ri  275  con4bii  324  imnani  405  mpbir2an  723  imorri  868  orri  875  mpbir3an  1360  xorexmid  1557  tru  1574  had1  1633  nic-mpALT  1702  nic-ax  1703  nic-axALT  1704  nfi  1818  mpgbir  1829  nfxfr  1883  19.35ri  1909  ax5e  1942  ax6ev  1999  sbt  2100  equsb1v  2140  ax13  2407  ax13ALT  2457  moanmo  2650  axi12  2733  axbnd  2734  axexte  2736  axextmo  2739  nulmo  2740  vexw  2747  eqeltri  2859  nfcxfr  2923  neir  2961  neirr  2967  eqnetri  3028  nelir  3067  mprgbir  3086  issetri  3474  moeq  3670  rmoeq  3701  cdeqi  3728  eqsstri  3983  vn0OLD  4299  rmo0  4317  ab0orv  4339  rab0  4342  rabnc  4348  reuprg  4669  tpid1  4734  tpid2  4736  mosneq  4807  pwv  4869  uni0OLD  4902  int0  4927  eqbrtri  5132  tr0  5231  trv  5232  zfrep4  5254  axnulALT  5267  0ex  5270  inex1  5286  elpwi2  5306  0elpw  5326  axpow2  5338  dvdemo1  5344  vpwex  5348  zfpair2  5405  prex  5409  exss  5444  brv  5454  opwo0id  5480  moop2  5485  0sn0ep  5565  po0  5586  epse  5643  relxp  5679  rel0  5785  relopabiv  5807  relopabi  5809  relopabiALT  5810  eliunxp  5823  opeliunxp2  5824  dmi  5911  dmep  5913  xpidtr  6122  xpima  6180  dmsn0  6210  cnvsn0  6211  0elon  6416  funmpt  6574  funmpt2  6575  funcnv0  6602  isarep2  6625  fresaunres2  6750  f0  6759  f10d  6855  f1o00  6856  f1oi  6859  f1oiOLD  6860  f1osn  6862  brprcneu  6871  brprcneuALT  6872  opabiotafun  6961  fvopab3ig  6985  opabex  7218  eufnfv  7227  isof1oopb  7323  ncanth  7365  mpofun  7534  reldmmpo  7544  ovid  7551  ovidig  7552  ovidi  7553  ovig  7556  ov3  7573  caovmo  7647  relmptopab  7660  porpss  7724  uniex2  7735  uniex2OLD  7736  tfinds2  7856  finds  7889  finds2  7891  oprabex  7969  oprabex3  7970  f1stres  8006  f2ndres  8007  relmpoopab  8085  fsplitfpar  8109  poseq  8150  opeliunxp2f  8202  tpos0  8248  issmo  8331  tfrlem6OLD  8365  tfrlem8  8367  tfrlem16  8376  tfr1a  8377  tfr1  8380  tz7.44lem1  8388  seqomlem2  8434  seqomlem3  8435  seqomlem4  8436  fnseqom  8438  ord3  8465  0lt1o  8485  0we1  8487  naddf  8664  eqer  8727  ecopover  8815  mapsnf1o3  8889  ssdomg  8993  en0  9011  en0r  9013  ensn1  9014  0fi  9035  enrefnn  9039  xpcomf1o  9050  map2xp  9131  limensuci  9137  1sdom2  9204  sdom1  9206  unblem4  9251  fidomdm  9287  marypha1lem  9389  hartogslem1  9500  hartogs  9502  card2on  9512  nelaneqOLDOLD  9562  epinid0  9563  ruALT  9567  disjcsn  9568  elnanel  9572  cnvepnep  9573  inf2  9588  inf3lem6  9598  infeq5i  9601  zfinf2  9607  cantnflt  9637  cnfcom  9665  trcl  9693  tz9.1c  9695  tc2  9705  r1funlim  9734  r1fnon  9735  karden  9877  tskwe  9932  cardprclem  9961  pm54.43  9983  r0weon  9992  iunmapdisj  10003  alephfnon  10045  alephfplem4  10087  alephfp  10088  alephval3  10090  kmlem2  10131  dju1dif  10152  ackbij1  10216  ackbij2lem2  10218  ackbij2  10221  infpssrlem3  10284  hsmexlem4  10408  hsmexlem5  10409  ac2  10440  axac3  10443  ac6  10459  axdclem2  10499  dmct  10503  ondomon  10542  alephsucpw  10550  pwcfsdom  10563  cfpwsdom  10564  smobeth  10566  axpowndlem3  10579  zfcndun  10595  zfcndpow  10596  zfcndinf  10598  zfcndac  10599  wunex2  10718  uniwun  10720  wuncval2  10727  grur1  10800  axgroth5  10804  axgroth2  10805  axgroth6  10808  axgroth3  10811  grothtsk  10815  inaprc  10816  ltsopi  10868  dmaddpi  10870  dmmulpi  10871  1lt2pi  10885  nqerf  10910  addnqf  10928  mulnqf  10929  1lt2nq  10953  m1p1sr  11072  m1m1sr  11073  0lt1sr  11075  axaddf  11125  axmulf  11126  ax1cn  11129  subaddrii  11542  ixi  11838  recgt0ii  12116  nn1suc  12250  4div2e2  12407  arch  12496  un0mulcl  12533  pnf0xnn0  12579  3halfnz  12670  nummac  12756  indstr  12935  mnfltpnf  13146  ioof  13469  0nelfz1  13566  fzp1disj  13607  fzp1nel  13635  fzof  13680  fvf1tp  13818  om2uzrani  13984  om2uzf1oi  13985  uzrdglem  13989  uzrdgfni  13990  uzrdg0i  13991  ltwenn  13994  hashgf1o  14003  axdc4uzlem  14015  sq0  14224  irec  14233  facmapnn  14317  hashkf  14364  hashfxnn0  14369  hashf  14370  hash0  14399  prhash2ex  14431  hashsslei  14459  hashxplem  14466  hashbclem  14485  hashf1lem1  14488  tpf1ofv0  14529  tpfo  14533  s1dm  14642  eqs1  14646  ccat2s1p1  14663  cats1un  14754  revs1  14798  0csh0  14826  cshw1  14855  cats1fvn  14891  funcnvs1  14945  pfx2  14980  relexp0g  15055  relexpsucnnr  15058  rtrclreclem1  15090  dfrtrclrec2  15091  rtrclreclem2  15092  rtrclreclem4  15094  dfrtrcl2  15095  climmo  15604  fsumcom2  15821  ackbijnn  15878  incexclem  15886  infcvgaux1i  15907  fprodcom2  16034  bpolylem  16097  bpoly3  16107  bpoly4  16108  efcvgfsum  16135  cos1bnd  16238  cos2bnd  16239  znnen  16263  qnnen  16264  aleph1re  16296  3dvds  16384  n2dvdsm1  16422  divalglem5  16450  flodddiv4  16468  sadcaddlem  16510  sadadd2lem  16512  sadadd3  16514  sadaddlem  16519  lcmf0  16687  lcmfunsnlem2lem1  16691  lcmfunsnlem2  16693  coprmprod  16714  coprmproddvdslem  16715  2prm  16745  3lcm2e6  16786  phicl2  16822  pockthi  16962  unbenlem  16963  prmrec  16977  vdwlem13  17048  vdwnn  17053  ramcl2  17071  prmgapprmo  17117  mod2xnegi  17126  modsubi  17127  structcnvcnv  17208  strleun  17212  setsres  17233  strfv  17258  starvndxnbasendx  17352  starvndxnplusgndx  17353  starvndxnmulrndx  17354  scandxnbasendx  17364  scandxnplusgndx  17365  scandxnmulrndx  17366  vscandxnbasendx  17369  vscandxnplusgndx  17370  vscandxnmulrndx  17371  vscandxnscandx  17372  ipndxnbasendx  17380  ipndxnplusgndx  17381  ipndxnmulrndx  17382  slotsdifipndx  17383  tsetndxnplusgndx  17405  tsetndxnmulrndx  17406  tsetndxnstarvndx  17407  slotstnscsi  17408  plendxnplusgndx  17419  plendxnmulrndx  17420  plendxnscandx  17421  plendxnvscandx  17422  slotsdifplendx  17423  basendxnocndx  17431  plendxnocndx  17432  dsndxnplusgndx  17438  dsndxnmulrndx  17439  slotsdnscsi  17440  dsndxntsetndx  17441  slotsdifdsndx  17442  unifndxntsetndx  17448  slotsdifunifndx  17449  slotsdifplendx2  17464  slotsdifocndx  17465  0rest  17477  firest  17480  restid  17481  prdsval  17503  prdsbas  17505  prdsplusg  17506  prdsmulr  17507  prdsvsca  17508  imasaddfnlem  17577  imasvscafn  17586  2oppchomf  17775  0ssc  17889  0subcat  17890  idfucl  17933  homarel  18088  dmaf  18101  cdaf  18102  setc2ohom  18147  catcfuccl  18170  relxpchom  18232  catcxpccl  18258  oppchofcl  18311  oyoncl  18321  letsr  18644  nulchn  18670  s1chn  18671  chnub  18673  chninf  18686  ex-chn1  18688  mgmidmo  18713  efmndmgm  18939  smndex1ibas  18954  smndex1mgm  18964  smndex1mnd  18967  smndex2dbas  18971  smndex2dnrinv  18972  smndex2hbas  18973  pwmnd  18994  releqg  19236  ga0  19363  psgnunilem3  19561  psgnunilem4  19562  pmtrsn  19584  efgval  19782  efger  19783  efgsval2  19798  efgsp1  19802  efgsfo  19804  efgredleme  19808  efgredlem  19812  efgred  19813  cygctb  19957  gsum2d2lem  20038  gsum2d2  20039  gsumcom2  20040  dprd2d2  20111  pgpfaclem1  20148  gsumle  20210  reldvdsr  20438  fldhmsubc  20888  00lsp  21102  cnfldfun  21536  cnfldfunALT  21537  xrsmgm  21557  pzriprnglem8  21638  pzriprnglem13  21643  pzriprnglem14  21644  pzriprngALT  21645  resubdrg  21758  ocv0  21827  cssval  21832  islinds2  21963  psrvscafval  22098  psrbag0  22213  psdmvr  22332  00ply1bas  22399  ply1plusgfvi  22401  m2detleib  22788  tgdom  23135  tgidm  23137  indistps2ALT  23171  restbas  23315  resttopon  23318  rest0  23326  leordtval2  23369  iocpnfordt  23372  icomnfordt  23373  iooordt  23374  ist1-3  23506  1stcfb  23602  comppfsc  23689  1stckgen  23711  ptbasfi  23738  dfac14  23775  opnfbas  23999  hauspwpwf1  24144  alexsubALT  24208  ptcmplem5  24213  cnextrel  24220  ust0  24377  0met  24523  prdsdsf  24524  prdsxmetlem  24525  prdsmet  24527  prdsbl  24648  qtopbaslem  24915  xrtgioo  24964  xrsdsre  24968  zcld  24971  recld2  24972  reperflem  24976  retopconn  24987  iccpnfcnv  25103  bndth  25117  nmoleub2lem2  25275  zclmncvs  25307  recmet  25482  resscdrg  25517  ishl2  25529  recms  25539  volf  25688  iundisj2  25708  volsup  25715  icombl  25723  ioombl  25724  ismbf3d  25813  0plef  25831  0pledm  25832  itg1ge0  25845  mbfi1fseqlem5  25878  itg2addlem  25917  reldv  26029  limciun  26053  dvexp  26112  dveflem  26138  lhop1lem  26172  lhop  26175  elply2  26353  elplyd  26359  ply1term  26361  ply0  26365  plymullem  26373  plymul02  26441  qaa  26484  pserulm  26585  pserdvlem2  26591  efcn  26606  sincosq1lem  26662  tangtx  26670  sincos4thpi  26678  pigt3  26683  pige3ALT  26685  efif1olem4  26710  logf1o  26729  relogf1o  26731  log1  26750  loge  26751  logi  26752  relogiso  26763  dvrelog  26802  relogcn  26803  logcn  26812  cxpcn3  26913  resqrtcn  26914  rtprmirr  26925  2logb9irr  26960  leibpi  27107  log2ublem1  27111  birthday  27119  emcllem5  27164  harmonicbnd  27168  harmonicbnd2  27169  harmonicbnd3  27172  lgamgulm2  27200  lgamcvglem  27204  gamf  27207  ppiltx  27341  ppiublem1  27366  ppiub  27368  bclbnd  27444  bpos1lem  27446  bposlem8  27455  lgsquadlem2  27545  2sqlem9  27591  2sqlem10  27592  addsqnreup  27607  chebbnd1  27636  selberg2lem  27714  pntrsumo1  27729  selbergsb  27739  pntpbnd  27752  ltsval2  27820  noxp1o  27827  nosepnelem  27843  noetasuplem2  27898  noetainflem2  27902  0lt1s  28005  addsf  28175  precsexlem1  28400  precsexlem2  28401  precsexlem3  28402  precsexlem4  28403  precsexlem5  28404  precsexlem9  28408  precsexlem10  28409  precsexlem11  28410  elons2  28451  oncutlt  28457  oniso  28464  onswe  28465  onsse  28466  onaddscl  28470  onmulscl  28471  onsbnd  28474  eln0s  28554  0zs  28581  zseo  28615  twocut  28616  0reno  28689  1reno  28690  lngndxnitvndx  28712  istrkg2ld  28729  tgcgr4  28800  ax5seglem7  29285  axlowdimlem4  29295  axlowdimlem6  29297  axlowdimlem7  29298  axlowdimlem10  29301  axlowdimlem13  29304  axlowdimlem16  29307  uhgr0e  29421  uhgr0  29423  upgrbi  29443  umgrbi  29451  usgr0  29593  lfuhgr1v0e  29604  usgrexmpllem  29610  usgrexmpl  29613  griedg0prc  29614  cplgr0  29775  usgrexilem  29790  cffldtocusgr  29797  rgrusgrprc  29939  rusgrprc  29940  rgrprcx  29942  rgrx0ndm  29943  usgr2pthlem  30112  pthdlem2  30117  uspgrn2crct  30157  wwlksnext  30242  clwwlknondisj  30462  0ewlk  30465  0wlk  30467  0pth  30476  1pthdlem1  30486  1trld  30493  wlk2v2elem2  30507  wlk2v2e  30508  upgr3v3e3cycl  30531  upgr4cycl4dv4e  30536  dfconngr1  30539  0conngr  30543  konigsbergumgr  30602  2wspmdisj  30688  2clwwlk2clwwlk  30701  numclwwlk3lem2lem  30734  numclwwlk3lem2  30735  ex-dif  30774  ex-in  30776  ex-eprel  30784  ex-id  30785  ex-fl  30798  ex-mod  30800  ex-hash  30804  ex-fpar  30813  avril1  30814  2bornot2b  30815  0vfval  30958  vsfval  30985  ajmoi  31210  ajfuni  31211  normlem2  31463  norm3adifii  31500  hhip  31529  hlim0  31587  hlimcaui  31588  hlimf  31589  hhssnv  31616  shscli  31669  shsval2i  31739  h1de2i  31905  fh3i  31975  fh4i  31976  cm2mi  31978  qlaxr3i  31988  mayetes3i  32081  ho0f  32103  hoif  32106  hodidi  32139  ho0subi  32147  hosd1i  32174  adjmo  32184  nmopsetn0  32217  nmfnsetn0  32230  funadj  32238  funcnvadj  32245  nmcexi  32378  cnlnadjlem8  32426  nmoptri2i  32451  opsqrlem4  32495  hmopidmchi  32503  pjoci  32532  pjinvari  32543  abrexdomjm  32853  elim2ifim  32891  iundisj2f  32935  rinvf1o  32975  dfcnv2  33020  snct  33057  fzodif2  33136  iundisj2fi  33142  dp2lt10  33203  dp2ltc  33206  dplti  33224  dpgti  33225  dpexpp1  33227  xrge0slmod  33668  isconstr  34126  zarcls  34264  zartopn  34265  xrge0pluscn  34330  qqhre  34410  esumrnmpt2  34458  esumfsup  34460  esumpcvgval  34468  hasheuni  34475  esumcvg  34476  esumcvgsum  34478  esumsup  34479  esum2d  34483  dmsigagen  34534  ldgenpisyslem3  34555  measvuni  34604  voliune  34619  volfiniune  34620  br2base  34659  dya2iocuni  34673  eulerpartlem1  34757  eulerpartlemt  34761  eulerpartgbij  34762  fib0  34789  coinfliprv  34873  ballotlem2  34879  ballotlemic  34897  ballotlem7  34926  ballotth  34928  rpsqrtcn  34980  chtvalz  35016  circlemethnat  35028  circlevma  35029  circlemethhgt  35030  hgt750lem  35038  bnj226  35123  bnj1101  35173  bnj110  35246  bnj149  35263  bnj150  35264  bnj151  35265  bnj517  35273  bnj580  35301  bnj865  35311  bnj900  35317  bnj996  35344  bnj1110  35370  bnj1133  35377  bnj1128  35378  bnj1145  35381  bnj1137  35383  bnj1171  35388  bnj1176  35393  axnulALT2  35471  fineqvnttrclse  35537  setinds2regs  35544  tz9.1regs  35547  f1resfz0f1d  35605  subfacp1lem5  35676  subfacp1lem6  35677  kur14lem9  35706  cvmcov2  35767  cvmliftlem1  35777  cvmliftlem4  35780  cvmliftlem5  35781  gonanegoal  35844  satfv0  35850  satfv0fun  35863  fmlan0  35883  gonan0  35884  fmla0disjsuc  35890  ex-sategoelel12  35919  msrfo  36038  problem5  36161  brtpid1  36213  brtpid2  36214  brtpid3  36215  faclimlem1  36235  axextndbi  36294  txprel  36369  relsset  36378  relbigcup  36387  fvbigcup  36392  fnsingle  36409  fvsingle  36410  snelsingles  36412  funimage  36418  fullfunfnv  36438  imagesset  36445  funtransport  36523  colinrel  36549  funray  36632  funline  36634  0hf  36669  nmulr0  36687  neibastop2lem  36871  filnetlem3  36891  nrmo  36921  waj-ax  36925  lukshef-ax2  36926  arg-ax  36927  limsucncmpi  36956  ttctr  37004  dfttc2g  37017  ttcuniun  37021  ttcuni  37024  dfttc4lem2  37040  regsfromregtco  37049  dnizeq0  37064  knoppcnlem8  37089  knoppcnlem11  37092  cnndvlem1  37126  bj-babylob  37197  bj-ax12ssb  37280  bj-nnfnth  37376  bj-snsetex  37599  bj-0eltag  37614  bj-2upln0  37659  bj-2upln1upl  37660  bj-snexg  37670  bj-unexg  37674  bj-adjg1  37679  bj-axseprep  37711  f1omptsnlem  37982  f1omptsn  37983  icoreresf  37998  relowlssretop  38009  relowlpssretop  38010  domalom  38050  matunitlindf  38269  poimirlem3  38274  poimirlem9  38280  poimirlem16  38287  poimirlem17  38288  poimirlem18  38289  poimirlem19  38290  poimirlem20  38291  poimirlem26  38297  mblfinlem1  38308  mblfinlem2  38309  ismblfin  38312  voliunnfl  38315  cnambfre  38319  abrexdom  38381  fdc  38396  cncfres  38416  heibor1lem  38460  grposnOLD  38533  bicontr  38731  an12i  38747  tsim1  38779  ac6s6f  38822  vvdifopab  38914  brcnvrabga  38991  opabf  39025  xrnrel  39031  relqmap  39101  dmsucmap  39117  mopre  39120  relcoels  39163  cnvcosseq  39176  refrelcoss3  39202  refrelcoss2  39203  symrelcoss2  39205  refrelcoss  39252  symrelcoss  39293  n0eldmqs  39381  ax13fromc9  39680  dedths  39736  renegclALT  39737  12gcd5e1  42770  60gcd7e1  42772  lcmineqlem23  42818  dvrelog2  42831  dvrelog3  42832  dvrelog2b  42833  aks4d1p1p6  42840  aks4d1p1p7  42841  aks4d1p1  42843  sticksstones22  42935  25or6to4  42973  sn-axprlem3  42989  acos1half  43119  moxfr  43423  mapfzcons1  43448  diophrw  43490  0dioph  43509  vdioph  43510  rabren3dioph  43542  2nn0ind  43672  rpnnen3  43759  kelac2lem  43791  frlmpwfi  43825  oaordnrex  44022  omnord1ex  44031  oenord1ex  44042  oaomoencom  44044  ifpbiidcor2  44209  iscard4  44259  sqrtcval  44367  resqrtvalex  44371  eliunov2  44405  xphe  44507  0he  44508  he0  44510  snhesn  44512  idhe  44513  frege54cor1c  44641  clsk1independent  44772  neicvgnvor  44842  amgm2d  44924  amgm3d  44925  amgm4d  44926  ismnushort  45011  lhe4.4ex1a  45039  rusbcALT  45148  ipo0  45158  ifr0  45159  vk15.4j  45237  2sb5nd  45269  dfvd1ir  45282  dfvd2anir  45293  dfvd2ir  45295  dfvd3ir  45302  dfvd3anir  45305  iden2  45323  e0bir  45485  uun2221p1  45522  uun2221p2  45523  2sb5ndVD  45618  2sb5ndALT  45640  iunconnlem2  45643  trwf  45668  wfaxext  45702  wfaxpow  45706  wfaxinf2  45710  wfac8prim  45711  permaxinf2lem  45721  nregmodelf1o  45724  fnchoice  45749  unisn0  45774  eliincex  45828  icof  45935  fnmptif  45980  supminfxr  46178  rexanuz2nf  46206  fsumiunss  46291  climlimsupcex  46483  liminfltlimsupex  46495  liminflelimsupcex  46511  xlimrel  46534  xlimfun  46569  resincncf  46589  dvnprodlem3  46662  volioc  46686  volico  46697  dmvolss  46699  volioof  46701  stoweidlem13  46727  stoweidlem34  46748  stirlinglem5  46792  stirlinglem13  46800  stirlingr  46804  fourierdlem42  46863  fourierdlem62  46882  fouriersw  46945  etransc  46997  salexct  47048  salexct2  47053  salgencntex  47057  sge0rnn0  47082  gsumge0cl  47085  sge00  47090  sge0resplit  47120  sge0reuz  47161  omeiunle  47231  0ome  47243  icoresmbl  47257  ovn0lem  47279  ovnhoilem1  47315  hspmbl  47343  nsssmfmbf  47493  mbfpsssmf  47497  smfresal  47502  smfmullem4  47508  smfpimbor1lem1  47512  smfpimbor1lem2  47513  quantgodel  47588  nthrucw  47607  goldratmolem2  47623  lambert0  47624  lamberte  47625  cjnpoly  47626  tannpoly  47627  sinnpoly  47628  aistia  47634  aisfina  47635  aiffnbandciffatnotciffb  47641  axorbciffatcxorb  47642  abnotbtaxb  47652  abnotataxb  47653  eusnsn  47763  aiotaval  47832  aiota0ndef  47834  fundcmpsurinjimaid  48160  ichv  48198  ichf  48199  ichid  48200  icht  48201  ichcircshi  48203  icheq  48211  spr0nelg  48225  m3prm  48344  m7prm  48352  0noddALTV  48454  2noddALTV  48458  341fppr2  48499  9fppr8  48502  nfermltl8rev  48507  nfermltl2rev  48508  nfermltlrev  48509  sbgoldbo  48552  nnsum3primes4  48553  evengpop3  48563  stgr1  48726  usgrexmpl1lem  48786  usgrexmpl1  48787  usgrexmpl1tri  48790  usgrexmpl2lem  48791  usgrexmpl2  48792  usgrexmpl2nb0  48796  usgrexmpl2nb1  48797  usgrexmpl2nb2  48798  usgrexmpl2nb3  48799  usgrexmpl2nb4  48800  usgrexmpl2nb5  48801  gpgedg2ov  48831  gpgedg2iv  48832  gpg5nbgrvtx03starlem1  48833  gpg5nbgrvtx03starlem2  48834  gpg5nbgrvtx03starlem3  48835  gpg5nbgrvtx13starlem1  48836  gpg5nbgrvtx13starlem2  48837  gpg5nbgrvtx13starlem3  48838  gpg5grlim  48858  gpg5grlic  48859  gpgprismgr4cycllem2  48861  gpgprismgr4cycllem7  48866  pg4cyclnex  48892  gpg5edgnedg  48895  grlimedgnedg  48896  oddinmgm  48940  nn0mnd  48944  2zrngamgm  49010  2zrngaabl  49015  2zrngmmgm  49017  2zrngnring  49023  fldhmsubcALTV  49098  eliunxp2  49114  zlmodzxzldeplem  49278  zlmodzxzldep  49284  ldepslinc  49289  rrx2xpreen  49499  rrx2plordisom  49503  line2ylem  49531  line2  49532  line2x  49534  inlinecirc02plem  49566  mosn  49591  mof0  49616  mof0ALT  49618  tposrescnv  49657  tposres3  49659  tposideq2  49667  f1omoOLD  49672  nelsubc3  49849  reldmxpc  50024  reldmprcof1  50159  setc1onsubc  50380  reldmlmd2  50431  reldmcmd2  50432  rellmd  50437  relcmd  50438  ex-gte  50507  empty-surprise  50560  eximp-surprise2  50563  amgmw2d  50624