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  856  orri  863  mpbir3an  1342  xorexmid  1527  tru  1544  had1  1603  nic-mpALT  1672  nic-ax  1673  nic-axALT  1674  nfi  1788  mpgbir  1799  nfxfr  1853  19.35ri  1879  ax5e  1912  ax6ev  1969  sbt  2066  equsb1v  2105  ax13  2380  ax13ALT  2430  moanmo  2622  axi12  2706  axbnd  2707  axexte  2709  axextmo  2712  nulmo  2713  vexw  2720  eqeltri  2837  nfcxfr  2903  neir  2943  neirr  2949  eqnetri  3011  nelir  3049  mprgbir  3068  cbvrexdva2OLD  3350  issetri  3499  moeq  3713  rmoeq  3744  cdeqi  3771  eqsstri  4030  rmo0  4362  rabnc  4391  reuprg  4703  tpid1  4768  tpid2  4770  mosneq  4842  pwv  4904  uni0  4935  int0  4962  eqbrtri  5164  tr0  5272  trv  5273  zfrep4  5293  axnulALT  5304  0ex  5307  inex1  5317  elpwi2  5335  0elpw  5356  axpow2  5367  dvdemo1  5373  vpwex  5377  zfpair2  5433  exss  5468  brv  5477  opwo0id  5502  moop2  5507  0sn0ep  5588  po0  5609  epse  5667  relxp  5703  rel0  5809  relopabiv  5830  relopabi  5832  relopabiALT  5833  eliunxp  5848  opeliunxp2  5849  dmi  5932  dmep  5934  xpidtr  6142  xpima  6202  dmsn0  6229  cnvsn0  6230  0elon  6438  funmpt  6604  funmpt2  6605  funcnv0  6632  isarep2  6658  fresaunres2  6780  f0  6789  f10d  6882  f1o00  6883  f1oi  6886  f1osn  6888  brprcneu  6896  brprcneuALT  6897  opabiotafun  6989  fvopab3ig  7012  opabex  7240  eufnfv  7249  isof1oopb  7345  ncanth  7386  mpofun  7557  reldmmpo  7567  ovid  7574  ovidig  7575  ovidi  7576  ovig  7579  ov3  7596  caovmo  7670  relmptopab  7683  porpss  7747  uniex2  7758  tfinds2  7885  finds  7918  finds2  7920  oprabex  8001  oprabex3  8002  f1stres  8038  f2ndres  8039  relmpoopab  8119  fsplitfpar  8143  poseq  8183  opeliunxp2f  8235  tpos0  8281  wfrrelOLD  8354  wfrlem14OLD  8362  wfrlem16OLD  8364  issmo  8388  tfrlem6  8422  tfrlem8  8424  tfrlem16  8433  tfr1a  8434  tfr1  8437  tz7.44lem1  8445  seqomlem2  8491  seqomlem3  8492  seqomlem4  8493  fnseqom  8495  ord3  8523  0lt1o  8542  0we1  8544  naddf  8719  eqer  8781  ecopover  8861  mapsnf1o3  8935  ssdomg  9040  en0  9058  en0r  9060  ensn1  9061  0fi  9082  snfiOLD  9084  enrefnn  9087  xpcomf1o  9101  map2xp  9187  limensuci  9193  1sdom2  9276  sdom1  9278  sdom1OLD  9279  unblem4  9331  fidomdm  9374  marypha1lem  9473  hartogslem1  9582  hartogs  9584  card2on  9594  nelaneq  9639  epinid0  9640  ruALT  9643  disjcsn  9644  elnanel  9647  cnvepnep  9648  inf2  9663  inf3lem6  9673  infeq5i  9676  zfinf2  9682  cantnflt  9712  cnfcom  9740  trcl  9768  tz9.1c  9770  tc2  9782  r1funlim  9806  r1fnon  9807  karden  9935  tskwe  9990  cardprclem  10019  pm54.43  10041  r0weon  10052  iunmapdisj  10063  alephfnon  10105  alephfplem4  10147  alephfp  10148  alephval3  10150  kmlem2  10192  dju1dif  10213  ackbij1  10277  ackbij2lem2  10279  ackbij2  10282  infpssrlem3  10345  hsmexlem4  10469  hsmexlem5  10470  ac2  10501  axac3  10504  ac6  10520  axdclem2  10560  dmct  10564  ondomon  10603  alephsucpw  10610  pwcfsdom  10623  cfpwsdom  10624  smobeth  10626  axpowndlem3  10639  zfcndun  10655  zfcndpow  10656  zfcndinf  10658  zfcndac  10659  wunex2  10778  uniwun  10780  wuncval2  10787  grur1  10860  axgroth5  10864  axgroth2  10865  axgroth6  10868  axgroth3  10871  grothtsk  10875  inaprc  10876  ltsopi  10928  dmaddpi  10930  dmmulpi  10931  1lt2pi  10945  nqerf  10970  addnqf  10988  mulnqf  10989  1lt2nq  11013  m1p1sr  11132  m1m1sr  11133  0lt1sr  11135  axaddf  11185  axmulf  11186  ax1cn  11189  subaddrii  11598  ixi  11892  recgt0ii  12174  nn1suc  12288  neg1lt0  12383  4d2e2  12436  arch  12523  un0mulcl  12560  pnf0xnn0  12606  3halfnz  12697  nummac  12778  indstr  12958  mnfltpnf  13168  ioof  13487  0nelfz1  13583  fzp1disj  13623  fzp1nel  13651  fzof  13696  fvf1tp  13829  om2uzrani  13993  om2uzf1oi  13994  uzrdglem  13998  uzrdgfni  13999  uzrdg0i  14000  ltwenn  14003  hashgf1o  14012  axdc4uzlem  14024  sq0  14231  irec  14240  facmapnn  14324  hashkf  14371  hashfxnn0  14376  hashf  14377  hash0  14406  prhash2ex  14438  hashsslei  14465  hashxplem  14472  hashbclem  14491  hashf1lem1  14494  tpf1ofv0  14535  tpfo  14539  s1dm  14646  eqs1  14650  ccat2s1p1  14667  cats1un  14759  revs1  14803  0csh0  14831  cshw1  14860  cats1fvn  14897  funcnvs1  14951  pfx2  14986  relexp0g  15061  relexpsucnnr  15064  rtrclreclem1  15096  dfrtrclrec2  15097  rtrclreclem2  15098  rtrclreclem4  15100  dfrtrcl2  15101  climmo  15593  fsumcom2  15810  ackbijnn  15864  incexclem  15872  infcvgaux1i  15893  fprodcom2  16020  bpolylem  16084  bpoly3  16094  bpoly4  16095  efcvgfsum  16122  cos1bnd  16223  cos2bnd  16224  znnen  16248  qnnen  16249  aleph1re  16281  3dvds  16368  n2dvdsm1  16406  divalglem5  16434  flodddiv4  16452  sadcaddlem  16494  sadadd2lem  16496  sadadd3  16498  sadaddlem  16503  lcmf0  16671  lcmfunsnlem2lem1  16675  lcmfunsnlem2  16677  coprmprod  16698  coprmproddvdslem  16699  2prm  16729  3lcm2e6  16769  phicl2  16805  pockthi  16945  unbenlem  16946  prmrec  16960  vdwlem13  17031  vdwnn  17036  ramcl2  17054  prmgapprmo  17100  mod2xnegi  17109  modsubi  17110  structcnvcnv  17190  strleun  17194  setsres  17215  strfv  17240  starvndxnbasendx  17348  starvndxnplusgndx  17349  starvndxnmulrndx  17350  scandxnbasendx  17360  scandxnplusgndx  17361  scandxnmulrndx  17362  vscandxnbasendx  17365  vscandxnplusgndx  17366  vscandxnmulrndx  17367  vscandxnscandx  17368  ipndxnbasendx  17376  ipndxnplusgndx  17377  ipndxnmulrndx  17378  slotsdifipndx  17379  tsetndxnplusgndx  17401  tsetndxnmulrndx  17402  tsetndxnstarvndx  17403  slotstnscsi  17404  plendxnplusgndx  17415  plendxnmulrndx  17416  plendxnscandx  17417  plendxnvscandx  17418  slotsdifplendx  17419  basendxnocndx  17427  plendxnocndx  17428  dsndxnplusgndx  17434  dsndxnmulrndx  17435  slotsdnscsi  17436  dsndxntsetndx  17437  slotsdifdsndx  17438  unifndxntsetndx  17444  slotsdifunifndx  17445  slotsdifplendx2  17461  slotsdifocndx  17462  0rest  17474  firest  17477  restid  17478  prdsval  17500  prdsbas  17502  prdsplusg  17503  prdsmulr  17504  prdsvsca  17505  imasaddfnlem  17573  imasvscafn  17582  2oppchomf  17767  rescabsOLD  17878  0ssc  17882  0subcat  17883  idfucl  17926  homarel  18081  dmaf  18094  cdaf  18095  setc2ohom  18140  catcfuccl  18163  relxpchom  18226  catcxpccl  18252  oppchofcl  18305  oyoncl  18315  odubasOLD  18337  letsr  18638  mgmidmo  18673  efmndmgm  18898  smndex1ibas  18913  smndex1mgm  18920  smndex1mnd  18923  smndex2dbas  18927  smndex2dnrinv  18928  smndex2hbas  18929  pwmnd  18950  releqg  19193  ga0  19316  oppglemOLD  19369  psgnunilem3  19514  psgnunilem4  19515  pmtrsn  19537  efgval  19735  efger  19736  efgsval2  19751  efgsp1  19755  efgsfo  19757  efgredleme  19761  efgredlem  19765  efgred  19766  cygctb  19910  gsum2d2lem  19991  gsum2d2  19992  gsumcom2  19993  dprd2d2  20064  pgpfaclem1  20101  opprlemOLD  20340  reldvdsr  20360  fldhmsubc  20786  00lsp  20979  sralemOLD  21176  srascaOLD  21184  sravscaOLD  21186  cnfldfun  21378  cnfldfunALT  21379  cnfldfunOLD  21391  cnfldfunALTOLD  21392  cnfldfunALTOLDOLD  21393  xrsmgm  21419  pzriprnglem8  21499  pzriprnglem13  21504  pzriprnglem14  21505  pzriprngALT  21506  znbaslemOLD  21554  resubdrg  21626  ocv0  21695  cssval  21700  thlbasOLD  21715  thlleOLD  21717  islinds2  21833  psrvscafval  21968  opsrbaslemOLD  22068  psrbag0  22086  psdmvr  22173  00ply1bas  22241  ply1plusgfvi  22243  matscaOLD  22420  m2detleib  22637  tgdom  22985  tgidm  22987  indistps2ALT  23022  restbas  23166  resttopon  23169  rest0  23177  leordtval2  23220  iocpnfordt  23223  icomnfordt  23224  iooordt  23225  ist1-3  23357  1stcfb  23453  comppfsc  23540  1stckgen  23562  ptbasfi  23589  dfac14  23626  opnfbas  23850  hauspwpwf1  23995  alexsubALT  24059  ptcmplem5  24064  cnextrel  24071  ust0  24228  tuslemOLD  24276  0met  24376  prdsdsf  24377  prdsxmetlem  24378  prdsmet  24380  setsmsbasOLD  24486  setsmsdsOLD  24488  prdsbl  24504  tngdsOLD  24669  qtopbaslem  24779  xrtgioo  24828  xrsdsre  24832  zcld  24835  recld2  24836  reperflem  24840  retopconn  24851  iccpnfcnv  24975  bndth  24990  nmoleub2lem2  25149  zclmncvs  25182  recmet  25357  resscdrg  25392  ishl2  25404  recms  25414  volf  25564  iundisj2  25584  volsup  25591  icombl  25599  ioombl  25600  ismbf3d  25689  0plef  25707  0pledm  25708  itg1ge0  25721  mbfi1fseqlem5  25754  itg2addlem  25793  reldv  25905  limciun  25929  dvexp  25991  dveflem  26017  lhop1lem  26052  lhop  26055  elply2  26235  elplyd  26241  ply1term  26243  ply0  26247  plymullem  26255  qaa  26365  pserulm  26465  pserdvlem2  26472  efcn  26487  sincosq1lem  26539  tangtx  26547  sincos4thpi  26555  pigt3  26560  pige3ALT  26562  efif1olem4  26587  logf1o  26606  relogf1o  26608  log1  26627  loge  26628  logi  26629  relogiso  26640  dvrelog  26679  relogcn  26680  logcn  26689  cxpcn3  26791  resqrtcn  26792  rtprmirr  26803  2logb9irr  26838  leibpi  26985  log2ublem1  26989  birthday  26997  emcllem5  27043  harmonicbnd  27047  harmonicbnd2  27048  harmonicbnd3  27051  lgamgulm2  27079  lgamcvglem  27083  gamf  27086  ppiltx  27220  ppiublem1  27246  ppiub  27248  bclbnd  27324  bpos1lem  27326  bposlem8  27335  lgsquadlem2  27425  2sqlem9  27471  2sqlem10  27472  addsqnreup  27487  chebbnd1  27516  selberg2lem  27594  pntrsumo1  27609  selbergsb  27619  pntpbnd  27632  sltval2  27701  noxp1o  27708  nosepnelem  27724  noetasuplem2  27779  noetainflem2  27783  0slt1s  27874  addsf  28015  precsexlem1  28231  precsexlem2  28232  precsexlem3  28233  precsexlem4  28234  precsexlem5  28235  precsexlem9  28239  precsexlem10  28240  precsexlem11  28241  elons2  28281  onaddscl  28286  onmulscl  28287  eln0s  28358  0zs  28374  zseo  28406  nohalf  28407  lngndxnitvndx  28451  istrkg2ld  28468  tgcgr4  28539  ttgvalOLD  28884  ttglemOLD  28886  cchhllemOLD  28902  ax5seglem7  28950  axlowdimlem4  28960  axlowdimlem6  28962  axlowdimlem7  28963  axlowdimlem10  28966  axlowdimlem13  28969  axlowdimlem16  28972  uhgr0e  29088  uhgr0  29090  upgrbi  29110  umgrbi  29118  usgr0  29260  lfuhgr1v0e  29271  usgrexmpllem  29277  usgrexmpl  29280  griedg0prc  29281  cplgr0  29442  usgrexilem  29457  cffldtocusgr  29464  cffldtocusgrOLD  29465  rgrusgrprc  29607  rusgrprc  29608  rgrprcx  29610  rgrx0ndm  29611  usgr2pthlem  29783  pthdlem2  29788  uspgrn2crct  29828  wwlksnext  29913  clwwlknondisj  30130  0ewlk  30133  0wlk  30135  0pth  30144  1pthdlem1  30154  1trld  30161  wlk2v2elem2  30175  wlk2v2e  30176  upgr3v3e3cycl  30199  upgr4cycl4dv4e  30204  dfconngr1  30207  0conngr  30211  konigsbergumgr  30270  2wspmdisj  30356  2clwwlk2clwwlk  30369  numclwwlk3lem2lem  30402  numclwwlk3lem2  30403  ex-dif  30442  ex-in  30444  ex-eprel  30452  ex-id  30453  ex-fl  30466  ex-mod  30468  ex-hash  30472  ex-fpar  30481  avril1  30482  2bornot2b  30483  0vfval  30625  vsfval  30652  ajmoi  30877  ajfuni  30878  normlem2  31130  norm3adifii  31167  hhip  31196  hlim0  31254  hlimcaui  31255  hlimf  31256  hhssnv  31283  shscli  31336  shsval2i  31406  h1de2i  31572  fh3i  31642  fh4i  31643  cm2mi  31645  qlaxr3i  31655  mayetes3i  31748  ho0f  31770  hoif  31773  hodidi  31806  ho0subi  31814  hosd1i  31841  adjmo  31851  nmopsetn0  31884  nmfnsetn0  31897  funadj  31905  funcnvadj  31912  nmcexi  32045  cnlnadjlem8  32093  nmoptri2i  32118  opsqrlem4  32162  hmopidmchi  32170  pjoci  32199  pjinvari  32210  abrexdomjm  32526  elim2ifim  32558  iundisj2f  32603  rinvf1o  32640  dfcnv2  32686  snct  32725  fzodif2  32793  iundisj2fi  32799  dp2lt10  32866  dp2ltc  32869  dplti  32887  dpgti  32888  dpexpp1  32890  s1chn  33000  chnub  33002  gsumle  33101  xrge0slmod  33376  isconstr  33777  zarcls  33873  zartopn  33874  xrge0pluscn  33939  zlmdsOLD  33962  zlmtsetOLD  33964  qqhre  34021  esumrnmpt2  34069  esumfsup  34071  esumpcvgval  34079  hasheuni  34086  esumcvg  34087  esumcvgsum  34089  esumsup  34090  esum2d  34094  dmsigagen  34145  ldgenpisyslem3  34166  measvuni  34215  voliune  34230  volfiniune  34231  br2base  34271  dya2iocuni  34285  eulerpartlem1  34369  eulerpartlemt  34373  eulerpartgbij  34374  fib0  34401  coinfliprv  34485  ballotlem2  34491  ballotlemic  34509  ballotlem7  34538  ballotth  34540  plymul02  34561  rpsqrtcn  34608  chtvalz  34644  circlemethnat  34656  circlevma  34657  circlemethhgt  34658  hgt750lem  34666  bnj226  34748  bnj1101  34798  bnj110  34872  bnj149  34889  bnj150  34890  bnj151  34891  bnj517  34899  bnj580  34927  bnj865  34937  bnj900  34943  bnj996  34970  bnj1110  34996  bnj1133  35003  bnj1128  35004  bnj1145  35007  bnj1137  35009  bnj1171  35014  bnj1176  35019  f1resfz0f1d  35119  subfacp1lem5  35189  subfacp1lem6  35190  kur14lem9  35219  cvmcov2  35280  cvmliftlem1  35290  cvmliftlem4  35293  cvmliftlem5  35294  gonanegoal  35357  satfv0  35363  satfv0fun  35376  fmlan0  35396  gonan0  35397  fmla0disjsuc  35403  ex-sategoelel12  35432  msrfo  35551  problem5  35674  brtpid1  35721  brtpid2  35722  brtpid3  35723  faclimlem1  35743  axextndbi  35805  txprel  35880  relsset  35889  relbigcup  35898  fvbigcup  35903  fnsingle  35920  fvsingle  35921  snelsingles  35923  funimage  35929  fullfunfnv  35947  imagesset  35954  funtransport  36032  colinrel  36058  funray  36141  funline  36143  0hf  36178  neibastop2lem  36361  filnetlem3  36381  nrmo  36411  waj-ax  36415  lukshef-ax2  36416  arg-ax  36417  limsucncmpi  36446  dnizeq0  36476  knoppcnlem8  36501  knoppcnlem11  36504  cnndvlem1  36538  bj-babylob  36605  bj-ax12ssb  36659  bj-nnfnth  36744  bj-snsetex  36964  bj-0eltag  36979  bj-2upln0  37024  bj-2upln1upl  37025  bj-snexg  37035  bj-unexg  37039  bj-adjg1  37044  f1omptsnlem  37337  f1omptsn  37338  icoreresf  37353  relowlssretop  37364  relowlpssretop  37365  domalom  37405  matunitlindf  37625  poimirlem3  37630  poimirlem9  37636  poimirlem16  37643  poimirlem17  37644  poimirlem18  37645  poimirlem19  37646  poimirlem20  37647  poimirlem26  37653  mblfinlem1  37664  mblfinlem2  37665  ismblfin  37668  voliunnfl  37671  cnambfre  37675  abrexdom  37737  fdc  37752  cncfres  37772  heibor1lem  37816  grposnOLD  37889  bicontr  38087  an12i  38105  tsim1  38137  ac6s6f  38180  vvdifopab  38261  brcnvrabga  38343  opabf  38369  xrnrel  38374  relcoels  38425  cnvcosseq  38438  refrelcoss3  38464  refrelcoss2  38465  symrelcoss2  38467  refrelcoss  38524  symrelcoss  38561  n0eldmqs  38649  ax13fromc9  38907  dedths  38963  renegclALT  38964  hlhilslemOLD  41941  12gcd5e1  42004  60gcd7e1  42006  lcmineqlem23  42052  dvrelog2  42065  dvrelog3  42066  dvrelog2b  42067  aks4d1p1p6  42074  aks4d1p1p7  42075  aks4d1p1  42077  sticksstones22  42169  2xp3dxp2ge1d  42242  sn-axprlem3  42256  acos1half  42388  moxfr  42703  mapfzcons1  42728  diophrw  42770  0dioph  42789  vdioph  42790  rabren3dioph  42826  2nn0ind  42957  rpnnen3  43044  kelac2lem  43076  frlmpwfi  43110  oaordnrex  43308  omnord1ex  43317  oenord1ex  43328  oaomoencom  43330  ifpbiidcor2  43496  iscard4  43546  sqrtcval  43654  resqrtvalex  43658  eliunov2  43692  xphe  43794  0he  43795  he0  43797  snhesn  43799  idhe  43800  frege54cor1c  43928  clsk1independent  44059  neicvgnvor  44129  amgm2d  44211  amgm3d  44212  amgm4d  44213  ismnushort  44320  lhe4.4ex1a  44348  rusbcALT  44458  ipo0  44468  ifr0  44469  vk15.4j  44548  2sb5nd  44580  dfvd1ir  44593  dfvd2anir  44604  dfvd2ir  44606  dfvd3ir  44613  dfvd3anir  44616  iden2  44634  e0bir  44797  uun2221p1  44834  uun2221p2  44835  2sb5ndVD  44930  2sb5ndALT  44952  iunconnlem2  44955  trwf  44976  wfaxext  45010  wfaxpow  45014  wfaxinf2  45018  wfac8prim  45019  fnchoice  45034  unisn0  45059  eliincex  45115  icof  45224  fnmptif  45272  supminfxr  45475  rexanuz2nf  45503  fsumiunss  45590  climlimsupcex  45784  liminfltlimsupex  45796  liminflelimsupcex  45812  xlimrel  45835  xlimfun  45870  resincncf  45890  dvnprodlem3  45963  volioc  45987  volico  45998  dmvolss  46000  volioof  46002  stoweidlem13  46028  stoweidlem34  46049  stirlinglem5  46093  stirlinglem13  46101  stirlingr  46105  fourierdlem42  46164  fourierdlem62  46183  fouriersw  46246  etransc  46298  salexct  46349  salexct2  46354  salgencntex  46358  sge0rnn0  46383  gsumge0cl  46386  sge00  46391  sge0resplit  46421  sge0reuz  46462  omeiunle  46532  0ome  46544  icoresmbl  46558  ovn0lem  46580  ovnhoilem1  46616  hspmbl  46644  nsssmfmbf  46794  mbfpsssmf  46798  smfresal  46803  smfmullem4  46809  smfpimbor1lem1  46813  smfpimbor1lem2  46814  aistia  46909  aisfina  46910  aiffnbandciffatnotciffb  46916  axorbciffatcxorb  46917  abnotbtaxb  46927  abnotataxb  46928  eusnsn  47038  aiotaval  47107  aiota0ndef  47109  fundcmpsurinjimaid  47398  ichv  47436  ichf  47437  ichid  47438  icht  47439  ichcircshi  47441  icheq  47449  spr0nelg  47463  m3prm  47579  m7prm  47587  0noddALTV  47676  2noddALTV  47680  341fppr2  47721  9fppr8  47724  nfermltl8rev  47729  nfermltl2rev  47730  nfermltlrev  47731  sbgoldbo  47774  nnsum3primes4  47775  evengpop3  47785  stgr1  47928  usgrexmpl1lem  47980  usgrexmpl1  47981  usgrexmpl1tri  47984  usgrexmpl2lem  47985  usgrexmpl2  47986  usgrexmpl2nb0  47990  usgrexmpl2nb1  47991  usgrexmpl2nb2  47992  usgrexmpl2nb3  47993  usgrexmpl2nb4  47994  usgrexmpl2nb5  47995  gpg5nbgrvtx03starlem1  48024  gpg5nbgrvtx03starlem2  48025  gpg5nbgrvtx03starlem3  48026  gpg5nbgrvtx13starlem1  48027  gpg5nbgrvtx13starlem2  48028  gpg5nbgrvtx13starlem3  48029  gpg5grlic  48047  oddinmgm  48091  nn0mnd  48095  2zrngamgm  48161  2zrngaabl  48166  2zrngmmgm  48168  2zrngnring  48174  fldhmsubcALTV  48249  eliunxp2  48250  zlmodzxzldeplem  48415  zlmodzxzldep  48421  ldepslinc  48426  rrx2xpreen  48640  rrx2plordisom  48644  line2ylem  48672  line2  48673  line2x  48675  inlinecirc02plem  48707  mosn  48732  mof0  48747  mof0ALT  48749  tposrescnv  48779  tposres3  48781  tposideq2  48789  f1omo  48792  reldmxpc  48952  prstclevalOLD  49158  prstcocvalOLD  49161  ex-gte  49248  empty-surprise  49301  eximp-surprise2  49304  amgmw2d  49323