Theorem mpbir 233

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

Syntax hints:   ↔ wb 208

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 209

This theorem is referenced by:  pm5.74ri  274  con4bii  323  imnani  404  mpbir2an  721  imorri  866  orri  873  mpbir3an  1354  xorexmid  1546  tru  1563  had1  1622  nic-mpALT  1691  nic-ax  1692  nic-axALT  1693  nfi  1807  mpgbir  1818  nfxfr  1872  19.35ri  1898  ax5e  1931  ax6ev  1988  sbt  2094  equsb1v  2138  ax13  2405  ax13ALT  2455  moanmo  2648  axi12  2731  axbnd  2732  axexte  2734  axextmo  2737  nulmo  2738  vexw  2745  eqeltri  2857  nfcxfr  2921  neir  2959  neirr  2965  eqnetri  3026  nelir  3063  mprgbir  3082  issetri  3472  moeq  3668  rmoeq  3699  cdeqi  3726  eqsstri  3980  vn0  4295  rmo0  4312  ab0orv  4333  rab0  4336  rabnc  4342  reuprg  4659  tpid1  4724  tpid2  4726  mosneq  4797  pwv  4859  uni0OLD  4892  int0  4917  eqbrtri  5118  tr0  5217  trv  5218  zfrep4  5240  axnulALT  5251  0ex  5254  inex1  5270  elpwi2  5288  0elpw  5309  axpow2  5321  dvdemo1  5327  vpwex  5331  zfpair2  5388  prex  5392  exss  5427  brv  5437  opwo0id  5463  moop2  5468  0sn0ep  5547  po0  5568  epse  5625  relxp  5661  rel0  5767  relopabiv  5789  relopabi  5791  relopabiALT  5792  eliunxp  5805  opeliunxp2  5806  dmi  5893  dmep  5895  xpidtr  6105  xpima  6163  dmsn0  6191  cnvsn0  6192  0elon  6396  funmpt  6554  funmpt2  6555  funcnv0  6582  isarep2  6606  fresaunres2  6731  f0  6740  f10d  6836  f1o00  6837  f1oi  6840  f1oiOLD  6841  f1osn  6843  brprcneu  6852  brprcneuALT  6853  opabiotafun  6942  fvopab3ig  6966  opabex  7199  eufnfv  7208  isof1oopb  7304  ncanth  7346  mpofun  7515  reldmmpo  7525  ovid  7532  ovidig  7533  ovidi  7534  ovig  7537  ov3  7554  caovmo  7628  relmptopab  7641  porpss  7705  uniex2  7716  tfinds2  7839  finds  7872  finds2  7874  oprabex  7952  oprabex3  7953  f1stres  7989  f2ndres  7990  relmpoopab  8067  fsplitfpar  8091  poseq  8132  opeliunxp2f  8184  tpos0  8230  issmo  8313  tfrlem6OLD  8347  tfrlem8  8349  tfrlem16  8358  tfr1a  8359  tfr1  8362  tz7.44lem1  8370  seqomlem2  8416  seqomlem3  8417  seqomlem4  8418  fnseqom  8420  ord3  8447  0lt1o  8467  0we1  8469  naddf  8646  eqer  8709  ecopover  8797  mapsnf1o3  8871  ssdomg  8975  en0  8993  en0r  8995  ensn1  8996  0fi  9017  enrefnn  9021  xpcomf1o  9032  map2xp  9113  limensuci  9119  1sdom2  9186  sdom1  9188  unblem4  9233  fidomdm  9271  marypha1lem  9373  hartogslem1  9484  hartogs  9486  card2on  9496  nelaneqOLDOLD  9546  epinid0  9547  ruALT  9551  disjcsn  9552  elnanel  9556  cnvepnep  9557  inf2  9572  inf3lem6  9582  infeq5i  9585  zfinf2  9591  cantnflt  9621  cnfcom  9649  trcl  9677  tz9.1c  9679  tc2  9689  r1funlim  9718  r1fnon  9719  karden  9847  tskwe  9902  cardprclem  9931  pm54.43  9953  r0weon  9962  iunmapdisj  9973  alephfnon  10015  alephfplem4  10057  alephfp  10058  alephval3  10060  kmlem2  10102  dju1dif  10123  ackbij1  10187  ackbij2lem2  10189  ackbij2  10192  infpssrlem3  10256  hsmexlem4  10380  hsmexlem5  10381  ac2  10412  axac3  10415  ac6  10431  axdclem2  10471  dmct  10475  ondomon  10514  alephsucpw  10522  pwcfsdom  10535  cfpwsdom  10536  smobeth  10538  axpowndlem3  10551  zfcndun  10567  zfcndpow  10568  zfcndinf  10570  zfcndac  10571  wunex2  10690  uniwun  10692  wuncval2  10699  grur1  10772  axgroth5  10776  axgroth2  10777  axgroth6  10780  axgroth3  10783  grothtsk  10787  inaprc  10788  ltsopi  10840  dmaddpi  10842  dmmulpi  10843  1lt2pi  10857  nqerf  10882  addnqf  10900  mulnqf  10901  1lt2nq  10925  m1p1sr  11044  m1m1sr  11045  0lt1sr  11047  axaddf  11097  axmulf  11098  ax1cn  11101  subaddrii  11514  ixi  11810  recgt0ii  12092  nn1suc  12226  4div2e2  12383  arch  12472  un0mulcl  12509  pnf0xnn0  12555  3halfnz  12646  nummac  12732  indstr  12911  mnfltpnf  13122  ioof  13445  0nelfz1  13542  fzp1disj  13582  fzp1nel  13610  fzof  13655  fvf1tp  13793  om2uzrani  13959  om2uzf1oi  13960  uzrdglem  13964  uzrdgfni  13965  uzrdg0i  13966  ltwenn  13969  hashgf1o  13978  axdc4uzlem  13990  sq0  14199  irec  14208  facmapnn  14292  hashkf  14339  hashfxnn0  14344  hashf  14345  hash0  14374  prhash2ex  14406  hashsslei  14433  hashxplem  14440  hashbclem  14459  hashf1lem1  14462  tpf1ofv0  14503  tpfo  14507  s1dm  14616  eqs1  14620  ccat2s1p1  14637  cats1un  14728  revs1  14772  0csh0  14800  cshw1  14829  cats1fvn  14865  funcnvs1  14919  pfx2  14954  relexp0g  15029  relexpsucnnr  15032  rtrclreclem1  15064  dfrtrclrec2  15065  rtrclreclem2  15066  rtrclreclem4  15068  dfrtrcl2  15069  climmo  15575  fsumcom2  15792  ackbijnn  15849  incexclem  15857  infcvgaux1i  15878  fprodcom2  16005  bpolylem  16069  bpoly3  16079  bpoly4  16080  efcvgfsum  16107  cos1bnd  16210  cos2bnd  16211  znnen  16235  qnnen  16236  aleph1re  16268  3dvds  16356  n2dvdsm1  16394  divalglem5  16422  flodddiv4  16440  sadcaddlem  16482  sadadd2lem  16484  sadadd3  16486  sadaddlem  16491  lcmf0  16659  lcmfunsnlem2lem1  16663  lcmfunsnlem2  16665  coprmprod  16686  coprmproddvdslem  16687  2prm  16717  3lcm2e6  16758  phicl2  16794  pockthi  16934  unbenlem  16935  prmrec  16949  vdwlem13  17020  vdwnn  17025  ramcl2  17043  prmgapprmo  17089  mod2xnegi  17098  modsubi  17099  structcnvcnv  17180  strleun  17184  setsres  17205  strfv  17230  starvndxnbasendx  17324  starvndxnplusgndx  17325  starvndxnmulrndx  17326  scandxnbasendx  17336  scandxnplusgndx  17337  scandxnmulrndx  17338  vscandxnbasendx  17341  vscandxnplusgndx  17342  vscandxnmulrndx  17343  vscandxnscandx  17344  ipndxnbasendx  17352  ipndxnplusgndx  17353  ipndxnmulrndx  17354  slotsdifipndx  17355  tsetndxnplusgndx  17377  tsetndxnmulrndx  17378  tsetndxnstarvndx  17379  slotstnscsi  17380  plendxnplusgndx  17391  plendxnmulrndx  17392  plendxnscandx  17393  plendxnvscandx  17394  slotsdifplendx  17395  basendxnocndx  17403  plendxnocndx  17404  dsndxnplusgndx  17410  dsndxnmulrndx  17411  slotsdnscsi  17412  dsndxntsetndx  17413  slotsdifdsndx  17414  unifndxntsetndx  17420  slotsdifunifndx  17421  slotsdifplendx2  17436  slotsdifocndx  17437  0rest  17449  firest  17452  restid  17453  prdsval  17475  prdsbas  17477  prdsplusg  17478  prdsmulr  17479  prdsvsca  17480  imasaddfnlem  17549  imasvscafn  17558  2oppchomf  17747  0ssc  17861  0subcat  17862  idfucl  17905  homarel  18060  dmaf  18073  cdaf  18074  setc2ohom  18119  catcfuccl  18142  relxpchom  18204  catcxpccl  18230  oppchofcl  18283  oyoncl  18293  letsr  18616  nulchn  18642  s1chn  18643  chnub  18645  chninf  18658  ex-chn1  18660  mgmidmo  18685  efmndmgm  18910  smndex1ibas  18925  smndex1mgm  18935  smndex1mnd  18938  smndex2dbas  18942  smndex2dnrinv  18943  smndex2hbas  18944  pwmnd  18965  releqg  19207  ga0  19329  psgnunilem3  19527  psgnunilem4  19528  pmtrsn  19550  efgval  19748  efger  19749  efgsval2  19764  efgsp1  19768  efgsfo  19770  efgredleme  19774  efgredlem  19778  efgred  19779  cygctb  19923  gsum2d2lem  20004  gsum2d2  20005  gsumcom2  20006  dprd2d2  20077  pgpfaclem1  20114  gsumle  20176  reldvdsr  20396  fldhmsubc  20822  00lsp  21036  cnfldfun  21426  cnfldfunALT  21427  xrsmgm  21447  pzriprnglem8  21528  pzriprnglem13  21533  pzriprnglem14  21534  pzriprngALT  21535  resubdrg  21648  ocv0  21717  cssval  21722  islinds2  21853  psrvscafval  21988  psrbag0  22103  psdmvr  22222  00ply1bas  22289  ply1plusgfvi  22291  m2detleib  22679  tgdom  23026  tgidm  23028  indistps2ALT  23062  restbas  23206  resttopon  23209  rest0  23217  leordtval2  23260  iocpnfordt  23263  icomnfordt  23264  iooordt  23265  ist1-3  23397  1stcfb  23493  comppfsc  23580  1stckgen  23602  ptbasfi  23629  dfac14  23666  opnfbas  23890  hauspwpwf1  24035  alexsubALT  24099  ptcmplem5  24104  cnextrel  24111  ust0  24268  0met  24414  prdsdsf  24415  prdsxmetlem  24416  prdsmet  24418  prdsbl  24539  qtopbaslem  24806  xrtgioo  24855  xrsdsre  24859  zcld  24862  recld2  24863  reperflem  24867  retopconn  24878  iccpnfcnv  24994  bndth  25008  nmoleub2lem2  25166  zclmncvs  25198  recmet  25373  resscdrg  25408  ishl2  25420  recms  25430  volf  25579  iundisj2  25599  volsup  25606  icombl  25614  ioombl  25615  ismbf3d  25704  0plef  25722  0pledm  25723  itg1ge0  25736  mbfi1fseqlem5  25769  itg2addlem  25808  reldv  25920  limciun  25944  dvexp  26003  dveflem  26029  lhop1lem  26063  lhop  26066  elply2  26244  elplyd  26250  ply1term  26252  ply0  26256  plymullem  26264  plymul02  26332  qaa  26375  pserulm  26473  pserdvlem2  26479  efcn  26494  sincosq1lem  26550  tangtx  26558  sincos4thpi  26566  pigt3  26571  pige3ALT  26573  efif1olem4  26598  logf1o  26617  relogf1o  26619  log1  26638  loge  26639  logi  26640  relogiso  26651  dvrelog  26690  relogcn  26691  logcn  26700  cxpcn3  26801  resqrtcn  26802  rtprmirr  26813  2logb9irr  26848  leibpi  26995  log2ublem1  26999  birthday  27007  emcllem5  27052  harmonicbnd  27056  harmonicbnd2  27057  harmonicbnd3  27060  lgamgulm2  27088  lgamcvglem  27092  gamf  27095  ppiltx  27229  ppiublem1  27254  ppiub  27256  bclbnd  27332  bpos1lem  27334  bposlem8  27343  lgsquadlem2  27433  2sqlem9  27479  2sqlem10  27480  addsqnreup  27495  chebbnd1  27524  selberg2lem  27602  pntrsumo1  27617  selbergsb  27627  pntpbnd  27640  ltsval2  27708  noxp1o  27715  nosepnelem  27731  noetasuplem2  27786  noetainflem2  27790  0lt1s  27893  addsf  28063  precsexlem1  28288  precsexlem2  28289  precsexlem3  28290  precsexlem4  28291  precsexlem5  28292  precsexlem9  28296  precsexlem10  28297  precsexlem11  28298  elons2  28339  oncutlt  28345  oniso  28352  onswe  28353  onsse  28354  onaddscl  28358  onmulscl  28359  onsbnd  28362  eln0s  28442  0zs  28469  zseo  28503  twocut  28504  0reno  28577  1reno  28578  lngndxnitvndx  28600  istrkg2ld  28617  tgcgr4  28688  ax5seglem7  29093  axlowdimlem4  29103  axlowdimlem6  29105  axlowdimlem7  29106  axlowdimlem10  29109  axlowdimlem13  29112  axlowdimlem16  29115  uhgr0e  29229  uhgr0  29231  upgrbi  29251  umgrbi  29259  usgr0  29401  lfuhgr1v0e  29412  usgrexmpllem  29418  usgrexmpl  29421  griedg0prc  29422  cplgr0  29583  usgrexilem  29598  cffldtocusgr  29605  rgrusgrprc  29747  rusgrprc  29748  rgrprcx  29750  rgrx0ndm  29751  usgr2pthlem  29920  pthdlem2  29925  uspgrn2crct  29965  wwlksnext  30050  clwwlknondisj  30270  0ewlk  30273  0wlk  30275  0pth  30284  1pthdlem1  30294  1trld  30301  wlk2v2elem2  30315  wlk2v2e  30316  upgr3v3e3cycl  30339  upgr4cycl4dv4e  30344  dfconngr1  30347  0conngr  30351  konigsbergumgr  30410  2wspmdisj  30496  2clwwlk2clwwlk  30509  numclwwlk3lem2lem  30542  numclwwlk3lem2  30543  ex-dif  30582  ex-in  30584  ex-eprel  30592  ex-id  30593  ex-fl  30606  ex-mod  30608  ex-hash  30612  ex-fpar  30621  avril1  30622  2bornot2b  30623  0vfval  30766  vsfval  30793  ajmoi  31018  ajfuni  31019  normlem2  31271  norm3adifii  31308  hhip  31337  hlim0  31395  hlimcaui  31396  hlimf  31397  hhssnv  31424  shscli  31477  shsval2i  31547  h1de2i  31713  fh3i  31783  fh4i  31784  cm2mi  31786  qlaxr3i  31796  mayetes3i  31889  ho0f  31911  hoif  31914  hodidi  31947  ho0subi  31955  hosd1i  31982  adjmo  31992  nmopsetn0  32025  nmfnsetn0  32038  funadj  32046  funcnvadj  32053  nmcexi  32186  cnlnadjlem8  32234  nmoptri2i  32259  opsqrlem4  32303  hmopidmchi  32311  pjoci  32340  pjinvari  32351  abrexdomjm  32666  elim2ifim  32704  iundisj2f  32750  rinvf1o  32793  dfcnv2  32838  snct  32875  fzodif2  32954  iundisj2fi  32960  dp2lt10  33022  dp2ltc  33025  dplti  33043  dpgti  33044  dpexpp1  33046  xrge0slmod  33495  isconstr  33994  zarcls  34132  zartopn  34133  xrge0pluscn  34198  qqhre  34278  esumrnmpt2  34326  esumfsup  34328  esumpcvgval  34336  hasheuni  34343  esumcvg  34344  esumcvgsum  34346  esumsup  34347  esum2d  34351  dmsigagen  34402  ldgenpisyslem3  34423  measvuni  34472  voliune  34487  volfiniune  34488  br2base  34527  dya2iocuni  34541  eulerpartlem1  34625  eulerpartlemt  34629  eulerpartgbij  34630  fib0  34657  coinfliprv  34741  ballotlem2  34747  ballotlemic  34765  ballotlem7  34794  ballotth  34796  rpsqrtcn  34848  chtvalz  34884  circlemethnat  34896  circlevma  34897  circlemethhgt  34898  hgt750lem  34906  bnj226  34991  bnj1101  35041  bnj110  35114  bnj149  35131  bnj150  35132  bnj151  35133  bnj517  35141  bnj580  35169  bnj865  35179  bnj900  35185  bnj996  35212  bnj1110  35238  bnj1133  35245  bnj1128  35246  bnj1145  35249  bnj1137  35251  bnj1171  35256  bnj1176  35261  axnulALT2  35338  fineqvnttrclse  35381  setinds2regs  35388  tz9.1regs  35391  f1resfz0f1d  35425  subfacp1lem5  35495  subfacp1lem6  35496  kur14lem9  35525  cvmcov2  35586  cvmliftlem1  35596  cvmliftlem4  35599  cvmliftlem5  35600  gonanegoal  35663  satfv0  35669  satfv0fun  35682  fmlan0  35702  gonan0  35703  fmla0disjsuc  35709  ex-sategoelel12  35738  msrfo  35857  problem5  35980  brtpid1  36032  brtpid2  36033  brtpid3  36034  faclimlem1  36054  axextndbi  36113  txprel  36188  relsset  36197  relbigcup  36206  fvbigcup  36211  fnsingle  36228  fvsingle  36229  snelsingles  36231  funimage  36237  fullfunfnv  36257  imagesset  36264  funtransport  36342  colinrel  36368  funray  36451  funline  36453  0hf  36488  nmulr0  36506  neibastop2lem  36681  filnetlem3  36701  nrmo  36731  waj-ax  36735  lukshef-ax2  36736  arg-ax  36737  limsucncmpi  36766  ttctr  36814  dfttc2g  36827  ttcuniun  36831  ttcuni  36834  dfttc4lem2  36850  regsfromregtco  36859  dnizeq0  36874  knoppcnlem8  36899  knoppcnlem11  36902  cnndvlem1  36936  bj-babylob  37008  bj-ax12ssb  37091  bj-nnfnth  37187  bj-snsetex  37409  bj-0eltag  37424  bj-2upln0  37469  bj-2upln1upl  37470  bj-snexg  37480  bj-unexg  37484  bj-adjg1  37489  bj-axseprep  37520  f1omptsnlem  37791  f1omptsn  37792  icoreresf  37807  relowlssretop  37818  relowlpssretop  37819  domalom  37859  matunitlindf  38078  poimirlem3  38083  poimirlem9  38089  poimirlem16  38096  poimirlem17  38097  poimirlem18  38098  poimirlem19  38099  poimirlem20  38100  poimirlem26  38106  mblfinlem1  38117  mblfinlem2  38118  ismblfin  38121  voliunnfl  38124  cnambfre  38128  abrexdom  38190  fdc  38205  cncfres  38225  heibor1lem  38269  grposnOLD  38342  bicontr  38540  an12i  38558  tsim1  38590  ac6s6f  38633  vvdifopab  38725  brcnvrabga  38802  opabf  38836  xrnrel  38842  relqmap  38912  dmsucmap  38928  mopre  38931  relcoels  38974  cnvcosseq  38987  refrelcoss3  39013  refrelcoss2  39014  symrelcoss2  39016  refrelcoss  39063  symrelcoss  39104  n0eldmqs  39192  ax13fromc9  39491  dedths  39547  renegclALT  39548  12gcd5e1  42581  60gcd7e1  42583  lcmineqlem23  42629  dvrelog2  42642  dvrelog3  42643  dvrelog2b  42644  aks4d1p1p6  42651  aks4d1p1p7  42652  aks4d1p1  42654  sticksstones22  42746  sn-axprlem3  42798  acos1half  42928  moxfr  43234  mapfzcons1  43259  diophrw  43301  0dioph  43320  vdioph  43321  rabren3dioph  43353  2nn0ind  43483  rpnnen3  43570  kelac2lem  43602  frlmpwfi  43636  oaordnrex  43833  omnord1ex  43842  oenord1ex  43853  oaomoencom  43855  ifpbiidcor2  44020  iscard4  44070  sqrtcval  44178  resqrtvalex  44182  eliunov2  44216  xphe  44318  0he  44319  he0  44321  snhesn  44323  idhe  44324  frege54cor1c  44452  clsk1independent  44583  neicvgnvor  44653  amgm2d  44735  amgm3d  44736  amgm4d  44737  ismnushort  44838  lhe4.4ex1a  44866  rusbcALT  44975  ipo0  44985  ifr0  44986  vk15.4j  45065  2sb5nd  45097  dfvd1ir  45110  dfvd2anir  45121  dfvd2ir  45123  dfvd3ir  45130  dfvd3anir  45133  iden2  45151  e0bir  45313  uun2221p1  45350  uun2221p2  45351  2sb5ndVD  45446  2sb5ndALT  45468  iunconnlem2  45471  trwf  45496  wfaxext  45530  wfaxpow  45534  wfaxinf2  45538  wfac8prim  45539  permaxinf2lem  45549  nregmodelf1o  45552  fnchoice  45570  unisn0  45595  eliincex  45649  icof  45756  fnmptif  45801  supminfxr  45999  rexanuz2nf  46027  fsumiunss  46112  climlimsupcex  46304  liminfltlimsupex  46316  liminflelimsupcex  46332  xlimrel  46355  xlimfun  46390  resincncf  46410  dvnprodlem3  46483  volioc  46507  volico  46518  dmvolss  46520  volioof  46522  stoweidlem13  46548  stoweidlem34  46569  stirlinglem5  46613  stirlinglem13  46621  stirlingr  46625  fourierdlem42  46684  fourierdlem62  46703  fouriersw  46766  etransc  46818  salexct  46869  salexct2  46874  salgencntex  46878  sge0rnn0  46903  gsumge0cl  46906  sge00  46911  sge0resplit  46941  sge0reuz  46982  omeiunle  47052  0ome  47064  icoresmbl  47078  ovn0lem  47100  ovnhoilem1  47136  hspmbl  47164  nsssmfmbf  47314  mbfpsssmf  47318  smfresal  47323  smfmullem4  47329  smfpimbor1lem1  47333  smfpimbor1lem2  47334  quantgodel  47409  nthrucw  47423  goldratmolem2  47441  lambert0  47442  lamberte  47443  cjnpoly  47444  tannpoly  47445  sinnpoly  47446  aistia  47452  aisfina  47453  aiffnbandciffatnotciffb  47459  axorbciffatcxorb  47460  abnotbtaxb  47470  abnotataxb  47471  eusnsn  47581  aiotaval  47650  aiota0ndef  47652  fundcmpsurinjimaid  47978  ichv  48016  ichf  48017  ichid  48018  icht  48019  ichcircshi  48021  icheq  48029  spr0nelg  48043  m3prm  48162  m7prm  48170  0noddALTV  48272  2noddALTV  48276  341fppr2  48317  9fppr8  48320  nfermltl8rev  48325  nfermltl2rev  48326  nfermltlrev  48327  sbgoldbo  48370  nnsum3primes4  48371  evengpop3  48381  stgr1  48544  usgrexmpl1lem  48604  usgrexmpl1  48605  usgrexmpl1tri  48608  usgrexmpl2lem  48609  usgrexmpl2  48610  usgrexmpl2nb0  48614  usgrexmpl2nb1  48615  usgrexmpl2nb2  48616  usgrexmpl2nb3  48617  usgrexmpl2nb4  48618  usgrexmpl2nb5  48619  gpgedg2ov  48649  gpgedg2iv  48650  gpg5nbgrvtx03starlem1  48651  gpg5nbgrvtx03starlem2  48652  gpg5nbgrvtx03starlem3  48653  gpg5nbgrvtx13starlem1  48654  gpg5nbgrvtx13starlem2  48655  gpg5nbgrvtx13starlem3  48656  gpg5grlim  48676  gpg5grlic  48677  gpgprismgr4cycllem2  48679  gpgprismgr4cycllem7  48684  pg4cyclnex  48710  gpg5edgnedg  48713  grlimedgnedg  48714  oddinmgm  48758  nn0mnd  48762  2zrngamgm  48828  2zrngaabl  48833  2zrngmmgm  48835  2zrngnring  48841  fldhmsubcALTV  48916  eliunxp2  48917  zlmodzxzldeplem  49081  zlmodzxzldep  49087  ldepslinc  49092  rrx2xpreen  49302  rrx2plordisom  49306  line2ylem  49334  line2  49335  line2x  49337  inlinecirc02plem  49369  mosn  49395  mof0  49420  mof0ALT  49422  tposrescnv  49461  tposres3  49463  tposideq2  49471  f1omoOLD  49476  nelsubc3  49653  reldmxpc  49828  reldmprcof1  49963  setc1onsubc  50184  reldmlmd2  50235  reldmcmd2  50236  rellmd  50241  relcmd  50242  ex-gte  50311  empty-surprise  50364  eximp-surprise2  50367  amgmw2d  50386