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  1914  ax5e  1947  ax6ev  2004  sbt  2105  equsb1v  2144  ax13  2407  ax13ALT  2457  moanmo  2650  axi12  2733  axbnd  2734  axexte  2736  axextmo  2739  nulmo  2740  vexw  2747  eqeltri  2860  nfcxfr  2924  neir  2962  neirr  2968  eqnetri  3029  nelir  3068  mprgbir  3087  issetri  3473  moeq  3668  rmoeq  3699  cdeqi  3726  eqsstri  3959  vn0OLD  4295  rmo0  4313  ab0orv  4335  rab0  4338  rabnc  4344  pwv  4578  reuprg  4665  tpid1  4731  tpid2  4733  mosneq  4802  uni0OLD  4902  int0  4927  eqbrtri  5132  tr0  5231  trv  5232  zfrep4  5252  axnulALT  5264  0ex  5267  inex1  5284  elpwi2  5304  0elpw  5324  axpow2  5336  dvdemo1  5342  vpwex  5346  zfpair2  5399  prex  5403  exss  5438  brv  5448  opwo0id  5476  moop2  5481  0sn0ep  5562  po0  5583  epse  5640  relxp  5676  rel0  5785  relopabiv  5807  relopabi  5809  relopabiOLD  5810  relopabiALT  5811  eliunxp  5824  opeliunxp2  5825  dmi  5915  dmep  5917  relres  6012  xpidtr  6134  xpima  6192  imadifssrn  6220  dmsn0  6229  cnvsn0  6230  0elon  6444  funmpt  6606  funmpt2  6607  funcnv0  6636  isarep2  6659  fresaunres2  6784  f0  6793  f10d  6890  f1o00  6891  f1oi  6894  f1oiOLD  6895  f1osn  6897  brprcneu  6906  brprcneuALT  6907  opabiotafun  6996  fvopab3ig  7020  opabex  7257  eufnfv  7266  isof1oopb  7364  ncanth  7406  mpofun  7575  reldmmpo  7584  ovid  7593  ovidig  7594  ovidi  7595  ovig  7598  ov3  7615  caovmo  7690  relmptopab  7703  funmpt3  7719  mpt3fvd  7720  porpss  7775  uniex2  7786  uniex2OLD  7787  tfinds2  7909  finds  7942  finds2  7944  oprabex  8022  oprabex3  8023  f1stres  8059  f2ndres  8060  relmpoopab  8141  fsplitfpar  8166  poseq  8212  opeliunxp2f  8265  tpos0  8311  issmo  8394  tfrlem6OLD  8428  tfrlem8  8430  tfrlem16  8439  tfr1a  8440  tfr1  8443  tz7.44lem1  8451  seqomlem2  8499  seqomlem3  8500  seqomlem4  8501  fnseqom  8503  ord3  8530  0lt1o  8550  0we1  8552  naddf  8729  eqer  8792  ecopover  8880  mapsnf1o3  8961  ssdomg  9065  en0  9083  en0r  9085  ensn1  9086  0fi  9108  enrefnn  9112  xpcomf1o  9123  map2xp  9204  limensuci  9210  1sdom2  9277  sdom1  9279  unblem4  9325  fidomdm  9361  marypha1lem  9462  hartogslem1  9573  hartogs  9575  card2on  9585  nelaneqOLDOLD  9635  epinid0  9636  ruALT  9640  disjcsn  9641  elnanel  9645  cnvepnep  9646  inf2  9661  inf3lem6  9671  infeq5i  9674  zfinf2  9680  cantnflt  9710  cnfcom  9738  trcl  9766  tz9.1c  9768  tc2  9778  r1funlimOLD  9807  r1fun  9808  r1dmlim  9809  r1fnon  9810  0hf  9954  karden  9996  kardenOLD  9997  tskwe  10068  cardprclem  10097  pm54.43  10121  r0weon  10130  iunmapdisj  10141  alephfnon  10183  alephfplem4  10225  alephfp  10226  alephval3  10228  kmlem2  10269  dju1dif  10290  ackbij1  10354  ackbij2lem2  10356  ackbij2  10359  infpssrlem3  10422  hsmexlem4  10546  hsmexlem5  10547  ac2  10578  axac3  10581  ac6  10597  axdclem2  10637  dmct  10641  dmctOLD  10642  ondomon  10686  alephsucpw  10694  pwcfsdom  10707  cfpwsdom  10708  smobeth  10710  axpowndlem3  10723  zfcndun  10739  zfcndpow  10740  zfcndinf  10742  zfcndac  10743  wunex2  10862  uniwun  10864  wuncval2  10871  grur1  10944  axgroth5  10948  axgroth2  10949  axgroth6  10952  axgroth3  10955  grothtsk  10959  inaprc  10960  ltsopi  11012  dmaddpi  11014  dmmulpi  11015  1lt2pi  11029  nqerf  11054  addnqf  11072  mulnqf  11073  1lt2nq  11097  m1p1sr  11216  m1m1sr  11217  0lt1sr  11219  axaddf  11269  axmulf  11270  ax1cn  11273  subaddrii  11686  ixi  11985  recgt0ii  12263  nn1suc  12397  4div2e2  12554  arch  12643  un0mulcl  12680  pnf0xnn0  12726  3halfnz  12818  nummac  12904  indstr  13083  mnfltpnf  13295  ioof  13618  0nelfz1  13716  fzp1disj  13757  fzp1nel  13785  fzof  13830  f1resfz0f1d  13967  fvf1tp  13969  om2uzrani  14135  om2uzf1oi  14136  uzrdglem  14140  uzrdgfni  14141  uzrdg0i  14142  ltwenn  14145  hashgf1o  14154  axdc4uzlem  14166  sq0  14375  irec  14385  facmapnn  14470  hashkf  14517  hashfxnn0  14522  hashf  14523  hash0  14552  prhash2ex  14584  hashsslei  14612  hashxplem  14619  hashbclem  14638  hashf1lem1  14641  tpf1ofv0  14682  tpfo  14686  s1dm  14796  eqs1  14802  ccat2s1p1  14819  cats1un  14912  revs1  14956  0csh0  14986  cshw1  15015  cats1fvn  15051  funcnvs1  15106  pfx2  15141  relexp0g  15218  relexpsucnnr  15221  rtrclreclem1  15253  dfrtrclrec2  15254  rtrclreclem2  15255  rtrclreclem4  15257  dfrtrcl2  15258  climmo  15768  fsumcom2  15984  ackbijnn  16041  incexclem  16049  infcvgaux1i  16070  fprodcom2  16195  bpolylem  16258  bpoly3  16268  bpoly4  16269  efcvgfsum  16296  cos1bnd  16399  cos2bnd  16400  znnen  16424  qnnen  16425  aleph1re  16457  3dvds  16545  n2dvdsm1  16583  divalglem5  16611  flodddiv4  16629  sadcaddlem  16671  sadadd2lem  16673  sadadd3  16675  sadaddlem  16680  lcmf0  16853  lcmfunsnlem2lem1  16857  lcmfunsnlem2  16859  coprmprod  16880  coprmproddvdslem  16881  2prm  16911  3lcm2e6  16952  phicl2  16989  pockthi  17129  unbenlem  17130  prmrec  17144  vdwlem13  17215  vdwnn  17220  ramcl2  17238  prmgapprmo  17284  mod2xnegi  17293  modsubi  17294  structcnvcnv  17375  strleun  17379  setsres  17400  strfv  17425  starvndxnbasendx  17521  starvndxnplusgndx  17522  starvndxnmulrndx  17523  scandxnbasendx  17533  scandxnplusgndx  17534  scandxnmulrndx  17535  vscandxnbasendx  17538  vscandxnplusgndx  17539  vscandxnmulrndx  17540  vscandxnscandx  17541  ipndxnbasendx  17549  ipndxnplusgndx  17550  ipndxnmulrndx  17551  slotsdifipndx  17552  tsetndxnplusgndx  17574  tsetndxnmulrndx  17575  tsetndxnstarvndx  17576  slotstnscsi  17577  plendxnplusgndx  17588  plendxnmulrndx  17589  plendxnscandx  17590  plendxnvscandx  17591  slotsdifplendx  17592  basendxnocndx  17600  plendxnocndx  17601  dsndxnplusgndx  17607  dsndxnmulrndx  17608  slotsdnscsi  17609  dsndxntsetndx  17610  slotsdifdsndx  17611  unifndxntsetndx  17617  slotsdifunifndx  17618  slotsdifplendx2  17637  slotsdifocndx  17638  0rest  17650  firest  17653  restid  17654  prdsval  17676  prdsbas  17678  prdsplusg  17679  prdsmulr  17680  prdsvsca  17681  imasaddfnlem  17750  imasvscafn  17759  2oppchomf  17948  0ssc  18062  0subcat  18063  idfucl  18106  homarel  18261  dmaf  18274  cdaf  18275  setc2ohom  18320  catcfuccl  18343  relxpchom  18405  catcxpccl  18431  oppchofcl  18484  oyoncl  18494  letsr  18817  nulchn  18843  s1chn  18844  chnub  18846  chninf  18859  ex-chn1  18861  mgmidmo  18888  efmndmgm  19131  smndex1ibas  19146  smndex1mgm  19156  smndex1mnd  19159  smndex2dbas  19163  smndex2dnrinv  19164  smndex2hbas  19165  degenmgm  19187  degenmgm2nfun  19189  degenmgm2  19190  pwmnd  19193  releqg  19435  ga0  19563  psgnunilem3  19761  psgnunilem4  19762  pmtrsn  19784  efgval  19982  efger  19983  efgsval2  19998  efgsp1  20002  efgsfo  20004  efgredleme  20008  efgredlem  20012  efgred  20013  cygctb  20157  gsum2d2lem  20238  gsum2d2  20239  gsumcom2  20240  dprd2d2  20311  pgpfaclem1  20348  gsumle  20410  reldvdsr  20641  fldhmsubc  21093  00lsp  21307  cnfldfun  21744  cnfldfunALT  21745  xrsmgm  21765  pzriprnglem8  21849  pzriprnglem13  21854  pzriprnglem14  21855  pzriprngALT  21856  resubdrg  21969  ocv0  22038  cssval  22043  islinds2  22174  psrvscafval  22311  psrbag0  22426  psdmvr  22545  00ply1bas  22612  ply1plusgfvi  22614  m2detleib  23001  matunitlindf  23051  tgdom  23351  tgidm  23353  indistps2ALT  23387  restbas  23531  resttopon  23534  rest0  23542  leordtval2  23585  iocpnfordt  23588  icomnfordt  23589  iooordt  23590  ist1-3  23722  1stcfb  23818  comppfsc  23906  1stckgen  23928  ptbasfi  23955  dfac14  23992  opnfbas  24216  hauspwpwf1  24361  alexsubALT  24425  ptcmplem5  24430  cnextrel  24437  ust0  24594  0met  24740  prdsdsf  24741  prdsxmetlem  24742  prdsmet  24744  prdsbl  24865  qtopbaslem  25132  xrtgioo  25181  xrsdsre  25185  zcld  25188  recld2  25189  reperflem  25193  retopconn  25204  iccpnfcnv  25320  bndth  25334  nmoleub2lem2  25492  zclmncvs  25524  recmet  25699  resscdrg  25734  ishl2  25746  recms  25756  volf  25905  iundisj2  25925  volsup  25932  icombl  25940  ioombl  25941  ismbf3d  26030  0plef  26048  0pledm  26049  itg1ge0  26062  mbfi1fseqlem5  26095  itg2addlem  26134  reldv  26245  limciun  26269  dvexp  26328  dveflem  26354  lhop1lem  26388  lhop  26391  elply2  26569  elplyd  26575  ply1term  26577  ply0  26581  plymullem  26590  plymul02  26656  qaa  26704  pserulm  26806  pserdvlem2  26812  efcn  26827  sincosq1lem  26883  tangtx  26891  sincos4thpi  26899  pigt3  26903  pige3ALT  26905  efif1olem4  26930  logf1o  26949  relogf1o  26951  log1  26970  loge  26971  logi  26972  relogiso  26983  dvrelog  27022  relogcn  27023  logcn  27032  cxpcn3  27133  resqrtcn  27134  rtprmirr  27145  2logb9irr  27180  leibpi  27327  log2ublem1  27331  birthday  27339  emcllem5  27384  harmonicbnd  27388  harmonicbnd2  27389  harmonicbnd3  27392  lgamgulm2  27420  lgamcvglem  27424  gamf  27427  ppiltx  27561  ppiublem1  27586  ppiub  27588  bclbnd  27664  bpos1lem  27666  bposlem8  27675  lgsquadlem2  27765  2sqlem9  27811  2sqlem10  27812  addsqnreup  27827  chebbnd1  27856  selberg2lem  27934  pntrsumo1  27949  selbergsb  27959  pntpbnd  27972  ltsval2  28070  noxp1o  28077  nosepnelem  28093  noetasuplem2  28148  noetainflem2  28152  0lt1s  28255  addsf  28425  precsexlem1  28650  precsexlem2  28651  precsexlem3  28652  precsexlem4  28653  precsexlem5  28654  precsexlem9  28658  precsexlem10  28659  precsexlem11  28660  elons2  28701  oncutlt  28707  oniso  28714  onswe  28715  onsse  28716  onaddscl  28720  onmulscl  28721  onsbnd  28724  eln0s  28804  0zs  28831  zseo  28865  twocut  28866  0reno  28939  1reno  28940  lngndxnitvndx  28962  istrkg2ld  28979  tgcgr4  29051  ax5seglem7  29570  axlowdimlem4  29580  axlowdimlem6  29582  axlowdimlem7  29583  axlowdimlem10  29586  axlowdimlem13  29589  axlowdimlem16  29592  uhgr0e  29706  uhgr0  29708  upgrbi  29728  umgrbi  29736  usgr0  29881  lfuhgr1v0e  29892  usgrexmpllem  29898  usgrexmpl  29901  griedg0prc  29902  cplgr0  30063  usgrexilem  30078  cffldtocusgr  30085  rgrusgrprc  30227  rusgrprc  30228  rgrprcx  30230  rgrx0ndm  30231  usgr2pthlem  30406  pthdlem2  30411  uspgrn2crct  30454  wwlksnext  30539  clwwlknondisj  30759  0ewlk  30762  0wlk  30764  0pth  30773  1pthdlem1  30783  1trld  30790  wlk2v2elem2  30814  wlk2v2e  30815  upgr3v3e3cycl  30838  upgr4cycl4dv4e  30843  dfconngr1  30846  0conngr  30850  konigsbergumgr  30909  2wspmdisj  30995  2clwwlk2clwwlk  31008  numclwwlk3lem2lem  31041  numclwwlk3lem2  31042  ex-dif  31081  ex-in  31083  ex-eprel  31091  ex-id  31092  ex-fl  31105  ex-mod  31107  ex-hash  31111  ex-fpar  31120  avril1  31121  2bornot2b  31122  0vfval  31265  vsfval  31292  ajmoi  31517  ajfuni  31518  normlem2  31770  norm3adifii  31807  hhip  31836  hlim0  31894  hlimcaui  31895  hlimf  31896  hhssnv  31923  shscli  31976  shsval2i  32046  h1de2i  32212  fh3i  32282  fh4i  32283  cm2mi  32285  qlaxr3i  32295  mayetes3i  32388  ho0f  32410  hoif  32413  hodidi  32446  ho0subi  32454  hosd1i  32481  adjmo  32491  nmopsetn0  32524  nmfnsetn0  32537  funadj  32545  funcnvadj  32552  nmcexi  32685  cnlnadjlem8  32733  nmoptri2i  32758  opsqrlem4  32802  hmopidmchi  32810  pjoci  32839  pjinvari  32850  abrexdomjm  33202  elim2ifim  33239  iundisj2f  33282  rinvf1o  33322  dfcnv2  33366  snct  33402  fzodif2  33479  iundisj2fi  33485  dp2lt10  33546  dp2ltc  33549  dplti  33567  dpgti  33568  dpexpp1  33570  ltwenn0  33635  xrge0slmod  34013  isconstr  34479  zarcls  34617  zartopn  34618  xrge0pluscn  34683  qqhre  34763  esumrnmpt2  34811  esumfsup  34813  esumpcvgval  34821  hasheuni  34828  esumcvg  34829  esumcvgsum  34831  esumsup  34832  esum2d  34836  dmsigagen  34888  ldgenpisyslem3  34909  measvuni  34958  voliune  34973  volfiniune  34974  br2base  35012  dya2iocuni  35026  eulerpartlem1  35110  eulerpartlemt  35114  eulerpartgbij  35115  fib0  35142  coinfliprv  35226  ballotlem2  35232  ballotlemic  35250  ballotlem7  35279  ballotth  35281  rpsqrtcn  35333  chtvalz  35369  circlemethnat  35381  circlevma  35382  circlemethhgt  35383  hgt750lem  35391  bnj226  35476  bnj1101  35526  bnj110  35599  bnj149  35616  bnj150  35617  bnj151  35618  bnj517  35626  bnj580  35654  bnj865  35664  bnj900  35670  bnj996  35697  bnj1110  35723  bnj1133  35730  bnj1128  35731  bnj1145  35734  bnj1137  35736  bnj1171  35741  bnj1176  35746  axnulALT2  35825  rankse  35864  fineqvnttrclse  35933  setinds2regs  35940  tz9.1regs  35943  j0iso  36045  k39o  36058  j0le  36060  k3n0j0lt  36061  onprcf1acwevdlem2  36087  vsmext  36130  subfacp1lem5  36157  subfacp1lem6  36158  kur14lem9  36187  cvmcov2  36248  cvmliftlem1  36258  cvmliftlem4  36261  cvmliftlem5  36262  gonanegoal  36325  satfv0  36331  satfv0fun  36344  fmlan0  36364  gonan0  36365  fmla0disjsuc  36371  ex-sategoelel12  36400  msrfo  36519  problem5  36642  brtpid1  36701  brtpid2  36702  brtpid3  36703  faclimlem1  36723  axextndbi  36781  txprel  36856  relsset  36865  relbigcup  36874  fvbigcup  36879  fnsingle  36896  fvsingle  36897  snelsingles  36899  funimage  36905  fullfunfnv  36925  imagesset  36932  funtransport  37011  colinrel  37037  funray  37120  funline  37122  nmulr0  37159  neibastop2lem  37363  filnetlem3  37383  nrmo  37413  waj-ax  37417  lukshef-ax2  37418  arg-ax  37419  limsucncmpi  37448  ttctr  37496  dfttc2g  37509  ttcuniun  37513  ttcuni  37516  dfttc4lem2  37532  regsfromregtco  37541  dnizeq0  37556  knoppcnlem8  37581  knoppcnlem11  37584  cnndvlem1  37618  bj-babylob  37689  bj-ax12ssb  37772  bj-nnfnth  37868  bj-snsetex  38091  bj-0eltag  38106  bj-2upln0  38151  bj-2upln1upl  38152  bj-snexg  38162  bj-unexg  38166  bj-adjg1  38171  bj-axseprep  38260  f1omptsnlem  38527  f1omptsn  38528  icoreresf  38543  relowlssretop  38554  relowlpssretop  38555  domalom  38595  poimirlem3  38809  poimirlem9  38815  poimirlem16  38822  poimirlem17  38823  poimirlem18  38824  poimirlem19  38825  poimirlem20  38826  poimirlem26  38832  mblfinlem1  38843  mblfinlem2  38844  ismblfin  38847  voliunnfl  38850  cnambfre  38854  abrexdom  38932  fdc  38945  cncfres  38965  heibor1lem  39009  grposnOLD  39082  bicontr  39280  an12i  39296  tsim1  39328  ac6s6f  39371  vvdifopab  39463  brcnvrabga  39540  opabf  39574  xrnrel  39580  relqmap  39650  dmsucmap  39666  mopre  39669  relcoels  39712  cnvcosseq  39725  refrelcoss3  39751  refrelcoss2  39752  symrelcoss2  39754  refrelcoss  39801  symrelcoss  39842  n0eldmqs  39930  ax13fromc9  40229  dedths  40285  renegclALT  40286  12gcd5e1  43319  60gcd7e1  43321  lcmineqlem23  43367  dvrelog2  43380  dvrelog3  43381  dvrelog2b  43382  aks4d1p1p6  43389  aks4d1p1p7  43390  aks4d1p1  43392  sticksstones22  43484  25or6to4  43522  sn-axprlem3  43539  acos1half  43675  omexcn  43967  moxfr  43969  mapfzcons1  43994  diophrw  44036  0dioph  44055  vdioph  44056  rabren3dioph  44088  2nn0ind  44218  rpnnen3  44305  kelac2lem  44332  frlmpwfi  44366  oaordnrex  44558  omnord1ex  44567  oenord1ex  44578  oaomoencom  44580  ifpbiidcor2  44745  iscard4  44795  sqrtcval  44902  resqrtvalex  44906  eliunov2  44940  xphe  45042  0he  45043  he0  45045  snhesn  45047  idhe  45048  frege54cor1c  45176  clsk1independent  45307  neicvgnvor  45377  amgm2d  45459  amgm3d  45460  amgm4d  45461  ismnushort  45546  lhe4.4ex1a  45574  rusbcALT  45682  ipo0  45692  ifr0  45693  vk15.4j  45771  2sb5nd  45803  dfvd1ir  45816  dfvd2anir  45827  dfvd2ir  45829  dfvd3ir  45836  dfvd3anir  45839  iden2  45857  e0bir  46019  uun2221p1  46056  uun2221p2  46057  2sb5ndVD  46152  2sb5ndALT  46174  iunconnlem2  46177  trwf  46213  wfaxext  46247  wfaxpow  46251  wfaxinf2  46255  wfac8prim  46256  permaxinf2lem  46266  nregmodelf1o  46269  fnchoice  46320  unisn0  46345  eliincex  46398  icof  46505  fnmptif  46550  supminfxr  46747  rexanuz2nf  46775  fsumiunss  46860  climlimsupcex  47052  liminfltlimsupex  47064  liminflelimsupcex  47080  xlimrel  47103  xlimfun  47138  resincncf  47158  dvnprodlem3  47231  volioc  47255  volico  47266  dmvolss  47268  volioof  47270  stoweidlem13  47296  stoweidlem34  47317  stirlinglem5  47361  stirlinglem13  47369  stirlingr  47373  fourierdlem42  47432  fourierdlem62  47451  fouriersw  47514  etransc  47566  salexct  47617  salexct2  47622  salgencntex  47626  sge0rnn0  47651  gsumge0cl  47654  sge00  47659  sge0resplit  47689  sge0reuz  47730  omeiunle  47800  0ome  47812  icoresmbl  47826  ovn0lem  47848  ovnhoilem1  47884  hspmbl  47912  nsssmfmbf  48062  mbfpsssmf  48066  smfresal  48071  smfmullem4  48077  smfpimbor1lem1  48081  smfpimbor1lem2  48082  quantgodel  48157  numtowerdt  48189  goldratmolem2  48206  goldratmolem3  48207  goldratval  48209  lambert0  48210  lamberte  48211  cjnpoly  48212  aistia  48240  aisfina  48241  aiffnbandciffatnotciffb  48247  axorbciffatcxorb  48248  abnotbtaxb  48258  abnotataxb  48259  eusnsn  48369  aiotaval  48438  aiota0ndef  48440  fundcmpsurinjimaid  48766  ichv  48804  ichf  48805  ichid  48806  icht  48807  ichcircshi  48809  icheq  48817  spr0nelg  48831  m3prm  48950  m7prm  48958  0noddALTV  49060  2noddALTV  49064  341fppr2  49105  9fppr8  49108  nfermltl8rev  49113  nfermltl2rev  49114  nfermltlrev  49115  sbgoldbo  49158  nnsum3primes4  49159  evengpop3  49169  stgr1  49332  usgrexmpl1lem  49392  usgrexmpl1  49393  usgrexmpl1tri  49396  usgrexmpl2lem  49397  usgrexmpl2  49398  usgrexmpl2nb0  49402  usgrexmpl2nb1  49403  usgrexmpl2nb2  49404  usgrexmpl2nb3  49405  usgrexmpl2nb4  49406  usgrexmpl2nb5  49407  gpgedg2ov  49437  gpgedg2iv  49438  gpg5nbgrvtx03starlem1  49439  gpg5nbgrvtx03starlem2  49440  gpg5nbgrvtx03starlem3  49441  gpg5nbgrvtx13starlem1  49442  gpg5nbgrvtx13starlem2  49443  gpg5nbgrvtx13starlem3  49444  gpg5grlim  49464  gpg5grlic  49465  gpgprismgr4cycllem2  49467  gpgprismgr4cycllem7  49472  pg4cyclnex  49498  gpg5edgnedg  49501  grlimedgnedg  49502  oddinmgm  49545  nn0mnd  49549  2zrngamgm  49615  2zrngaabl  49620  2zrngmmgm  49622  2zrngnring  49628  fldhmsubcALTV  49703  eliunxp2  49777  zlmodzxzldeplem  49941  zlmodzxzldep  49947  ldepslinc  49952  rrx2xpreen  50163  rrx2plordisom  50167  line2ylem  50194  line2  50195  mosn  50255  mof0  50280  mof0ALT  50282  tposrescnv  50323  tposres3  50325  tposideq2  50333  f1omoOLD  50339  nelsubc3  50516  reldmxpc  50699  fucoisfunc  50818  fucoisfunc2lem1  50819  reldmprcof1  50847  setc1onsubc  51071  reldmlmd2  51167  reldmcmd2  51168  rellmd  51173  relcmd  51174  ex-gte  51228  dvsec  51284  dvcsc  51285  dvcot  51286  empty-surprise  51306  eximp-surprise2  51309  amgmw2d  51417