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 ⊢ 𝜑

This proof depends on syntax axioms:   ↔ wb 209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210

This theorem is used by:  pm5.74ri  275  con4bii  324  imnani  406  mpbir2an  724  imorri  869  orri  876  mpbir3an  1360  xorexmid  1557  tru  1574  had1  1633  had0  1634  had1OLD  1635  nic-mpALT  1705  nic-ax  1706  nic-axALT  1707  nfi  1821  mpgbir  1832  nfxfr  1886  19.35ri  1912  ax5e  1945  ax6ev  2002  sbt  2103  equsb1v  2142  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  3065  mprgbir  3084  issetri  3470  moeq  3665  rmoeq  3696  cdeqi  3723  eqsstri  3977  vn0OLD  4292  rmo0  4310  ab0orv  4332  rab0  4335  rabnc  4341  reuprg  4664  tpid1  4729  tpid2  4731  mosneq  4802  pwv  4864  uni0OLD  4897  int0  4922  eqbrtri  5126  tr0  5225  trv  5226  zfrep4  5246  axnulALT  5258  0ex  5261  inex1  5277  elpwi2  5297  0elpw  5317  axpow2  5329  dvdemo1  5335  vpwex  5339  zfpair2  5392  prex  5396  exss  5431  brv  5441  opwo0id  5469  moop2  5474  0sn0ep  5555  po0  5576  epse  5633  relxp  5669  rel0  5776  relopabiv  5798  relopabi  5800  relopabiALT  5801  eliunxp  5814  opeliunxp2  5815  dmi  5903  dmep  5905  xpidtr  6116  xpima  6174  imadifssrn  6200  dmsn0  6209  cnvsn0  6210  0elon  6417  funmpt  6576  funmpt2  6577  funcnv0  6604  isarep2  6627  fresaunres2  6752  f0  6761  f10d  6857  f1o00  6858  f1oi  6861  f1oiOLD  6862  f1osn  6864  brprcneu  6873  brprcneuALT  6874  opabiotafun  6963  fvopab3ig  6987  opabex  7224  eufnfv  7233  isof1oopb  7331  ncanth  7373  mpofun  7542  reldmmpo  7552  ovid  7559  ovidig  7560  ovidi  7561  ovig  7564  ov3  7581  caovmo  7656  relmptopab  7669  funmpt3  7685  mpt3fvd  7686  porpss  7741  uniex2  7752  uniex2OLD  7753  tfinds2  7873  finds  7906  finds2  7908  oprabex  7986  oprabex3  7987  f1stres  8023  f2ndres  8024  relmpoopab  8103  fsplitfpar  8127  poseq  8168  opeliunxp2f  8220  tpos0  8266  issmo  8349  tfrlem6OLD  8383  tfrlem8  8385  tfrlem16  8394  tfr1a  8395  tfr1  8398  tz7.44lem1  8406  seqomlem2  8454  seqomlem3  8455  seqomlem4  8456  fnseqom  8458  ord3  8485  0lt1o  8505  0we1  8507  naddf  8684  eqer  8747  ecopover  8835  mapsnf1o3  8916  ssdomg  9020  en0  9038  en0r  9040  ensn1  9041  0fi  9063  enrefnn  9067  xpcomf1o  9078  map2xp  9159  limensuci  9165  1sdom2  9232  sdom1  9234  unblem4  9280  fidomdm  9316  marypha1lem  9418  hartogslem1  9529  hartogs  9531  card2on  9541  nelaneqOLDOLD  9591  epinid0  9592  ruALT  9596  disjcsn  9597  elnanel  9601  cnvepnep  9602  inf2  9617  inf3lem6  9627  infeq5i  9630  zfinf2  9636  cantnflt  9666  cnfcom  9694  trcl  9722  tz9.1c  9724  tc2  9734  r1funlimOLD  9763  r1fun  9764  r1dmlim  9765  r1fnon  9766  0hf  9910  karden  9952  kardenOLD  9953  tskwe  10024  cardprclem  10053  pm54.43  10075  r0weon  10084  iunmapdisj  10095  alephfnon  10137  alephfplem4  10179  alephfp  10180  alephval3  10182  kmlem2  10223  dju1dif  10244  ackbij1  10308  ackbij2lem2  10310  ackbij2  10313  infpssrlem3  10376  hsmexlem4  10500  hsmexlem5  10501  ac2  10532  axac3  10535  ac6  10551  axdclem2  10591  dmct  10595  dmctOLD  10596  ondomon  10640  alephsucpw  10648  pwcfsdom  10661  cfpwsdom  10662  smobeth  10664  axpowndlem3  10677  zfcndun  10693  zfcndpow  10694  zfcndinf  10696  zfcndac  10697  wunex2  10816  uniwun  10818  wuncval2  10825  grur1  10898  axgroth5  10902  axgroth2  10903  axgroth6  10906  axgroth3  10909  grothtsk  10913  inaprc  10914  ltsopi  10966  dmaddpi  10968  dmmulpi  10969  1lt2pi  10983  nqerf  11008  addnqf  11026  mulnqf  11027  1lt2nq  11051  m1p1sr  11170  m1m1sr  11171  0lt1sr  11173  axaddf  11223  axmulf  11224  ax1cn  11227  subaddrii  11640  ixi  11938  recgt0ii  12216  nn1suc  12350  4div2e2  12507  arch  12596  un0mulcl  12633  pnf0xnn0  12679  3halfnz  12771  nummac  12857  indstr  13036  mnfltpnf  13248  ioof  13571  0nelfz1  13669  fzp1disj  13710  fzp1nel  13738  fzof  13783  f1resfz0f1d  13920  fvf1tp  13922  om2uzrani  14088  om2uzf1oi  14089  uzrdglem  14093  uzrdgfni  14094  uzrdg0i  14095  ltwenn  14098  hashgf1o  14107  axdc4uzlem  14119  sq0  14328  irec  14338  facmapnn  14422  hashkf  14469  hashfxnn0  14474  hashf  14475  hash0  14504  prhash2ex  14536  hashsslei  14564  hashxplem  14571  hashbclem  14590  hashf1lem1  14593  tpf1ofv0  14634  tpfo  14638  s1dm  14748  eqs1  14753  ccat2s1p1  14770  cats1un  14863  revs1  14907  0csh0  14937  cshw1  14966  cats1fvn  15002  funcnvs1  15056  pfx2  15091  relexp0g  15168  relexpsucnnr  15171  rtrclreclem1  15203  dfrtrclrec2  15204  rtrclreclem2  15205  rtrclreclem4  15207  dfrtrcl2  15208  climmo  15717  fsumcom2  15933  ackbijnn  15990  incexclem  15998  infcvgaux1i  16019  fprodcom2  16144  bpolylem  16207  bpoly3  16217  bpoly4  16218  efcvgfsum  16245  cos1bnd  16348  cos2bnd  16349  znnen  16373  qnnen  16374  aleph1re  16406  3dvds  16494  n2dvdsm1  16532  divalglem5  16560  flodddiv4  16578  sadcaddlem  16620  sadadd2lem  16622  sadadd3  16624  sadaddlem  16629  lcmf0  16802  lcmfunsnlem2lem1  16806  lcmfunsnlem2  16808  coprmprod  16829  coprmproddvdslem  16830  2prm  16860  3lcm2e6  16901  phicl2  16938  pockthi  17078  unbenlem  17079  prmrec  17093  vdwlem13  17164  vdwnn  17169  ramcl2  17187  prmgapprmo  17233  mod2xnegi  17242  modsubi  17243  structcnvcnv  17324  strleun  17328  setsres  17349  strfv  17374  starvndxnbasendx  17468  starvndxnplusgndx  17469  starvndxnmulrndx  17470  scandxnbasendx  17480  scandxnplusgndx  17481  scandxnmulrndx  17482  vscandxnbasendx  17485  vscandxnplusgndx  17486  vscandxnmulrndx  17487  vscandxnscandx  17488  ipndxnbasendx  17496  ipndxnplusgndx  17497  ipndxnmulrndx  17498  slotsdifipndx  17499  tsetndxnplusgndx  17521  tsetndxnmulrndx  17522  tsetndxnstarvndx  17523  slotstnscsi  17524  plendxnplusgndx  17535  plendxnmulrndx  17536  plendxnscandx  17537  plendxnvscandx  17538  slotsdifplendx  17539  basendxnocndx  17547  plendxnocndx  17548  dsndxnplusgndx  17554  dsndxnmulrndx  17555  slotsdnscsi  17556  dsndxntsetndx  17557  slotsdifdsndx  17558  unifndxntsetndx  17564  slotsdifunifndx  17565  slotsdifplendx2  17580  slotsdifocndx  17581  0rest  17593  firest  17596  restid  17597  prdsval  17619  prdsbas  17621  prdsplusg  17622  prdsmulr  17623  prdsvsca  17624  imasaddfnlem  17693  imasvscafn  17702  2oppchomf  17891  0ssc  18005  0subcat  18006  idfucl  18049  homarel  18204  dmaf  18217  cdaf  18218  setc2ohom  18263  catcfuccl  18286  relxpchom  18348  catcxpccl  18374  oppchofcl  18427  oyoncl  18437  letsr  18760  nulchn  18786  s1chn  18787  chnub  18789  chninf  18802  ex-chn1  18804  mgmidmo  18831  efmndmgm  19074  smndex1ibas  19089  smndex1mgm  19099  smndex1mnd  19102  smndex2dbas  19106  smndex2dnrinv  19107  smndex2hbas  19108  degenmgm  19130  degenmgm2nfun  19132  degenmgm2  19133  pwmnd  19136  releqg  19378  ga0  19505  psgnunilem3  19703  psgnunilem4  19704  pmtrsn  19726  efgval  19924  efger  19925  efgsval2  19940  efgsp1  19944  efgsfo  19946  efgredleme  19950  efgredlem  19954  efgred  19955  cygctb  20099  gsum2d2lem  20180  gsum2d2  20181  gsumcom2  20182  dprd2d2  20253  pgpfaclem1  20290  gsumle  20352  reldvdsr  20583  fldhmsubc  21035  00lsp  21249  cnfldfun  21685  cnfldfunALT  21686  xrsmgm  21706  pzriprnglem8  21787  pzriprnglem13  21792  pzriprnglem14  21793  pzriprngALT  21794  resubdrg  21907  ocv0  21976  cssval  21981  islinds2  22112  psrvscafval  22249  psrbag0  22364  psdmvr  22483  00ply1bas  22550  ply1plusgfvi  22552  m2detleib  22939  matunitlindf  22989  tgdom  23289  tgidm  23291  indistps2ALT  23325  restbas  23469  resttopon  23472  rest0  23480  leordtval2  23523  iocpnfordt  23526  icomnfordt  23527  iooordt  23528  ist1-3  23660  1stcfb  23756  comppfsc  23844  1stckgen  23866  ptbasfi  23893  dfac14  23930  opnfbas  24154  hauspwpwf1  24299  alexsubALT  24363  ptcmplem5  24368  cnextrel  24375  ust0  24532  0met  24678  prdsdsf  24679  prdsxmetlem  24680  prdsmet  24682  prdsbl  24803  qtopbaslem  25070  xrtgioo  25119  xrsdsre  25123  zcld  25126  recld2  25127  reperflem  25131  retopconn  25142  iccpnfcnv  25258  bndth  25272  nmoleub2lem2  25430  zclmncvs  25462  recmet  25637  resscdrg  25672  ishl2  25684  recms  25694  volf  25843  iundisj2  25863  volsup  25870  icombl  25878  ioombl  25879  ismbf3d  25968  0plef  25986  0pledm  25987  itg1ge0  26000  mbfi1fseqlem5  26033  itg2addlem  26072  reldv  26183  limciun  26207  dvexp  26266  dveflem  26292  lhop1lem  26326  lhop  26329  elply2  26507  elplyd  26513  ply1term  26515  ply0  26519  plymullem  26528  plymul02  26594  qaa  26640  pserulm  26742  pserdvlem2  26748  efcn  26763  sincosq1lem  26819  tangtx  26827  sincos4thpi  26835  pigt3  26839  pige3ALT  26841  efif1olem4  26866  logf1o  26885  relogf1o  26887  log1  26906  loge  26907  logi  26908  relogiso  26919  dvrelog  26958  relogcn  26959  logcn  26968  cxpcn3  27069  resqrtcn  27070  rtprmirr  27081  2logb9irr  27116  leibpi  27263  log2ublem1  27267  birthday  27275  emcllem5  27320  harmonicbnd  27324  harmonicbnd2  27325  harmonicbnd3  27328  lgamgulm2  27356  lgamcvglem  27360  gamf  27363  ppiltx  27497  ppiublem1  27522  ppiub  27524  bclbnd  27600  bpos1lem  27602  bposlem8  27611  lgsquadlem2  27701  2sqlem9  27747  2sqlem10  27748  addsqnreup  27763  chebbnd1  27792  selberg2lem  27870  pntrsumo1  27885  selbergsb  27895  pntpbnd  27908  ltsval2  28006  noxp1o  28013  nosepnelem  28029  noetasuplem2  28084  noetainflem2  28088  0lt1s  28191  addsf  28361  precsexlem1  28586  precsexlem2  28587  precsexlem3  28588  precsexlem4  28589  precsexlem5  28590  precsexlem9  28594  precsexlem10  28595  precsexlem11  28596  elons2  28637  oncutlt  28643  oniso  28650  onswe  28651  onsse  28652  onaddscl  28656  onmulscl  28657  onsbnd  28660  eln0s  28740  0zs  28767  zseo  28801  twocut  28802  0reno  28875  1reno  28876  lngndxnitvndx  28898  istrkg2ld  28915  tgcgr4  28987  ax5seglem7  29506  axlowdimlem4  29516  axlowdimlem6  29518  axlowdimlem7  29519  axlowdimlem10  29522  axlowdimlem13  29525  axlowdimlem16  29528  uhgr0e  29642  uhgr0  29644  upgrbi  29664  umgrbi  29672  usgr0  29817  lfuhgr1v0e  29828  usgrexmpllem  29834  usgrexmpl  29837  griedg0prc  29838  cplgr0  29999  usgrexilem  30014  cffldtocusgr  30021  rgrusgrprc  30163  rusgrprc  30164  rgrprcx  30166  rgrx0ndm  30167  usgr2pthlem  30342  pthdlem2  30347  uspgrn2crct  30390  wwlksnext  30475  clwwlknondisj  30695  0ewlk  30698  0wlk  30700  0pth  30709  1pthdlem1  30719  1trld  30726  wlk2v2elem2  30750  wlk2v2e  30751  upgr3v3e3cycl  30774  upgr4cycl4dv4e  30779  dfconngr1  30782  0conngr  30786  konigsbergumgr  30845  2wspmdisj  30931  2clwwlk2clwwlk  30944  numclwwlk3lem2lem  30977  numclwwlk3lem2  30978  ex-dif  31017  ex-in  31019  ex-eprel  31027  ex-id  31028  ex-fl  31041  ex-mod  31043  ex-hash  31047  ex-fpar  31056  avril1  31057  2bornot2b  31058  0vfval  31201  vsfval  31228  ajmoi  31453  ajfuni  31454  normlem2  31706  norm3adifii  31743  hhip  31772  hlim0  31830  hlimcaui  31831  hlimf  31832  hhssnv  31859  shscli  31912  shsval2i  31982  h1de2i  32148  fh3i  32218  fh4i  32219  cm2mi  32221  qlaxr3i  32231  mayetes3i  32324  ho0f  32346  hoif  32349  hodidi  32382  ho0subi  32390  hosd1i  32417  adjmo  32427  nmopsetn0  32460  nmfnsetn0  32473  funadj  32481  funcnvadj  32488  nmcexi  32621  cnlnadjlem8  32669  nmoptri2i  32694  opsqrlem4  32738  hmopidmchi  32746  pjoci  32775  pjinvari  32786  abrexdomjm  33096  elim2ifim  33134  iundisj2f  33177  rinvf1o  33217  dfcnv2  33262  snct  33298  fzodif2  33376  iundisj2fi  33382  dp2lt10  33443  dp2ltc  33446  dplti  33464  dpgti  33465  dpexpp1  33467  xrge0slmod  33902  isconstr  34361  zarcls  34499  zartopn  34500  xrge0pluscn  34565  qqhre  34645  esumrnmpt2  34693  esumfsup  34695  esumpcvgval  34703  hasheuni  34710  esumcvg  34711  esumcvgsum  34713  esumsup  34714  esum2d  34718  dmsigagen  34770  ldgenpisyslem3  34791  measvuni  34840  voliune  34855  volfiniune  34856  br2base  34894  dya2iocuni  34908  eulerpartlem1  34992  eulerpartlemt  34996  eulerpartgbij  34997  fib0  35024  coinfliprv  35108  ballotlem2  35114  ballotlemic  35132  ballotlem7  35161  ballotth  35163  rpsqrtcn  35215  chtvalz  35251  circlemethnat  35263  circlevma  35264  circlemethhgt  35265  hgt750lem  35273  bnj226  35358  bnj1101  35408  bnj110  35481  bnj149  35498  bnj150  35499  bnj151  35500  bnj517  35508  bnj580  35536  bnj865  35546  bnj900  35552  bnj996  35579  bnj1110  35605  bnj1133  35612  bnj1128  35613  bnj1145  35616  bnj1137  35618  bnj1171  35623  bnj1176  35628  axnulALT2  35704  fineqvnttrclse  35775  setinds2regs  35782  tz9.1regs  35785  subfacp1lem5  35928  subfacp1lem6  35929  kur14lem9  35958  cvmcov2  36019  cvmliftlem1  36029  cvmliftlem4  36032  cvmliftlem5  36033  gonanegoal  36096  satfv0  36102  satfv0fun  36115  fmlan0  36135  gonan0  36136  fmla0disjsuc  36142  ex-sategoelel12  36171  msrfo  36290  problem5  36413  brtpid1  36465  brtpid2  36466  brtpid3  36467  faclimlem1  36487  axextndbi  36546  txprel  36621  relsset  36630  relbigcup  36639  fvbigcup  36644  fnsingle  36661  fvsingle  36662  snelsingles  36664  funimage  36670  fullfunfnv  36690  imagesset  36697  funtransport  36776  colinrel  36802  funray  36885  funline  36887  nmulr0  36924  neibastop2lem  37128  filnetlem3  37148  nrmo  37178  waj-ax  37182  lukshef-ax2  37183  arg-ax  37184  limsucncmpi  37213  ttctr  37261  dfttc2g  37274  ttcuniun  37278  ttcuni  37281  dfttc4lem2  37297  regsfromregtco  37306  dnizeq0  37321  knoppcnlem8  37346  knoppcnlem11  37349  cnndvlem1  37383  bj-babylob  37454  bj-ax12ssb  37537  bj-nnfnth  37633  bj-snsetex  37856  bj-0eltag  37871  bj-2upln0  37916  bj-2upln1upl  37917  bj-snexg  37927  bj-unexg  37931  bj-adjg1  37936  bj-axseprep  37970  f1omptsnlem  38239  f1omptsn  38240  icoreresf  38255  relowlssretop  38266  relowlpssretop  38267  domalom  38307  poimirlem3  38521  poimirlem9  38527  poimirlem16  38534  poimirlem17  38535  poimirlem18  38536  poimirlem19  38537  poimirlem20  38538  poimirlem26  38544  mblfinlem1  38555  mblfinlem2  38556  ismblfin  38559  voliunnfl  38562  cnambfre  38566  abrexdom  38644  fdc  38659  cncfres  38679  heibor1lem  38723  grposnOLD  38796  bicontr  38994  an12i  39010  tsim1  39042  ac6s6f  39085  vvdifopab  39177  brcnvrabga  39254  opabf  39288  xrnrel  39294  relqmap  39364  dmsucmap  39380  mopre  39383  relcoels  39426  cnvcosseq  39439  refrelcoss3  39465  refrelcoss2  39466  symrelcoss2  39468  refrelcoss  39515  symrelcoss  39556  n0eldmqs  39644  ax13fromc9  39943  dedths  39999  renegclALT  40000  12gcd5e1  43033  60gcd7e1  43035  lcmineqlem23  43081  dvrelog2  43094  dvrelog3  43095  dvrelog2b  43096  aks4d1p1p6  43103  aks4d1p1p7  43104  aks4d1p1  43106  sticksstones22  43198  25or6to4  43236  sn-axprlem3  43252  acos1half  43389  moxfr  43682  mapfzcons1  43707  diophrw  43749  0dioph  43768  vdioph  43769  rabren3dioph  43801  2nn0ind  43931  rpnnen3  44018  kelac2lem  44050  frlmpwfi  44084  oaordnrex  44281  omnord1ex  44290  oenord1ex  44301  oaomoencom  44303  ifpbiidcor2  44468  iscard4  44518  sqrtcval  44626  resqrtvalex  44630  eliunov2  44664  xphe  44766  0he  44767  he0  44769  snhesn  44771  idhe  44772  frege54cor1c  44900  clsk1independent  45031  neicvgnvor  45101  amgm2d  45183  amgm3d  45184  amgm4d  45185  ismnushort  45270  lhe4.4ex1a  45298  rusbcALT  45407  ipo0  45417  ifr0  45418  vk15.4j  45496  2sb5nd  45528  dfvd1ir  45541  dfvd2anir  45552  dfvd2ir  45554  dfvd3ir  45561  dfvd3anir  45564  iden2  45582  e0bir  45744  uun2221p1  45781  uun2221p2  45782  2sb5ndVD  45877  2sb5ndALT  45899  iunconnlem2  45902  trwf  45927  wfaxext  45961  wfaxpow  45965  wfaxinf2  45969  wfac8prim  45970  permaxinf2lem  45980  nregmodelf1o  45983  fnchoice  46015  unisn0  46040  eliincex  46094  icof  46201  fnmptif  46246  supminfxr  46443  rexanuz2nf  46471  fsumiunss  46556  climlimsupcex  46748  liminfltlimsupex  46760  liminflelimsupcex  46776  xlimrel  46799  xlimfun  46834  resincncf  46854  dvnprodlem3  46927  volioc  46951  volico  46962  dmvolss  46964  volioof  46966  stoweidlem13  46992  stoweidlem34  47013  stirlinglem5  47057  stirlinglem13  47065  stirlingr  47069  fourierdlem42  47128  fourierdlem62  47147  fouriersw  47210  etransc  47262  salexct  47313  salexct2  47318  salgencntex  47322  sge0rnn0  47347  gsumge0cl  47350  sge00  47355  sge0resplit  47385  sge0reuz  47426  omeiunle  47496  0ome  47508  icoresmbl  47522  ovn0lem  47544  ovnhoilem1  47580  hspmbl  47608  nsssmfmbf  47758  mbfpsssmf  47762  smfresal  47767  smfmullem4  47773  smfpimbor1lem1  47777  smfpimbor1lem2  47778  quantgodel  47853  numtowerdt  47885  goldratmolem2  47902  goldratmolem3  47903  goldratval  47905  lambert0  47906  lamberte  47907  cjnpoly  47908  aistia  47936  aisfina  47937  aiffnbandciffatnotciffb  47943  axorbciffatcxorb  47944  abnotbtaxb  47954  abnotataxb  47955  eusnsn  48065  aiotaval  48134  aiota0ndef  48136  fundcmpsurinjimaid  48462  ichv  48500  ichf  48501  ichid  48502  icht  48503  ichcircshi  48505  icheq  48513  spr0nelg  48527  m3prm  48646  m7prm  48654  0noddALTV  48756  2noddALTV  48760  341fppr2  48801  9fppr8  48804  nfermltl8rev  48809  nfermltl2rev  48810  nfermltlrev  48811  sbgoldbo  48854  nnsum3primes4  48855  evengpop3  48865  stgr1  49028  usgrexmpl1lem  49088  usgrexmpl1  49089  usgrexmpl1tri  49092  usgrexmpl2lem  49093  usgrexmpl2  49094  usgrexmpl2nb0  49098  usgrexmpl2nb1  49099  usgrexmpl2nb2  49100  usgrexmpl2nb3  49101  usgrexmpl2nb4  49102  usgrexmpl2nb5  49103  gpgedg2ov  49133  gpgedg2iv  49134  gpg5nbgrvtx03starlem1  49135  gpg5nbgrvtx03starlem2  49136  gpg5nbgrvtx03starlem3  49137  gpg5nbgrvtx13starlem1  49138  gpg5nbgrvtx13starlem2  49139  gpg5nbgrvtx13starlem3  49140  gpg5grlim  49160  gpg5grlic  49161  gpgprismgr4cycllem2  49163  gpgprismgr4cycllem7  49168  pg4cyclnex  49194  gpg5edgnedg  49197  grlimedgnedg  49198  oddinmgm  49241  nn0mnd  49245  2zrngamgm  49311  2zrngaabl  49316  2zrngmmgm  49318  2zrngnring  49324  fldhmsubcALTV  49399  eliunxp2  49415  zlmodzxzldeplem  49579  zlmodzxzldep  49585  ldepslinc  49590  rrx2xpreen  49800  rrx2plordisom  49804  line2ylem  49832  line2  49833  line2x  49835  inlinecirc02plem  49867  mosn  49892  mof0  49917  mof0ALT  49919  tposrescnv  49956  tposres3  49958  tposideq2  49966  f1omoOLD  49971  nelsubc3  50148  reldmxpc  50323  reldmprcof1  50458  setc1onsubc  50679  reldmlmd2  50730  reldmcmd2  50731  rellmd  50736  relcmd  50737  ex-gte  50791  dvsec  50825  dvcsc  50826  dvcot  50827  empty-surprise  50847  eximp-surprise2  50850  amgmw2d  50958