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  1528  tru  1545  had1  1604  nic-mpALT  1673  nic-ax  1674  nic-axALT  1675  nfi  1789  mpgbir  1800  nfxfr  1854  19.35ri  1880  ax5e  1913  ax6ev  1970  equsb1v  2108  ax13  2375  ax13ALT  2425  moanmo  2617  axi12  2701  axbnd  2702  axexte  2704  axextmo  2707  nulmo  2708  vexw  2715  eqeltri  2827  nfcxfr  2892  neir  2931  neirr  2937  eqnetri  2998  nelir  3035  mprgbir  3054  issetri  3455  moeq  3666  rmoeq  3697  cdeqi  3724  eqsstri  3981  rmo0  4312  rabnc  4341  reuprg  4656  tpid1  4721  tpid2  4723  mosneq  4794  pwv  4856  uni0  4887  int0  4912  eqbrtri  5112  tr0  5210  trv  5211  zfrep4  5231  axnulALT  5242  0ex  5245  inex1  5255  elpwi2  5273  0elpw  5294  axpow2  5305  dvdemo1  5311  vpwex  5315  zfpair2  5371  exss  5403  brv  5412  opwo0id  5437  moop2  5442  0sn0ep  5520  po0  5541  epse  5598  relxp  5634  rel0  5739  relopabiv  5760  relopabi  5762  relopabiALT  5763  eliunxp  5777  opeliunxp2  5778  dmi  5861  dmep  5863  xpidtr  6069  xpima  6129  dmsn0  6156  cnvsn0  6157  0elon  6361  funmpt  6519  funmpt2  6520  funcnv0  6547  isarep2  6571  fresaunres2  6695  f0  6704  f10d  6797  f1o00  6798  f1oi  6801  f1osn  6803  brprcneu  6812  brprcneuALT  6813  opabiotafun  6902  fvopab3ig  6925  opabex  7154  eufnfv  7163  isof1oopb  7259  ncanth  7301  mpofun  7470  reldmmpo  7480  ovid  7487  ovidig  7488  ovidi  7489  ovig  7492  ov3  7509  caovmo  7583  relmptopab  7596  porpss  7660  uniex2  7671  tfinds2  7794  finds  7826  finds2  7828  oprabex  7908  oprabex3  7909  f1stres  7945  f2ndres  7946  relmpoopab  8024  fsplitfpar  8048  poseq  8088  opeliunxp2f  8140  tpos0  8186  issmo  8268  tfrlem6  8301  tfrlem8  8303  tfrlem16  8312  tfr1a  8313  tfr1  8316  tz7.44lem1  8324  seqomlem2  8370  seqomlem3  8371  seqomlem4  8372  fnseqom  8374  ord3  8400  0lt1o  8419  0we1  8421  naddf  8596  eqer  8658  ecopover  8745  mapsnf1o3  8819  ssdomg  8922  en0  8940  en0r  8942  ensn1  8943  0fi  8964  enrefnn  8968  xpcomf1o  8979  map2xp  9060  limensuci  9066  1sdom2  9132  sdom1  9134  unblem4  9179  fidomdm  9218  marypha1lem  9317  hartogslem1  9428  hartogs  9430  card2on  9440  nelaneqOLD  9488  epinid0  9489  ruALT  9492  disjcsn  9493  elnanel  9497  cnvepnep  9498  inf2  9513  inf3lem6  9523  infeq5i  9526  zfinf2  9532  cantnflt  9562  cnfcom  9590  trcl  9618  tz9.1c  9620  tc2  9632  r1funlim  9656  r1fnon  9657  karden  9785  tskwe  9840  cardprclem  9869  pm54.43  9891  r0weon  9900  iunmapdisj  9911  alephfnon  9953  alephfplem4  9995  alephfp  9996  alephval3  9998  kmlem2  10040  dju1dif  10061  ackbij1  10125  ackbij2lem2  10127  ackbij2  10130  infpssrlem3  10193  hsmexlem4  10317  hsmexlem5  10318  ac2  10349  axac3  10352  ac6  10368  axdclem2  10408  dmct  10412  ondomon  10451  alephsucpw  10458  pwcfsdom  10471  cfpwsdom  10472  smobeth  10474  axpowndlem3  10487  zfcndun  10503  zfcndpow  10504  zfcndinf  10506  zfcndac  10507  wunex2  10626  uniwun  10628  wuncval2  10635  grur1  10708  axgroth5  10712  axgroth2  10713  axgroth6  10716  axgroth3  10719  grothtsk  10723  inaprc  10724  ltsopi  10776  dmaddpi  10778  dmmulpi  10779  1lt2pi  10793  nqerf  10818  addnqf  10836  mulnqf  10837  1lt2nq  10861  m1p1sr  10980  m1m1sr  10981  0lt1sr  10983  axaddf  11033  axmulf  11034  ax1cn  11037  subaddrii  11447  ixi  11743  recgt0ii  12025  nn1suc  12144  4d2e2  12287  arch  12375  un0mulcl  12412  pnf0xnn0  12458  3halfnz  12549  nummac  12630  indstr  12811  mnfltpnf  13022  ioof  13344  0nelfz1  13440  fzp1disj  13480  fzp1nel  13508  fzof  13553  fvf1tp  13690  om2uzrani  13856  om2uzf1oi  13857  uzrdglem  13861  uzrdgfni  13862  uzrdg0i  13863  ltwenn  13866  hashgf1o  13875  axdc4uzlem  13887  sq0  14096  irec  14105  facmapnn  14189  hashkf  14236  hashfxnn0  14241  hashf  14242  hash0  14271  prhash2ex  14303  hashsslei  14330  hashxplem  14337  hashbclem  14356  hashf1lem1  14359  tpf1ofv0  14400  tpfo  14404  s1dm  14513  eqs1  14517  ccat2s1p1  14534  cats1un  14625  revs1  14669  0csh0  14697  cshw1  14726  cats1fvn  14762  funcnvs1  14816  pfx2  14851  relexp0g  14926  relexpsucnnr  14929  rtrclreclem1  14961  dfrtrclrec2  14962  rtrclreclem2  14963  rtrclreclem4  14965  dfrtrcl2  14966  climmo  15461  fsumcom2  15678  ackbijnn  15732  incexclem  15740  infcvgaux1i  15761  fprodcom2  15888  bpolylem  15952  bpoly3  15962  bpoly4  15963  efcvgfsum  15990  cos1bnd  16093  cos2bnd  16094  znnen  16118  qnnen  16119  aleph1re  16151  3dvds  16239  n2dvdsm1  16277  divalglem5  16305  flodddiv4  16323  sadcaddlem  16365  sadadd2lem  16367  sadadd3  16369  sadaddlem  16374  lcmf0  16542  lcmfunsnlem2lem1  16546  lcmfunsnlem2  16548  coprmprod  16569  coprmproddvdslem  16570  2prm  16600  3lcm2e6  16640  phicl2  16676  pockthi  16816  unbenlem  16817  prmrec  16831  vdwlem13  16902  vdwnn  16907  ramcl2  16925  prmgapprmo  16971  mod2xnegi  16980  modsubi  16981  structcnvcnv  17061  strleun  17065  setsres  17086  strfv  17111  starvndxnbasendx  17205  starvndxnplusgndx  17206  starvndxnmulrndx  17207  scandxnbasendx  17217  scandxnplusgndx  17218  scandxnmulrndx  17219  vscandxnbasendx  17222  vscandxnplusgndx  17223  vscandxnmulrndx  17224  vscandxnscandx  17225  ipndxnbasendx  17233  ipndxnplusgndx  17234  ipndxnmulrndx  17235  slotsdifipndx  17236  tsetndxnplusgndx  17258  tsetndxnmulrndx  17259  tsetndxnstarvndx  17260  slotstnscsi  17261  plendxnplusgndx  17272  plendxnmulrndx  17273  plendxnscandx  17274  plendxnvscandx  17275  slotsdifplendx  17276  basendxnocndx  17284  plendxnocndx  17285  dsndxnplusgndx  17291  dsndxnmulrndx  17292  slotsdnscsi  17293  dsndxntsetndx  17294  slotsdifdsndx  17295  unifndxntsetndx  17301  slotsdifunifndx  17302  slotsdifplendx2  17317  slotsdifocndx  17318  0rest  17330  firest  17333  restid  17334  prdsval  17356  prdsbas  17358  prdsplusg  17359  prdsmulr  17360  prdsvsca  17361  imasaddfnlem  17429  imasvscafn  17438  2oppchomf  17627  0ssc  17741  0subcat  17742  idfucl  17785  homarel  17940  dmaf  17953  cdaf  17954  setc2ohom  17999  catcfuccl  18022  relxpchom  18084  catcxpccl  18110  oppchofcl  18163  oyoncl  18173  letsr  18496  nulchn  18522  s1chn  18523  chnub  18525  chninf  18538  ex-chn1  18540  mgmidmo  18565  efmndmgm  18790  smndex1ibas  18805  smndex1mgm  18812  smndex1mnd  18815  smndex2dbas  18819  smndex2dnrinv  18820  smndex2hbas  18821  pwmnd  18842  releqg  19085  ga0  19208  psgnunilem3  19406  psgnunilem4  19407  pmtrsn  19429  efgval  19627  efger  19628  efgsval2  19643  efgsp1  19647  efgsfo  19649  efgredleme  19653  efgredlem  19657  efgred  19658  cygctb  19802  gsum2d2lem  19883  gsum2d2  19884  gsumcom2  19885  dprd2d2  19956  pgpfaclem1  19993  gsumle  20055  reldvdsr  20276  fldhmsubc  20698  00lsp  20912  cnfldfun  21303  cnfldfunALT  21304  cnfldfunOLD  21316  cnfldfunALTOLD  21317  xrsmgm  21341  pzriprnglem8  21423  pzriprnglem13  21428  pzriprnglem14  21429  pzriprngALT  21430  resubdrg  21543  ocv0  21612  cssval  21617  islinds2  21748  psrvscafval  21883  psrbag0  21995  psdmvr  22082  00ply1bas  22150  ply1plusgfvi  22152  m2detleib  22544  tgdom  22891  tgidm  22893  indistps2ALT  22927  restbas  23071  resttopon  23074  rest0  23082  leordtval2  23125  iocpnfordt  23128  icomnfordt  23129  iooordt  23130  ist1-3  23262  1stcfb  23358  comppfsc  23445  1stckgen  23467  ptbasfi  23494  dfac14  23531  opnfbas  23755  hauspwpwf1  23900  alexsubALT  23964  ptcmplem5  23969  cnextrel  23976  ust0  24133  0met  24279  prdsdsf  24280  prdsxmetlem  24281  prdsmet  24283  prdsbl  24404  qtopbaslem  24671  xrtgioo  24720  xrsdsre  24724  zcld  24727  recld2  24728  reperflem  24732  retopconn  24743  iccpnfcnv  24867  bndth  24882  nmoleub2lem2  25041  zclmncvs  25073  recmet  25248  resscdrg  25283  ishl2  25295  recms  25305  volf  25455  iundisj2  25475  volsup  25482  icombl  25490  ioombl  25491  ismbf3d  25580  0plef  25598  0pledm  25599  itg1ge0  25612  mbfi1fseqlem5  25645  itg2addlem  25684  reldv  25796  limciun  25820  dvexp  25882  dveflem  25908  lhop1lem  25943  lhop  25946  elply2  26126  elplyd  26132  ply1term  26134  ply0  26138  plymullem  26146  qaa  26256  pserulm  26356  pserdvlem2  26363  efcn  26378  sincosq1lem  26431  tangtx  26439  sincos4thpi  26447  pigt3  26452  pige3ALT  26454  efif1olem4  26479  logf1o  26498  relogf1o  26500  log1  26519  loge  26520  logi  26521  relogiso  26532  dvrelog  26571  relogcn  26572  logcn  26581  cxpcn3  26683  resqrtcn  26684  rtprmirr  26695  2logb9irr  26730  leibpi  26877  log2ublem1  26881  birthday  26889  emcllem5  26935  harmonicbnd  26939  harmonicbnd2  26940  harmonicbnd3  26943  lgamgulm2  26971  lgamcvglem  26975  gamf  26978  ppiltx  27112  ppiublem1  27138  ppiub  27140  bclbnd  27216  bpos1lem  27218  bposlem8  27227  lgsquadlem2  27317  2sqlem9  27363  2sqlem10  27364  addsqnreup  27379  chebbnd1  27408  selberg2lem  27486  pntrsumo1  27501  selbergsb  27511  pntpbnd  27524  sltval2  27593  noxp1o  27600  nosepnelem  27616  noetasuplem2  27671  noetainflem2  27675  0slt1s  27771  addsf  27923  precsexlem1  28143  precsexlem2  28144  precsexlem3  28145  precsexlem4  28146  precsexlem5  28147  precsexlem9  28151  precsexlem10  28152  precsexlem11  28153  elons2  28193  onscutlt  28199  onsiso  28203  onswe  28204  onsse  28205  onaddscl  28208  onmulscl  28209  eln0s  28285  0zs  28310  zseo  28343  twocut  28344  lngndxnitvndx  28419  istrkg2ld  28436  tgcgr4  28507  ax5seglem7  28911  axlowdimlem4  28921  axlowdimlem6  28923  axlowdimlem7  28924  axlowdimlem10  28927  axlowdimlem13  28930  axlowdimlem16  28933  uhgr0e  29047  uhgr0  29049  upgrbi  29069  umgrbi  29077  usgr0  29219  lfuhgr1v0e  29230  usgrexmpllem  29236  usgrexmpl  29239  griedg0prc  29240  cplgr0  29401  usgrexilem  29416  cffldtocusgr  29423  cffldtocusgrOLD  29424  rgrusgrprc  29566  rusgrprc  29567  rgrprcx  29569  rgrx0ndm  29570  usgr2pthlem  29739  pthdlem2  29744  uspgrn2crct  29784  wwlksnext  29869  clwwlknondisj  30086  0ewlk  30089  0wlk  30091  0pth  30100  1pthdlem1  30110  1trld  30117  wlk2v2elem2  30131  wlk2v2e  30132  upgr3v3e3cycl  30155  upgr4cycl4dv4e  30160  dfconngr1  30163  0conngr  30167  konigsbergumgr  30226  2wspmdisj  30312  2clwwlk2clwwlk  30325  numclwwlk3lem2lem  30358  numclwwlk3lem2  30359  ex-dif  30398  ex-in  30400  ex-eprel  30408  ex-id  30409  ex-fl  30422  ex-mod  30424  ex-hash  30428  ex-fpar  30437  avril1  30438  2bornot2b  30439  0vfval  30581  vsfval  30608  ajmoi  30833  ajfuni  30834  normlem2  31086  norm3adifii  31123  hhip  31152  hlim0  31210  hlimcaui  31211  hlimf  31212  hhssnv  31239  shscli  31292  shsval2i  31362  h1de2i  31528  fh3i  31598  fh4i  31599  cm2mi  31601  qlaxr3i  31611  mayetes3i  31704  ho0f  31726  hoif  31729  hodidi  31762  ho0subi  31770  hosd1i  31797  adjmo  31807  nmopsetn0  31840  nmfnsetn0  31853  funadj  31861  funcnvadj  31868  nmcexi  32001  cnlnadjlem8  32049  nmoptri2i  32074  opsqrlem4  32118  hmopidmchi  32126  pjoci  32155  pjinvari  32166  abrexdomjm  32482  elim2ifim  32520  iundisj2f  32565  rinvf1o  32607  dfcnv2  32653  snct  32690  fzodif2  32769  iundisj2fi  32774  dp2lt10  32859  dp2ltc  32862  dplti  32880  dpgti  32881  dpexpp1  32883  xrge0slmod  33308  isconstr  33744  zarcls  33882  zartopn  33883  xrge0pluscn  33948  qqhre  34028  esumrnmpt2  34076  esumfsup  34078  esumpcvgval  34086  hasheuni  34093  esumcvg  34094  esumcvgsum  34096  esumsup  34097  esum2d  34101  dmsigagen  34152  ldgenpisyslem3  34173  measvuni  34222  voliune  34237  volfiniune  34238  br2base  34277  dya2iocuni  34291  eulerpartlem1  34375  eulerpartlemt  34379  eulerpartgbij  34380  fib0  34407  coinfliprv  34491  ballotlem2  34497  ballotlemic  34515  ballotlem7  34544  ballotth  34546  plymul02  34554  rpsqrtcn  34601  chtvalz  34637  circlemethnat  34649  circlevma  34650  circlemethhgt  34651  hgt750lem  34659  bnj226  34741  bnj1101  34791  bnj110  34865  bnj149  34882  bnj150  34883  bnj151  34884  bnj517  34892  bnj580  34920  bnj865  34930  bnj900  34936  bnj996  34963  bnj1110  34989  bnj1133  34996  bnj1128  34997  bnj1145  35000  bnj1137  35002  bnj1171  35007  bnj1176  35012  setinds2regs  35117  tz9.1regs  35118  fineqvnttrclse  35132  f1resfz0f1d  35146  subfacp1lem5  35216  subfacp1lem6  35217  kur14lem9  35246  cvmcov2  35307  cvmliftlem1  35317  cvmliftlem4  35320  cvmliftlem5  35321  gonanegoal  35384  satfv0  35390  satfv0fun  35403  fmlan0  35423  gonan0  35424  fmla0disjsuc  35430  ex-sategoelel12  35459  msrfo  35578  problem5  35701  brtpid1  35753  brtpid2  35754  brtpid3  35755  faclimlem1  35775  axextndbi  35837  txprel  35912  relsset  35921  relbigcup  35930  fvbigcup  35935  fnsingle  35952  fvsingle  35953  snelsingles  35955  funimage  35961  fullfunfnv  35979  imagesset  35986  funtransport  36064  colinrel  36090  funray  36173  funline  36175  0hf  36210  neibastop2lem  36393  filnetlem3  36413  nrmo  36443  waj-ax  36447  lukshef-ax2  36448  arg-ax  36449  limsucncmpi  36478  dnizeq0  36508  knoppcnlem8  36533  knoppcnlem11  36536  cnndvlem1  36570  bj-babylob  36637  bj-ax12ssb  36691  bj-nnfnth  36776  bj-snsetex  36996  bj-0eltag  37011  bj-2upln0  37056  bj-2upln1upl  37057  bj-snexg  37067  bj-unexg  37071  bj-adjg1  37076  f1omptsnlem  37369  f1omptsn  37370  icoreresf  37385  relowlssretop  37396  relowlpssretop  37397  domalom  37437  matunitlindf  37657  poimirlem3  37662  poimirlem9  37668  poimirlem16  37675  poimirlem17  37676  poimirlem18  37677  poimirlem19  37678  poimirlem20  37679  poimirlem26  37685  mblfinlem1  37696  mblfinlem2  37697  ismblfin  37700  voliunnfl  37703  cnambfre  37707  abrexdom  37769  fdc  37784  cncfres  37804  heibor1lem  37848  grposnOLD  37921  bicontr  38119  an12i  38137  tsim1  38169  ac6s6f  38212  vvdifopab  38294  brcnvrabga  38369  opabf  38395  xrnrel  38400  relcoels  38460  cnvcosseq  38473  refrelcoss3  38499  refrelcoss2  38500  symrelcoss2  38502  refrelcoss  38559  symrelcoss  38596  n0eldmqs  38684  ax13fromc9  38944  dedths  39000  renegclALT  39001  12gcd5e1  42035  60gcd7e1  42037  lcmineqlem23  42083  dvrelog2  42096  dvrelog3  42097  dvrelog2b  42098  aks4d1p1p6  42105  aks4d1p1p7  42106  aks4d1p1  42108  sticksstones22  42200  sn-axprlem3  42249  acos1half  42390  moxfr  42724  mapfzcons1  42749  diophrw  42791  0dioph  42810  vdioph  42811  rabren3dioph  42847  2nn0ind  42977  rpnnen3  43064  kelac2lem  43096  frlmpwfi  43130  oaordnrex  43327  omnord1ex  43336  oenord1ex  43347  oaomoencom  43349  ifpbiidcor2  43515  iscard4  43565  sqrtcval  43673  resqrtvalex  43677  eliunov2  43711  xphe  43813  0he  43814  he0  43816  snhesn  43818  idhe  43819  frege54cor1c  43947  clsk1independent  44078  neicvgnvor  44148  amgm2d  44230  amgm3d  44231  amgm4d  44232  ismnushort  44333  lhe4.4ex1a  44361  rusbcALT  44470  ipo0  44480  ifr0  44481  vk15.4j  44560  2sb5nd  44592  dfvd1ir  44605  dfvd2anir  44616  dfvd2ir  44618  dfvd3ir  44625  dfvd3anir  44628  iden2  44646  e0bir  44808  uun2221p1  44845  uun2221p2  44846  2sb5ndVD  44941  2sb5ndALT  44963  iunconnlem2  44966  trwf  44991  wfaxext  45025  wfaxpow  45029  wfaxinf2  45033  wfac8prim  45034  permaxinf2lem  45044  nregmodelf1o  45047  fnchoice  45065  unisn0  45090  eliincex  45146  icof  45255  fnmptif  45301  supminfxr  45501  rexanuz2nf  45529  fsumiunss  45614  climlimsupcex  45806  liminfltlimsupex  45818  liminflelimsupcex  45834  xlimrel  45857  xlimfun  45892  resincncf  45912  dvnprodlem3  45985  volioc  46009  volico  46020  dmvolss  46022  volioof  46024  stoweidlem13  46050  stoweidlem34  46071  stirlinglem5  46115  stirlinglem13  46123  stirlingr  46127  fourierdlem42  46186  fourierdlem62  46205  fouriersw  46268  etransc  46320  salexct  46371  salexct2  46376  salgencntex  46380  sge0rnn0  46405  gsumge0cl  46408  sge00  46413  sge0resplit  46443  sge0reuz  46484  omeiunle  46554  0ome  46566  icoresmbl  46580  ovn0lem  46602  ovnhoilem1  46638  hspmbl  46666  nsssmfmbf  46816  mbfpsssmf  46820  smfresal  46825  smfmullem4  46831  smfpimbor1lem1  46835  smfpimbor1lem2  46836  lambert0  46917  lamberte  46918  cjnpoly  46919  tannpoly  46920  sinnpoly  46921  aistia  46927  aisfina  46928  aiffnbandciffatnotciffb  46934  axorbciffatcxorb  46935  abnotbtaxb  46945  abnotataxb  46946  eusnsn  47056  aiotaval  47125  aiota0ndef  47127  fundcmpsurinjimaid  47441  ichv  47479  ichf  47480  ichid  47481  icht  47482  ichcircshi  47484  icheq  47492  spr0nelg  47506  m3prm  47622  m7prm  47630  0noddALTV  47719  2noddALTV  47723  341fppr2  47764  9fppr8  47767  nfermltl8rev  47772  nfermltl2rev  47773  nfermltlrev  47774  sbgoldbo  47817  nnsum3primes4  47818  evengpop3  47828  stgr1  47991  usgrexmpl1lem  48051  usgrexmpl1  48052  usgrexmpl1tri  48055  usgrexmpl2lem  48056  usgrexmpl2  48057  usgrexmpl2nb0  48061  usgrexmpl2nb1  48062  usgrexmpl2nb2  48063  usgrexmpl2nb3  48064  usgrexmpl2nb4  48065  usgrexmpl2nb5  48066  gpgedg2ov  48096  gpgedg2iv  48097  gpg5nbgrvtx03starlem1  48098  gpg5nbgrvtx03starlem2  48099  gpg5nbgrvtx03starlem3  48100  gpg5nbgrvtx13starlem1  48101  gpg5nbgrvtx13starlem2  48102  gpg5nbgrvtx13starlem3  48103  gpg5grlim  48123  gpg5grlic  48124  gpgprismgr4cycllem2  48126  gpgprismgr4cycllem7  48131  pg4cyclnex  48157  gpg5edgnedg  48160  grlimedgnedg  48161  oddinmgm  48205  nn0mnd  48209  2zrngamgm  48275  2zrngaabl  48280  2zrngmmgm  48282  2zrngnring  48288  fldhmsubcALTV  48363  eliunxp2  48364  zlmodzxzldeplem  48529  zlmodzxzldep  48535  ldepslinc  48540  rrx2xpreen  48750  rrx2plordisom  48754  line2ylem  48782  line2  48783  line2x  48785  inlinecirc02plem  48817  mosn  48843  mof0  48868  mof0ALT  48870  tposrescnv  48909  tposres3  48911  tposideq2  48919  f1omoOLD  48924  nelsubc3  49102  reldmxpc  49277  reldmprcof1  49412  setc1onsubc  49633  reldmlmd2  49684  reldmcmd2  49685  rellmd  49690  relcmd  49691  ex-gte  49760  empty-surprise  49813  eximp-surprise2  49816  amgmw2d  49835