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  2143  ax13  2409  ax13ALT  2459  moanmo  2652  axi12  2735  axbnd  2736  axexte  2738  axextmo  2741  nulmo  2742  vexw  2749  eqeltri  2861  nfcxfr  2925  neir  2963  neirr  2969  eqnetri  3030  nelir  3069  mprgbir  3088  issetri  3476  moeq  3672  rmoeq  3703  cdeqi  3730  eqsstri  3984  vn0OLD  4299  rmo0  4317  ab0orv  4339  rab0  4342  rabnc  4348  reuprg  4671  tpid1  4736  tpid2  4738  mosneq  4809  pwv  4871  uni0OLD  4904  int0  4929  eqbrtri  5134  tr0  5233  trv  5234  zfrep4  5256  axnulALT  5269  0ex  5272  inex1  5288  elpwi2  5308  0elpw  5328  axpow2  5340  dvdemo1  5346  vpwex  5350  zfpair2  5407  prex  5411  exss  5446  brv  5456  opwo0id  5482  moop2  5487  0sn0ep  5567  po0  5588  epse  5645  relxp  5681  rel0  5787  relopabiv  5809  relopabi  5811  relopabiALT  5812  eliunxp  5825  opeliunxp2  5826  dmi  5913  dmep  5915  xpidtr  6124  xpima  6182  dmsn0  6212  cnvsn0  6213  0elon  6420  funmpt  6578  funmpt2  6579  funcnv0  6606  isarep2  6629  fresaunres2  6754  f0  6763  f10d  6859  f1o00  6860  f1oi  6863  f1oiOLD  6864  f1osn  6866  brprcneu  6875  brprcneuALT  6876  opabiotafun  6965  fvopab3ig  6989  opabex  7225  eufnfv  7234  isof1oopb  7332  ncanth  7374  mpofun  7543  reldmmpo  7553  ovid  7560  ovidig  7561  ovidi  7562  ovig  7565  ov3  7582  caovmo  7657  relmptopab  7670  porpss  7734  uniex2  7745  uniex2OLD  7746  tfinds2  7866  finds  7899  finds2  7901  oprabex  7979  oprabex3  7980  f1stres  8016  f2ndres  8017  relmpoopab  8095  fsplitfpar  8119  poseq  8160  opeliunxp2f  8212  tpos0  8258  issmo  8341  tfrlem6OLD  8375  tfrlem8  8377  tfrlem16  8386  tfr1a  8387  tfr1  8390  tz7.44lem1  8398  seqomlem2  8444  seqomlem3  8445  seqomlem4  8446  fnseqom  8448  ord3  8475  0lt1o  8495  0we1  8497  naddf  8674  eqer  8737  ecopover  8825  mapsnf1o3  8899  ssdomg  9003  en0  9021  en0r  9023  ensn1  9024  0fi  9046  enrefnn  9050  xpcomf1o  9061  map2xp  9142  limensuci  9148  1sdom2  9215  sdom1  9217  unblem4  9262  fidomdm  9298  marypha1lem  9400  hartogslem1  9511  hartogs  9513  card2on  9523  nelaneqOLDOLD  9573  epinid0  9574  ruALT  9578  disjcsn  9579  elnanel  9583  cnvepnep  9584  inf2  9599  inf3lem6  9609  infeq5i  9612  zfinf2  9618  cantnflt  9648  cnfcom  9676  trcl  9704  tz9.1c  9706  tc2  9716  r1funlim  9745  r1fnon  9746  karden  9895  kardenOLD  9896  tskwe  9952  cardprclem  9981  pm54.43  10003  r0weon  10012  iunmapdisj  10023  alephfnon  10065  alephfplem4  10107  alephfp  10108  alephval3  10110  kmlem2  10151  dju1dif  10172  ackbij1  10236  ackbij2lem2  10238  ackbij2  10241  infpssrlem3  10304  hsmexlem4  10428  hsmexlem5  10429  ac2  10460  axac3  10463  ac6  10479  axdclem2  10519  dmct  10523  ondomon  10562  alephsucpw  10570  pwcfsdom  10583  cfpwsdom  10584  smobeth  10586  axpowndlem3  10599  zfcndun  10615  zfcndpow  10616  zfcndinf  10618  zfcndac  10619  wunex2  10738  uniwun  10740  wuncval2  10747  grur1  10820  axgroth5  10824  axgroth2  10825  axgroth6  10828  axgroth3  10831  grothtsk  10835  inaprc  10836  ltsopi  10888  dmaddpi  10890  dmmulpi  10891  1lt2pi  10905  nqerf  10930  addnqf  10948  mulnqf  10949  1lt2nq  10973  m1p1sr  11092  m1m1sr  11093  0lt1sr  11095  axaddf  11145  axmulf  11146  ax1cn  11149  subaddrii  11562  ixi  11858  recgt0ii  12136  nn1suc  12270  4div2e2  12427  arch  12516  un0mulcl  12553  pnf0xnn0  12599  3halfnz  12691  nummac  12777  indstr  12956  mnfltpnf  13167  ioof  13490  0nelfz1  13587  fzp1disj  13628  fzp1nel  13656  fzof  13701  f1resfz0f1d  13838  fvf1tp  13840  om2uzrani  14006  om2uzf1oi  14007  uzrdglem  14011  uzrdgfni  14012  uzrdg0i  14013  ltwenn  14016  hashgf1o  14025  axdc4uzlem  14037  sq0  14246  irec  14255  facmapnn  14339  hashkf  14386  hashfxnn0  14391  hashf  14392  hash0  14421  prhash2ex  14453  hashsslei  14481  hashxplem  14488  hashbclem  14507  hashf1lem1  14510  tpf1ofv0  14551  tpfo  14555  s1dm  14665  eqs1  14670  ccat2s1p1  14687  cats1un  14780  revs1  14824  0csh0  14854  cshw1  14883  cats1fvn  14919  funcnvs1  14973  pfx2  15008  relexp0g  15083  relexpsucnnr  15086  rtrclreclem1  15118  dfrtrclrec2  15119  rtrclreclem2  15120  rtrclreclem4  15122  dfrtrcl2  15123  climmo  15632  fsumcom2  15848  ackbijnn  15905  incexclem  15913  infcvgaux1i  15934  fprodcom2  16061  bpolylem  16124  bpoly3  16134  bpoly4  16135  efcvgfsum  16162  cos1bnd  16265  cos2bnd  16266  znnen  16290  qnnen  16291  aleph1re  16323  3dvds  16411  n2dvdsm1  16449  divalglem5  16477  flodddiv4  16495  sadcaddlem  16537  sadadd2lem  16539  sadadd3  16541  sadaddlem  16546  lcmf0  16714  lcmfunsnlem2lem1  16718  lcmfunsnlem2  16720  coprmprod  16741  coprmproddvdslem  16742  2prm  16772  3lcm2e6  16813  phicl2  16849  pockthi  16989  unbenlem  16990  prmrec  17004  vdwlem13  17075  vdwnn  17080  ramcl2  17098  prmgapprmo  17144  mod2xnegi  17153  modsubi  17154  structcnvcnv  17235  strleun  17239  setsres  17260  strfv  17285  starvndxnbasendx  17379  starvndxnplusgndx  17380  starvndxnmulrndx  17381  scandxnbasendx  17391  scandxnplusgndx  17392  scandxnmulrndx  17393  vscandxnbasendx  17396  vscandxnplusgndx  17397  vscandxnmulrndx  17398  vscandxnscandx  17399  ipndxnbasendx  17407  ipndxnplusgndx  17408  ipndxnmulrndx  17409  slotsdifipndx  17410  tsetndxnplusgndx  17432  tsetndxnmulrndx  17433  tsetndxnstarvndx  17434  slotstnscsi  17435  plendxnplusgndx  17446  plendxnmulrndx  17447  plendxnscandx  17448  plendxnvscandx  17449  slotsdifplendx  17450  basendxnocndx  17458  plendxnocndx  17459  dsndxnplusgndx  17465  dsndxnmulrndx  17466  slotsdnscsi  17467  dsndxntsetndx  17468  slotsdifdsndx  17469  unifndxntsetndx  17475  slotsdifunifndx  17476  slotsdifplendx2  17491  slotsdifocndx  17492  0rest  17504  firest  17507  restid  17508  prdsval  17530  prdsbas  17532  prdsplusg  17533  prdsmulr  17534  prdsvsca  17535  imasaddfnlem  17604  imasvscafn  17613  2oppchomf  17802  0ssc  17916  0subcat  17917  idfucl  17960  homarel  18115  dmaf  18128  cdaf  18129  setc2ohom  18174  catcfuccl  18197  relxpchom  18259  catcxpccl  18285  oppchofcl  18338  oyoncl  18348  letsr  18671  nulchn  18697  s1chn  18698  chnub  18700  chninf  18713  ex-chn1  18715  mgmidmo  18742  efmndmgm  18981  smndex1ibas  18996  smndex1mgm  19006  smndex1mnd  19009  smndex2dbas  19013  smndex2dnrinv  19014  smndex2hbas  19015  degenmgm  19037  degenmgm2nfun  19039  degenmgm2  19040  pwmnd  19043  releqg  19285  ga0  19412  psgnunilem3  19610  psgnunilem4  19611  pmtrsn  19633  efgval  19831  efger  19832  efgsval2  19847  efgsp1  19851  efgsfo  19853  efgredleme  19857  efgredlem  19861  efgred  19862  cygctb  20006  gsum2d2lem  20087  gsum2d2  20088  gsumcom2  20089  dprd2d2  20160  pgpfaclem1  20197  gsumle  20259  reldvdsr  20488  fldhmsubc  20938  00lsp  21152  cnfldfun  21586  cnfldfunALT  21587  xrsmgm  21607  pzriprnglem8  21688  pzriprnglem13  21693  pzriprnglem14  21694  pzriprngALT  21695  resubdrg  21808  ocv0  21877  cssval  21882  islinds2  22013  psrvscafval  22148  psrbag0  22263  psdmvr  22382  00ply1bas  22449  ply1plusgfvi  22451  m2detleib  22838  tgdom  23185  tgidm  23187  indistps2ALT  23221  restbas  23365  resttopon  23368  rest0  23376  leordtval2  23419  iocpnfordt  23422  icomnfordt  23423  iooordt  23424  ist1-3  23556  1stcfb  23652  comppfsc  23740  1stckgen  23762  ptbasfi  23789  dfac14  23826  opnfbas  24050  hauspwpwf1  24195  alexsubALT  24259  ptcmplem5  24264  cnextrel  24271  ust0  24428  0met  24574  prdsdsf  24575  prdsxmetlem  24576  prdsmet  24578  prdsbl  24699  qtopbaslem  24966  xrtgioo  25015  xrsdsre  25019  zcld  25022  recld2  25023  reperflem  25027  retopconn  25038  iccpnfcnv  25154  bndth  25168  nmoleub2lem2  25326  zclmncvs  25358  recmet  25533  resscdrg  25568  ishl2  25580  recms  25590  volf  25739  iundisj2  25759  volsup  25766  icombl  25774  ioombl  25775  ismbf3d  25864  0plef  25882  0pledm  25883  itg1ge0  25896  mbfi1fseqlem5  25929  itg2addlem  25968  reldv  26080  limciun  26104  dvexp  26163  dveflem  26189  lhop1lem  26223  lhop  26226  elply2  26404  elplyd  26410  ply1term  26412  ply0  26416  plymullem  26424  plymul02  26492  qaa  26535  pserulm  26636  pserdvlem2  26642  efcn  26657  sincosq1lem  26713  tangtx  26721  sincos4thpi  26729  pigt3  26734  pige3ALT  26736  efif1olem4  26761  logf1o  26780  relogf1o  26782  log1  26801  loge  26802  logi  26803  relogiso  26814  dvrelog  26853  relogcn  26854  logcn  26863  cxpcn3  26964  resqrtcn  26965  rtprmirr  26976  2logb9irr  27011  leibpi  27158  log2ublem1  27162  birthday  27170  emcllem5  27215  harmonicbnd  27219  harmonicbnd2  27220  harmonicbnd3  27223  lgamgulm2  27251  lgamcvglem  27255  gamf  27258  ppiltx  27392  ppiublem1  27417  ppiub  27419  bclbnd  27495  bpos1lem  27497  bposlem8  27506  lgsquadlem2  27596  2sqlem9  27642  2sqlem10  27643  addsqnreup  27658  chebbnd1  27687  selberg2lem  27765  pntrsumo1  27780  selbergsb  27790  pntpbnd  27803  ltsval2  27871  noxp1o  27878  nosepnelem  27894  noetasuplem2  27949  noetainflem2  27953  0lt1s  28056  addsf  28226  precsexlem1  28451  precsexlem2  28452  precsexlem3  28453  precsexlem4  28454  precsexlem5  28455  precsexlem9  28459  precsexlem10  28460  precsexlem11  28461  elons2  28502  oncutlt  28508  oniso  28515  onswe  28516  onsse  28517  onaddscl  28521  onmulscl  28522  onsbnd  28525  eln0s  28605  0zs  28632  zseo  28666  twocut  28667  0reno  28740  1reno  28741  lngndxnitvndx  28763  istrkg2ld  28780  tgcgr4  28851  ax5seglem7  29340  axlowdimlem4  29350  axlowdimlem6  29352  axlowdimlem7  29353  axlowdimlem10  29356  axlowdimlem13  29359  axlowdimlem16  29362  uhgr0e  29476  uhgr0  29478  upgrbi  29498  umgrbi  29506  usgr0  29651  lfuhgr1v0e  29662  usgrexmpllem  29668  usgrexmpl  29671  griedg0prc  29672  cplgr0  29833  usgrexilem  29848  cffldtocusgr  29855  rgrusgrprc  29997  rusgrprc  29998  rgrprcx  30000  rgrx0ndm  30001  usgr2pthlem  30176  pthdlem2  30181  uspgrn2crct  30224  wwlksnext  30309  clwwlknondisj  30529  0ewlk  30532  0wlk  30534  0pth  30543  1pthdlem1  30553  1trld  30560  wlk2v2elem2  30578  wlk2v2e  30579  upgr3v3e3cycl  30602  upgr4cycl4dv4e  30607  dfconngr1  30610  0conngr  30614  konigsbergumgr  30673  2wspmdisj  30759  2clwwlk2clwwlk  30772  numclwwlk3lem2lem  30805  numclwwlk3lem2  30806  ex-dif  30845  ex-in  30847  ex-eprel  30855  ex-id  30856  ex-fl  30869  ex-mod  30871  ex-hash  30875  ex-fpar  30884  avril1  30885  2bornot2b  30886  0vfval  31029  vsfval  31056  ajmoi  31281  ajfuni  31282  normlem2  31534  norm3adifii  31571  hhip  31600  hlim0  31658  hlimcaui  31659  hlimf  31660  hhssnv  31687  shscli  31740  shsval2i  31810  h1de2i  31976  fh3i  32046  fh4i  32047  cm2mi  32049  qlaxr3i  32059  mayetes3i  32152  ho0f  32174  hoif  32177  hodidi  32210  ho0subi  32218  hosd1i  32245  adjmo  32255  nmopsetn0  32288  nmfnsetn0  32301  funadj  32309  funcnvadj  32316  nmcexi  32449  cnlnadjlem8  32497  nmoptri2i  32522  opsqrlem4  32566  hmopidmchi  32574  pjoci  32603  pjinvari  32614  abrexdomjm  32924  elim2ifim  32962  iundisj2f  33006  rinvf1o  33046  dfcnv2  33091  snct  33128  fzodif2  33206  iundisj2fi  33212  dp2lt10  33273  dp2ltc  33276  dplti  33294  dpgti  33295  dpexpp1  33297  xrge0slmod  33732  isconstr  34190  zarcls  34328  zartopn  34329  xrge0pluscn  34394  qqhre  34474  esumrnmpt2  34522  esumfsup  34524  esumpcvgval  34532  hasheuni  34539  esumcvg  34540  esumcvgsum  34542  esumsup  34543  esum2d  34547  dmsigagen  34599  ldgenpisyslem3  34620  measvuni  34669  voliune  34684  volfiniune  34685  br2base  34724  dya2iocuni  34738  eulerpartlem1  34822  eulerpartlemt  34826  eulerpartgbij  34827  fib0  34854  coinfliprv  34938  ballotlem2  34944  ballotlemic  34962  ballotlem7  34991  ballotth  34993  rpsqrtcn  35045  chtvalz  35081  circlemethnat  35093  circlevma  35094  circlemethhgt  35095  hgt750lem  35103  bnj226  35188  bnj1101  35238  bnj110  35311  bnj149  35328  bnj150  35329  bnj151  35330  bnj517  35338  bnj580  35366  bnj865  35376  bnj900  35382  bnj996  35409  bnj1110  35435  bnj1133  35442  bnj1128  35443  bnj1145  35446  bnj1137  35448  bnj1171  35453  bnj1176  35458  axnulALT2  35534  fineqvnttrclse  35594  setinds2regs  35601  tz9.1regs  35604  subfacp1lem5  35713  subfacp1lem6  35714  kur14lem9  35743  cvmcov2  35804  cvmliftlem1  35814  cvmliftlem4  35817  cvmliftlem5  35818  gonanegoal  35881  satfv0  35887  satfv0fun  35900  fmlan0  35920  gonan0  35921  fmla0disjsuc  35927  ex-sategoelel12  35956  msrfo  36075  problem5  36198  brtpid1  36250  brtpid2  36251  brtpid3  36252  faclimlem1  36272  axextndbi  36331  txprel  36406  relsset  36415  relbigcup  36424  fvbigcup  36429  fnsingle  36446  fvsingle  36447  snelsingles  36449  funimage  36455  fullfunfnv  36475  imagesset  36482  funtransport  36560  colinrel  36586  funray  36669  funline  36671  0hf  36706  nmulr0  36724  neibastop2lem  36928  filnetlem3  36948  nrmo  36978  waj-ax  36982  lukshef-ax2  36983  arg-ax  36984  limsucncmpi  37013  ttctr  37061  dfttc2g  37074  ttcuniun  37078  ttcuni  37081  dfttc4lem2  37097  regsfromregtco  37106  dnizeq0  37121  knoppcnlem8  37146  knoppcnlem11  37149  cnndvlem1  37183  bj-babylob  37254  bj-ax12ssb  37337  bj-nnfnth  37433  bj-snsetex  37656  bj-0eltag  37671  bj-2upln0  37716  bj-2upln1upl  37717  bj-snexg  37727  bj-unexg  37731  bj-adjg1  37736  bj-axseprep  37768  f1omptsnlem  38039  f1omptsn  38040  icoreresf  38055  relowlssretop  38066  relowlpssretop  38067  domalom  38107  matunitlindf  38326  poimirlem3  38331  poimirlem9  38337  poimirlem16  38344  poimirlem17  38345  poimirlem18  38346  poimirlem19  38347  poimirlem20  38348  poimirlem26  38354  mblfinlem1  38365  mblfinlem2  38366  ismblfin  38369  voliunnfl  38372  cnambfre  38376  abrexdom  38439  fdc  38454  cncfres  38474  heibor1lem  38518  grposnOLD  38591  bicontr  38789  an12i  38805  tsim1  38837  ac6s6f  38880  vvdifopab  38972  brcnvrabga  39049  opabf  39083  xrnrel  39089  relqmap  39159  dmsucmap  39175  mopre  39178  relcoels  39221  cnvcosseq  39234  refrelcoss3  39260  refrelcoss2  39261  symrelcoss2  39263  refrelcoss  39310  symrelcoss  39351  n0eldmqs  39439  ax13fromc9  39738  dedths  39794  renegclALT  39795  12gcd5e1  42828  60gcd7e1  42830  lcmineqlem23  42876  dvrelog2  42889  dvrelog3  42890  dvrelog2b  42891  aks4d1p1p6  42898  aks4d1p1p7  42899  aks4d1p1  42901  sticksstones22  42993  25or6to4  43031  sn-axprlem3  43047  acos1half  43177  moxfr  43481  mapfzcons1  43506  diophrw  43548  0dioph  43567  vdioph  43568  rabren3dioph  43600  2nn0ind  43730  rpnnen3  43817  kelac2lem  43849  frlmpwfi  43883  oaordnrex  44080  omnord1ex  44089  oenord1ex  44100  oaomoencom  44102  ifpbiidcor2  44267  iscard4  44317  sqrtcval  44425  resqrtvalex  44429  eliunov2  44463  xphe  44565  0he  44566  he0  44568  snhesn  44570  idhe  44571  frege54cor1c  44699  clsk1independent  44830  neicvgnvor  44900  amgm2d  44982  amgm3d  44983  amgm4d  44984  ismnushort  45069  lhe4.4ex1a  45097  rusbcALT  45206  ipo0  45216  ifr0  45217  vk15.4j  45295  2sb5nd  45327  dfvd1ir  45340  dfvd2anir  45351  dfvd2ir  45353  dfvd3ir  45360  dfvd3anir  45363  iden2  45381  e0bir  45543  uun2221p1  45580  uun2221p2  45581  2sb5ndVD  45676  2sb5ndALT  45698  iunconnlem2  45701  trwf  45726  wfaxext  45760  wfaxpow  45764  wfaxinf2  45768  wfac8prim  45769  permaxinf2lem  45779  nregmodelf1o  45782  fnchoice  45807  unisn0  45832  eliincex  45886  icof  45993  fnmptif  46038  supminfxr  46236  rexanuz2nf  46264  fsumiunss  46349  climlimsupcex  46541  liminfltlimsupex  46553  liminflelimsupcex  46569  xlimrel  46592  xlimfun  46627  resincncf  46647  dvnprodlem3  46720  volioc  46744  volico  46755  dmvolss  46757  volioof  46759  stoweidlem13  46785  stoweidlem34  46806  stirlinglem5  46850  stirlinglem13  46858  stirlingr  46862  fourierdlem42  46921  fourierdlem62  46940  fouriersw  47003  etransc  47055  salexct  47106  salexct2  47111  salgencntex  47115  sge0rnn0  47140  gsumge0cl  47143  sge00  47148  sge0resplit  47178  sge0reuz  47219  omeiunle  47289  0ome  47301  icoresmbl  47315  ovn0lem  47337  ovnhoilem1  47373  hspmbl  47401  nsssmfmbf  47551  mbfpsssmf  47555  smfresal  47560  smfmullem4  47566  smfpimbor1lem1  47570  smfpimbor1lem2  47571  quantgodel  47646  nthrucw  47665  goldratmolem2  47681  lambert0  47682  lamberte  47683  cjnpoly  47684  tannpoly  47685  sinnpoly  47686  aistia  47692  aisfina  47693  aiffnbandciffatnotciffb  47699  axorbciffatcxorb  47700  abnotbtaxb  47710  abnotataxb  47711  eusnsn  47821  aiotaval  47890  aiota0ndef  47892  fundcmpsurinjimaid  48218  ichv  48256  ichf  48257  ichid  48258  icht  48259  ichcircshi  48261  icheq  48269  spr0nelg  48283  m3prm  48402  m7prm  48410  0noddALTV  48512  2noddALTV  48516  341fppr2  48557  9fppr8  48560  nfermltl8rev  48565  nfermltl2rev  48566  nfermltlrev  48567  sbgoldbo  48610  nnsum3primes4  48611  evengpop3  48621  stgr1  48784  usgrexmpl1lem  48844  usgrexmpl1  48845  usgrexmpl1tri  48848  usgrexmpl2lem  48849  usgrexmpl2  48850  usgrexmpl2nb0  48854  usgrexmpl2nb1  48855  usgrexmpl2nb2  48856  usgrexmpl2nb3  48857  usgrexmpl2nb4  48858  usgrexmpl2nb5  48859  gpgedg2ov  48889  gpgedg2iv  48890  gpg5nbgrvtx03starlem1  48891  gpg5nbgrvtx03starlem2  48892  gpg5nbgrvtx03starlem3  48893  gpg5nbgrvtx13starlem1  48894  gpg5nbgrvtx13starlem2  48895  gpg5nbgrvtx13starlem3  48896  gpg5grlim  48916  gpg5grlic  48917  gpgprismgr4cycllem2  48919  gpgprismgr4cycllem7  48924  pg4cyclnex  48950  gpg5edgnedg  48953  grlimedgnedg  48954  oddinmgm  48997  nn0mnd  49001  2zrngamgm  49067  2zrngaabl  49072  2zrngmmgm  49074  2zrngnring  49080  fldhmsubcALTV  49155  eliunxp2  49171  zlmodzxzldeplem  49335  zlmodzxzldep  49341  ldepslinc  49346  rrx2xpreen  49556  rrx2plordisom  49560  line2ylem  49588  line2  49589  line2x  49591  inlinecirc02plem  49623  mosn  49648  mof0  49673  mof0ALT  49675  tposrescnv  49714  tposres3  49716  tposideq2  49724  f1omoOLD  49729  nelsubc3  49906  reldmxpc  50081  reldmprcof1  50216  setc1onsubc  50437  reldmlmd2  50488  reldmcmd2  50489  rellmd  50494  relcmd  50495  ex-gte  50564  empty-surprise  50617  eximp-surprise2  50620  amgmw2d  50709