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  855  orri  862  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  equsb1v  2106  ax13  2373  ax13ALT  2423  moanmo  2615  axi12  2699  axbnd  2700  axexte  2702  axextmo  2705  nulmo  2706  vexw  2713  eqeltri  2824  nfcxfr  2889  neir  2928  neirr  2934  eqnetri  2995  nelir  3032  mprgbir  3051  cbvrexdva2OLD  3314  issetri  3457  moeq  3669  rmoeq  3700  cdeqi  3727  eqsstri  3984  rmo0  4315  rabnc  4344  reuprg  4657  tpid1  4722  tpid2  4724  mosneq  4796  pwv  4858  uni0  4889  int0  4915  eqbrtri  5116  tr0  5214  trv  5215  zfrep4  5235  axnulALT  5246  0ex  5249  inex1  5259  elpwi2  5277  0elpw  5298  axpow2  5309  dvdemo1  5315  vpwex  5319  zfpair2  5375  exss  5410  brv  5419  opwo0id  5444  moop2  5449  0sn0ep  5527  po0  5548  epse  5605  relxp  5641  rel0  5746  relopabiv  5767  relopabi  5769  relopabiALT  5770  eliunxp  5784  opeliunxp2  5785  dmi  5868  dmep  5870  xpidtr  6075  xpima  6135  dmsn0  6162  cnvsn0  6163  0elon  6366  funmpt  6524  funmpt2  6525  funcnv0  6552  isarep2  6576  fresaunres2  6700  f0  6709  f10d  6802  f1o00  6803  f1oi  6806  f1osn  6808  brprcneu  6816  brprcneuALT  6817  opabiotafun  6907  fvopab3ig  6930  opabex  7160  eufnfv  7169  isof1oopb  7266  ncanth  7308  mpofun  7477  reldmmpo  7487  ovid  7494  ovidig  7495  ovidi  7496  ovig  7499  ov3  7516  caovmo  7590  relmptopab  7603  porpss  7667  uniex2  7678  tfinds2  7804  finds  7836  finds2  7838  oprabex  7918  oprabex3  7919  f1stres  7955  f2ndres  7956  relmpoopab  8034  fsplitfpar  8058  poseq  8098  opeliunxp2f  8150  tpos0  8196  issmo  8278  tfrlem6  8311  tfrlem8  8313  tfrlem16  8322  tfr1a  8323  tfr1  8326  tz7.44lem1  8334  seqomlem2  8380  seqomlem3  8381  seqomlem4  8382  fnseqom  8384  ord3  8410  0lt1o  8429  0we1  8431  naddf  8606  eqer  8668  ecopover  8755  mapsnf1o3  8829  ssdomg  8932  en0  8950  en0r  8952  ensn1  8953  0fi  8974  snfiOLD  8976  enrefnn  8979  xpcomf1o  8990  map2xp  9071  limensuci  9077  1sdom2  9147  sdom1  9149  unblem4  9200  fidomdm  9243  marypha1lem  9342  hartogslem1  9453  hartogs  9455  card2on  9465  nelaneqOLD  9513  epinid0  9514  ruALT  9517  disjcsn  9518  elnanel  9522  cnvepnep  9523  inf2  9538  inf3lem6  9548  infeq5i  9551  zfinf2  9557  cantnflt  9587  cnfcom  9615  trcl  9643  tz9.1c  9645  tc2  9657  r1funlim  9681  r1fnon  9682  karden  9810  tskwe  9865  cardprclem  9894  pm54.43  9916  r0weon  9925  iunmapdisj  9936  alephfnon  9978  alephfplem4  10020  alephfp  10021  alephval3  10023  kmlem2  10065  dju1dif  10086  ackbij1  10150  ackbij2lem2  10152  ackbij2  10155  infpssrlem3  10218  hsmexlem4  10342  hsmexlem5  10343  ac2  10374  axac3  10377  ac6  10393  axdclem2  10433  dmct  10437  ondomon  10476  alephsucpw  10483  pwcfsdom  10496  cfpwsdom  10497  smobeth  10499  axpowndlem3  10512  zfcndun  10528  zfcndpow  10529  zfcndinf  10531  zfcndac  10532  wunex2  10651  uniwun  10653  wuncval2  10660  grur1  10733  axgroth5  10737  axgroth2  10738  axgroth6  10741  axgroth3  10744  grothtsk  10748  inaprc  10749  ltsopi  10801  dmaddpi  10803  dmmulpi  10804  1lt2pi  10818  nqerf  10843  addnqf  10861  mulnqf  10862  1lt2nq  10886  m1p1sr  11005  m1m1sr  11006  0lt1sr  11008  axaddf  11058  axmulf  11059  ax1cn  11062  subaddrii  11471  ixi  11767  recgt0ii  12049  nn1suc  12168  4d2e2  12311  arch  12399  un0mulcl  12436  pnf0xnn0  12482  3halfnz  12573  nummac  12654  indstr  12835  mnfltpnf  13046  ioof  13368  0nelfz1  13464  fzp1disj  13504  fzp1nel  13532  fzof  13577  fvf1tp  13711  om2uzrani  13877  om2uzf1oi  13878  uzrdglem  13882  uzrdgfni  13883  uzrdg0i  13884  ltwenn  13887  hashgf1o  13896  axdc4uzlem  13908  sq0  14117  irec  14126  facmapnn  14210  hashkf  14257  hashfxnn0  14262  hashf  14263  hash0  14292  prhash2ex  14324  hashsslei  14351  hashxplem  14358  hashbclem  14377  hashf1lem1  14380  tpf1ofv0  14421  tpfo  14425  s1dm  14533  eqs1  14537  ccat2s1p1  14554  cats1un  14645  revs1  14689  0csh0  14717  cshw1  14746  cats1fvn  14783  funcnvs1  14837  pfx2  14872  relexp0g  14947  relexpsucnnr  14950  rtrclreclem1  14982  dfrtrclrec2  14983  rtrclreclem2  14984  rtrclreclem4  14986  dfrtrcl2  14987  climmo  15482  fsumcom2  15699  ackbijnn  15753  incexclem  15761  infcvgaux1i  15782  fprodcom2  15909  bpolylem  15973  bpoly3  15983  bpoly4  15984  efcvgfsum  16011  cos1bnd  16114  cos2bnd  16115  znnen  16139  qnnen  16140  aleph1re  16172  3dvds  16260  n2dvdsm1  16298  divalglem5  16326  flodddiv4  16344  sadcaddlem  16386  sadadd2lem  16388  sadadd3  16390  sadaddlem  16395  lcmf0  16563  lcmfunsnlem2lem1  16567  lcmfunsnlem2  16569  coprmprod  16590  coprmproddvdslem  16591  2prm  16621  3lcm2e6  16661  phicl2  16697  pockthi  16837  unbenlem  16838  prmrec  16852  vdwlem13  16923  vdwnn  16928  ramcl2  16946  prmgapprmo  16992  mod2xnegi  17001  modsubi  17002  structcnvcnv  17082  strleun  17086  setsres  17107  strfv  17132  starvndxnbasendx  17226  starvndxnplusgndx  17227  starvndxnmulrndx  17228  scandxnbasendx  17238  scandxnplusgndx  17239  scandxnmulrndx  17240  vscandxnbasendx  17243  vscandxnplusgndx  17244  vscandxnmulrndx  17245  vscandxnscandx  17246  ipndxnbasendx  17254  ipndxnplusgndx  17255  ipndxnmulrndx  17256  slotsdifipndx  17257  tsetndxnplusgndx  17279  tsetndxnmulrndx  17280  tsetndxnstarvndx  17281  slotstnscsi  17282  plendxnplusgndx  17293  plendxnmulrndx  17294  plendxnscandx  17295  plendxnvscandx  17296  slotsdifplendx  17297  basendxnocndx  17305  plendxnocndx  17306  dsndxnplusgndx  17312  dsndxnmulrndx  17313  slotsdnscsi  17314  dsndxntsetndx  17315  slotsdifdsndx  17316  unifndxntsetndx  17322  slotsdifunifndx  17323  slotsdifplendx2  17338  slotsdifocndx  17339  0rest  17351  firest  17354  restid  17355  prdsval  17377  prdsbas  17379  prdsplusg  17380  prdsmulr  17381  prdsvsca  17382  imasaddfnlem  17450  imasvscafn  17459  2oppchomf  17648  0ssc  17762  0subcat  17763  idfucl  17806  homarel  17961  dmaf  17974  cdaf  17975  setc2ohom  18020  catcfuccl  18043  relxpchom  18105  catcxpccl  18131  oppchofcl  18184  oyoncl  18194  letsr  18517  mgmidmo  18552  efmndmgm  18777  smndex1ibas  18792  smndex1mgm  18799  smndex1mnd  18802  smndex2dbas  18806  smndex2dnrinv  18807  smndex2hbas  18808  pwmnd  18829  releqg  19072  ga0  19195  psgnunilem3  19393  psgnunilem4  19394  pmtrsn  19416  efgval  19614  efger  19615  efgsval2  19630  efgsp1  19634  efgsfo  19636  efgredleme  19640  efgredlem  19644  efgred  19645  cygctb  19789  gsum2d2lem  19870  gsum2d2  19871  gsumcom2  19872  dprd2d2  19943  pgpfaclem1  19980  gsumle  20042  reldvdsr  20263  fldhmsubc  20688  00lsp  20902  cnfldfun  21293  cnfldfunALT  21294  cnfldfunOLD  21306  cnfldfunALTOLD  21307  xrsmgm  21331  pzriprnglem8  21413  pzriprnglem13  21418  pzriprnglem14  21419  pzriprngALT  21420  resubdrg  21533  ocv0  21602  cssval  21607  islinds2  21738  psrvscafval  21873  psrbag0  21985  psdmvr  22072  00ply1bas  22140  ply1plusgfvi  22142  m2detleib  22534  tgdom  22881  tgidm  22883  indistps2ALT  22917  restbas  23061  resttopon  23064  rest0  23072  leordtval2  23115  iocpnfordt  23118  icomnfordt  23119  iooordt  23120  ist1-3  23252  1stcfb  23348  comppfsc  23435  1stckgen  23457  ptbasfi  23484  dfac14  23521  opnfbas  23745  hauspwpwf1  23890  alexsubALT  23954  ptcmplem5  23959  cnextrel  23966  ust0  24123  0met  24270  prdsdsf  24271  prdsxmetlem  24272  prdsmet  24274  prdsbl  24395  qtopbaslem  24662  xrtgioo  24711  xrsdsre  24715  zcld  24718  recld2  24719  reperflem  24723  retopconn  24734  iccpnfcnv  24858  bndth  24873  nmoleub2lem2  25032  zclmncvs  25064  recmet  25239  resscdrg  25274  ishl2  25286  recms  25296  volf  25446  iundisj2  25466  volsup  25473  icombl  25481  ioombl  25482  ismbf3d  25571  0plef  25589  0pledm  25590  itg1ge0  25603  mbfi1fseqlem5  25636  itg2addlem  25675  reldv  25787  limciun  25811  dvexp  25873  dveflem  25899  lhop1lem  25934  lhop  25937  elply2  26117  elplyd  26123  ply1term  26125  ply0  26129  plymullem  26137  qaa  26247  pserulm  26347  pserdvlem2  26354  efcn  26369  sincosq1lem  26422  tangtx  26430  sincos4thpi  26438  pigt3  26443  pige3ALT  26445  efif1olem4  26470  logf1o  26489  relogf1o  26491  log1  26510  loge  26511  logi  26512  relogiso  26523  dvrelog  26562  relogcn  26563  logcn  26572  cxpcn3  26674  resqrtcn  26675  rtprmirr  26686  2logb9irr  26721  leibpi  26868  log2ublem1  26872  birthday  26880  emcllem5  26926  harmonicbnd  26930  harmonicbnd2  26931  harmonicbnd3  26934  lgamgulm2  26962  lgamcvglem  26966  gamf  26969  ppiltx  27103  ppiublem1  27129  ppiub  27131  bclbnd  27207  bpos1lem  27209  bposlem8  27218  lgsquadlem2  27308  2sqlem9  27354  2sqlem10  27355  addsqnreup  27370  chebbnd1  27399  selberg2lem  27477  pntrsumo1  27492  selbergsb  27502  pntpbnd  27515  sltval2  27584  noxp1o  27591  nosepnelem  27607  noetasuplem2  27662  noetainflem2  27666  0slt1s  27761  addsf  27912  precsexlem1  28132  precsexlem2  28133  precsexlem3  28134  precsexlem4  28135  precsexlem5  28136  precsexlem9  28140  precsexlem10  28141  precsexlem11  28142  elons2  28182  onscutlt  28188  onsiso  28192  onswe  28193  onsse  28194  onaddscl  28197  onmulscl  28198  eln0s  28274  0zs  28299  zseo  28332  twocut  28333  lngndxnitvndx  28406  istrkg2ld  28423  tgcgr4  28494  ax5seglem7  28898  axlowdimlem4  28908  axlowdimlem6  28910  axlowdimlem7  28911  axlowdimlem10  28914  axlowdimlem13  28917  axlowdimlem16  28920  uhgr0e  29034  uhgr0  29036  upgrbi  29056  umgrbi  29064  usgr0  29206  lfuhgr1v0e  29217  usgrexmpllem  29223  usgrexmpl  29226  griedg0prc  29227  cplgr0  29388  usgrexilem  29403  cffldtocusgr  29410  cffldtocusgrOLD  29411  rgrusgrprc  29553  rusgrprc  29554  rgrprcx  29556  rgrx0ndm  29557  usgr2pthlem  29726  pthdlem2  29731  uspgrn2crct  29771  wwlksnext  29856  clwwlknondisj  30073  0ewlk  30076  0wlk  30078  0pth  30087  1pthdlem1  30097  1trld  30104  wlk2v2elem2  30118  wlk2v2e  30119  upgr3v3e3cycl  30142  upgr4cycl4dv4e  30147  dfconngr1  30150  0conngr  30154  konigsbergumgr  30213  2wspmdisj  30299  2clwwlk2clwwlk  30312  numclwwlk3lem2lem  30345  numclwwlk3lem2  30346  ex-dif  30385  ex-in  30387  ex-eprel  30395  ex-id  30396  ex-fl  30409  ex-mod  30411  ex-hash  30415  ex-fpar  30424  avril1  30425  2bornot2b  30426  0vfval  30568  vsfval  30595  ajmoi  30820  ajfuni  30821  normlem2  31073  norm3adifii  31110  hhip  31139  hlim0  31197  hlimcaui  31198  hlimf  31199  hhssnv  31226  shscli  31279  shsval2i  31349  h1de2i  31515  fh3i  31585  fh4i  31586  cm2mi  31588  qlaxr3i  31598  mayetes3i  31691  ho0f  31713  hoif  31716  hodidi  31749  ho0subi  31757  hosd1i  31784  adjmo  31794  nmopsetn0  31827  nmfnsetn0  31840  funadj  31848  funcnvadj  31855  nmcexi  31988  cnlnadjlem8  32036  nmoptri2i  32061  opsqrlem4  32105  hmopidmchi  32113  pjoci  32142  pjinvari  32153  abrexdomjm  32469  elim2ifim  32507  iundisj2f  32552  rinvf1o  32587  dfcnv2  32633  snct  32670  fzodif2  32747  iundisj2fi  32753  dp2lt10  32837  dp2ltc  32840  dplti  32858  dpgti  32859  dpexpp1  32861  s1chn  32965  chnub  32967  xrge0slmod  33295  isconstr  33702  zarcls  33840  zartopn  33841  xrge0pluscn  33906  qqhre  33986  esumrnmpt2  34034  esumfsup  34036  esumpcvgval  34044  hasheuni  34051  esumcvg  34052  esumcvgsum  34054  esumsup  34055  esum2d  34059  dmsigagen  34110  ldgenpisyslem3  34131  measvuni  34180  voliune  34195  volfiniune  34196  br2base  34236  dya2iocuni  34250  eulerpartlem1  34334  eulerpartlemt  34338  eulerpartgbij  34339  fib0  34366  coinfliprv  34450  ballotlem2  34456  ballotlemic  34474  ballotlem7  34503  ballotth  34505  plymul02  34513  rpsqrtcn  34560  chtvalz  34596  circlemethnat  34608  circlevma  34609  circlemethhgt  34610  hgt750lem  34618  bnj226  34700  bnj1101  34750  bnj110  34824  bnj149  34841  bnj150  34842  bnj151  34843  bnj517  34851  bnj580  34879  bnj865  34889  bnj900  34895  bnj996  34922  bnj1110  34948  bnj1133  34955  bnj1128  34956  bnj1145  34959  bnj1137  34961  bnj1171  34966  bnj1176  34971  setinds2regs  35065  tz9.1regs  35066  f1resfz0f1d  35086  subfacp1lem5  35156  subfacp1lem6  35157  kur14lem9  35186  cvmcov2  35247  cvmliftlem1  35257  cvmliftlem4  35260  cvmliftlem5  35261  gonanegoal  35324  satfv0  35330  satfv0fun  35343  fmlan0  35363  gonan0  35364  fmla0disjsuc  35370  ex-sategoelel12  35399  msrfo  35518  problem5  35641  brtpid1  35693  brtpid2  35694  brtpid3  35695  faclimlem1  35715  axextndbi  35777  txprel  35852  relsset  35861  relbigcup  35870  fvbigcup  35875  fnsingle  35892  fvsingle  35893  snelsingles  35895  funimage  35901  fullfunfnv  35919  imagesset  35926  funtransport  36004  colinrel  36030  funray  36113  funline  36115  0hf  36150  neibastop2lem  36333  filnetlem3  36353  nrmo  36383  waj-ax  36387  lukshef-ax2  36388  arg-ax  36389  limsucncmpi  36418  dnizeq0  36448  knoppcnlem8  36473  knoppcnlem11  36476  cnndvlem1  36510  bj-babylob  36577  bj-ax12ssb  36631  bj-nnfnth  36716  bj-snsetex  36936  bj-0eltag  36951  bj-2upln0  36996  bj-2upln1upl  36997  bj-snexg  37007  bj-unexg  37011  bj-adjg1  37016  f1omptsnlem  37309  f1omptsn  37310  icoreresf  37325  relowlssretop  37336  relowlpssretop  37337  domalom  37377  matunitlindf  37597  poimirlem3  37602  poimirlem9  37608  poimirlem16  37615  poimirlem17  37616  poimirlem18  37617  poimirlem19  37618  poimirlem20  37619  poimirlem26  37625  mblfinlem1  37636  mblfinlem2  37637  ismblfin  37640  voliunnfl  37643  cnambfre  37647  abrexdom  37709  fdc  37724  cncfres  37744  heibor1lem  37788  grposnOLD  37861  bicontr  38059  an12i  38077  tsim1  38109  ac6s6f  38152  vvdifopab  38234  brcnvrabga  38309  opabf  38335  xrnrel  38340  relcoels  38400  cnvcosseq  38413  refrelcoss3  38439  refrelcoss2  38440  symrelcoss2  38442  refrelcoss  38499  symrelcoss  38536  n0eldmqs  38624  ax13fromc9  38884  dedths  38940  renegclALT  38941  12gcd5e1  41976  60gcd7e1  41978  lcmineqlem23  42024  dvrelog2  42037  dvrelog3  42038  dvrelog2b  42039  aks4d1p1p6  42046  aks4d1p1p7  42047  aks4d1p1  42049  sticksstones22  42141  sn-axprlem3  42190  acos1half  42331  moxfr  42665  mapfzcons1  42690  diophrw  42732  0dioph  42751  vdioph  42752  rabren3dioph  42788  2nn0ind  42918  rpnnen3  43005  kelac2lem  43037  frlmpwfi  43071  oaordnrex  43268  omnord1ex  43277  oenord1ex  43288  oaomoencom  43290  ifpbiidcor2  43456  iscard4  43506  sqrtcval  43614  resqrtvalex  43618  eliunov2  43652  xphe  43754  0he  43755  he0  43757  snhesn  43759  idhe  43760  frege54cor1c  43888  clsk1independent  44019  neicvgnvor  44089  amgm2d  44171  amgm3d  44172  amgm4d  44173  ismnushort  44274  lhe4.4ex1a  44302  rusbcALT  44412  ipo0  44422  ifr0  44423  vk15.4j  44502  2sb5nd  44534  dfvd1ir  44547  dfvd2anir  44558  dfvd2ir  44560  dfvd3ir  44567  dfvd3anir  44570  iden2  44588  e0bir  44750  uun2221p1  44787  uun2221p2  44788  2sb5ndVD  44883  2sb5ndALT  44905  iunconnlem2  44908  trwf  44933  wfaxext  44967  wfaxpow  44971  wfaxinf2  44975  wfac8prim  44976  permaxinf2lem  44986  nregmodelf1o  44989  fnchoice  45007  unisn0  45032  eliincex  45088  icof  45197  fnmptif  45243  supminfxr  45444  rexanuz2nf  45472  fsumiunss  45557  climlimsupcex  45751  liminfltlimsupex  45763  liminflelimsupcex  45779  xlimrel  45802  xlimfun  45837  resincncf  45857  dvnprodlem3  45930  volioc  45954  volico  45965  dmvolss  45967  volioof  45969  stoweidlem13  45995  stoweidlem34  46016  stirlinglem5  46060  stirlinglem13  46068  stirlingr  46072  fourierdlem42  46131  fourierdlem62  46150  fouriersw  46213  etransc  46265  salexct  46316  salexct2  46321  salgencntex  46325  sge0rnn0  46350  gsumge0cl  46353  sge00  46358  sge0resplit  46388  sge0reuz  46429  omeiunle  46499  0ome  46511  icoresmbl  46525  ovn0lem  46547  ovnhoilem1  46583  hspmbl  46611  nsssmfmbf  46761  mbfpsssmf  46765  smfresal  46770  smfmullem4  46776  smfpimbor1lem1  46780  smfpimbor1lem2  46781  lambert0  46872  lamberte  46873  cjnpoly  46874  tannpoly  46875  sinnpoly  46876  aistia  46882  aisfina  46883  aiffnbandciffatnotciffb  46889  axorbciffatcxorb  46890  abnotbtaxb  46900  abnotataxb  46901  eusnsn  47011  aiotaval  47080  aiota0ndef  47082  fundcmpsurinjimaid  47396  ichv  47434  ichf  47435  ichid  47436  icht  47437  ichcircshi  47439  icheq  47447  spr0nelg  47461  m3prm  47577  m7prm  47585  0noddALTV  47674  2noddALTV  47678  341fppr2  47719  9fppr8  47722  nfermltl8rev  47727  nfermltl2rev  47728  nfermltlrev  47729  sbgoldbo  47772  nnsum3primes4  47773  evengpop3  47783  stgr1  47946  usgrexmpl1lem  48006  usgrexmpl1  48007  usgrexmpl1tri  48010  usgrexmpl2lem  48011  usgrexmpl2  48012  usgrexmpl2nb0  48016  usgrexmpl2nb1  48017  usgrexmpl2nb2  48018  usgrexmpl2nb3  48019  usgrexmpl2nb4  48020  usgrexmpl2nb5  48021  gpgedg2ov  48051  gpgedg2iv  48052  gpg5nbgrvtx03starlem1  48053  gpg5nbgrvtx03starlem2  48054  gpg5nbgrvtx03starlem3  48055  gpg5nbgrvtx13starlem1  48056  gpg5nbgrvtx13starlem2  48057  gpg5nbgrvtx13starlem3  48058  gpg5grlim  48078  gpg5grlic  48079  gpgprismgr4cycllem2  48081  gpgprismgr4cycllem7  48086  pg4cyclnex  48112  gpg5edgnedg  48115  grlimedgnedg  48116  oddinmgm  48160  nn0mnd  48164  2zrngamgm  48230  2zrngaabl  48235  2zrngmmgm  48237  2zrngnring  48243  fldhmsubcALTV  48318  eliunxp2  48319  zlmodzxzldeplem  48484  zlmodzxzldep  48490  ldepslinc  48495  rrx2xpreen  48705  rrx2plordisom  48709  line2ylem  48737  line2  48738  line2x  48740  inlinecirc02plem  48772  mosn  48798  mof0  48823  mof0ALT  48825  tposrescnv  48864  tposres3  48866  tposideq2  48874  f1omoOLD  48879  nelsubc3  49057  reldmxpc  49232  reldmprcof1  49367  setc1onsubc  49588  reldmlmd2  49639  reldmcmd2  49640  rellmd  49645  relcmd  49646  ex-gte  49715  empty-surprise  49768  eximp-surprise2  49771  amgmw2d  49790