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  3323  issetri  3466  moeq  3678  rmoeq  3709  cdeqi  3736  eqsstri  3993  rmo0  4325  rabnc  4354  reuprg  4667  tpid1  4732  tpid2  4734  mosneq  4806  pwv  4868  uni0  4899  int0  4926  eqbrtri  5128  tr0  5227  trv  5228  zfrep4  5248  axnulALT  5259  0ex  5262  inex1  5272  elpwi2  5290  0elpw  5311  axpow2  5322  dvdemo1  5328  vpwex  5332  zfpair2  5388  exss  5423  brv  5432  opwo0id  5457  moop2  5462  0sn0ep  5542  po0  5563  epse  5620  relxp  5656  rel0  5762  relopabiv  5783  relopabi  5785  relopabiALT  5786  eliunxp  5801  opeliunxp2  5802  dmi  5885  dmep  5887  xpidtr  6095  xpima  6155  dmsn0  6182  cnvsn0  6183  0elon  6387  funmpt  6554  funmpt2  6555  funcnv0  6582  isarep2  6608  fresaunres2  6732  f0  6741  f10d  6834  f1o00  6835  f1oi  6838  f1osn  6840  brprcneu  6848  brprcneuALT  6849  opabiotafun  6941  fvopab3ig  6964  opabex  7194  eufnfv  7203  isof1oopb  7300  ncanth  7342  mpofun  7513  reldmmpo  7523  ovid  7530  ovidig  7531  ovidi  7532  ovig  7535  ov3  7552  caovmo  7626  relmptopab  7639  porpss  7703  uniex2  7714  tfinds2  7840  finds  7872  finds2  7874  oprabex  7955  oprabex3  7956  f1stres  7992  f2ndres  7993  relmpoopab  8073  fsplitfpar  8097  poseq  8137  opeliunxp2f  8189  tpos0  8235  issmo  8317  tfrlem6  8350  tfrlem8  8352  tfrlem16  8361  tfr1a  8362  tfr1  8365  tz7.44lem1  8373  seqomlem2  8419  seqomlem3  8420  seqomlem4  8421  fnseqom  8423  ord3  8449  0lt1o  8468  0we1  8470  naddf  8645  eqer  8707  ecopover  8794  mapsnf1o3  8868  ssdomg  8971  en0  8989  en0r  8991  ensn1  8992  0fi  9013  snfiOLD  9015  enrefnn  9018  xpcomf1o  9030  map2xp  9111  limensuci  9117  1sdom2  9187  sdom1  9189  sdom1OLD  9190  unblem4  9242  fidomdm  9285  marypha1lem  9384  hartogslem1  9495  hartogs  9497  card2on  9507  nelaneq  9552  epinid0  9553  ruALT  9556  disjcsn  9557  elnanel  9560  cnvepnep  9561  inf2  9576  inf3lem6  9586  infeq5i  9589  zfinf2  9595  cantnflt  9625  cnfcom  9653  trcl  9681  tz9.1c  9683  tc2  9695  r1funlim  9719  r1fnon  9720  karden  9848  tskwe  9903  cardprclem  9932  pm54.43  9954  r0weon  9965  iunmapdisj  9976  alephfnon  10018  alephfplem4  10060  alephfp  10061  alephval3  10063  kmlem2  10105  dju1dif  10126  ackbij1  10190  ackbij2lem2  10192  ackbij2  10195  infpssrlem3  10258  hsmexlem4  10382  hsmexlem5  10383  ac2  10414  axac3  10417  ac6  10433  axdclem2  10473  dmct  10477  ondomon  10516  alephsucpw  10523  pwcfsdom  10536  cfpwsdom  10537  smobeth  10539  axpowndlem3  10552  zfcndun  10568  zfcndpow  10569  zfcndinf  10571  zfcndac  10572  wunex2  10691  uniwun  10693  wuncval2  10700  grur1  10773  axgroth5  10777  axgroth2  10778  axgroth6  10781  axgroth3  10784  grothtsk  10788  inaprc  10789  ltsopi  10841  dmaddpi  10843  dmmulpi  10844  1lt2pi  10858  nqerf  10883  addnqf  10901  mulnqf  10902  1lt2nq  10926  m1p1sr  11045  m1m1sr  11046  0lt1sr  11048  axaddf  11098  axmulf  11099  ax1cn  11102  subaddrii  11511  ixi  11807  recgt0ii  12089  nn1suc  12208  4d2e2  12351  arch  12439  un0mulcl  12476  pnf0xnn0  12522  3halfnz  12613  nummac  12694  indstr  12875  mnfltpnf  13086  ioof  13408  0nelfz1  13504  fzp1disj  13544  fzp1nel  13572  fzof  13617  fvf1tp  13751  om2uzrani  13917  om2uzf1oi  13918  uzrdglem  13922  uzrdgfni  13923  uzrdg0i  13924  ltwenn  13927  hashgf1o  13936  axdc4uzlem  13948  sq0  14157  irec  14166  facmapnn  14250  hashkf  14297  hashfxnn0  14302  hashf  14303  hash0  14332  prhash2ex  14364  hashsslei  14391  hashxplem  14398  hashbclem  14417  hashf1lem1  14420  tpf1ofv0  14461  tpfo  14465  s1dm  14573  eqs1  14577  ccat2s1p1  14594  cats1un  14686  revs1  14730  0csh0  14758  cshw1  14787  cats1fvn  14824  funcnvs1  14878  pfx2  14913  relexp0g  14988  relexpsucnnr  14991  rtrclreclem1  15023  dfrtrclrec2  15024  rtrclreclem2  15025  rtrclreclem4  15027  dfrtrcl2  15028  climmo  15523  fsumcom2  15740  ackbijnn  15794  incexclem  15802  infcvgaux1i  15823  fprodcom2  15950  bpolylem  16014  bpoly3  16024  bpoly4  16025  efcvgfsum  16052  cos1bnd  16155  cos2bnd  16156  znnen  16180  qnnen  16181  aleph1re  16213  3dvds  16301  n2dvdsm1  16339  divalglem5  16367  flodddiv4  16385  sadcaddlem  16427  sadadd2lem  16429  sadadd3  16431  sadaddlem  16436  lcmf0  16604  lcmfunsnlem2lem1  16608  lcmfunsnlem2  16610  coprmprod  16631  coprmproddvdslem  16632  2prm  16662  3lcm2e6  16702  phicl2  16738  pockthi  16878  unbenlem  16879  prmrec  16893  vdwlem13  16964  vdwnn  16969  ramcl2  16987  prmgapprmo  17033  mod2xnegi  17042  modsubi  17043  structcnvcnv  17123  strleun  17127  setsres  17148  strfv  17173  starvndxnbasendx  17267  starvndxnplusgndx  17268  starvndxnmulrndx  17269  scandxnbasendx  17279  scandxnplusgndx  17280  scandxnmulrndx  17281  vscandxnbasendx  17284  vscandxnplusgndx  17285  vscandxnmulrndx  17286  vscandxnscandx  17287  ipndxnbasendx  17295  ipndxnplusgndx  17296  ipndxnmulrndx  17297  slotsdifipndx  17298  tsetndxnplusgndx  17320  tsetndxnmulrndx  17321  tsetndxnstarvndx  17322  slotstnscsi  17323  plendxnplusgndx  17334  plendxnmulrndx  17335  plendxnscandx  17336  plendxnvscandx  17337  slotsdifplendx  17338  basendxnocndx  17346  plendxnocndx  17347  dsndxnplusgndx  17353  dsndxnmulrndx  17354  slotsdnscsi  17355  dsndxntsetndx  17356  slotsdifdsndx  17357  unifndxntsetndx  17363  slotsdifunifndx  17364  slotsdifplendx2  17379  slotsdifocndx  17380  0rest  17392  firest  17395  restid  17396  prdsval  17418  prdsbas  17420  prdsplusg  17421  prdsmulr  17422  prdsvsca  17423  imasaddfnlem  17491  imasvscafn  17500  2oppchomf  17685  0ssc  17799  0subcat  17800  idfucl  17843  homarel  17998  dmaf  18011  cdaf  18012  setc2ohom  18057  catcfuccl  18080  relxpchom  18142  catcxpccl  18168  oppchofcl  18221  oyoncl  18231  letsr  18552  mgmidmo  18587  efmndmgm  18812  smndex1ibas  18827  smndex1mgm  18834  smndex1mnd  18837  smndex2dbas  18841  smndex2dnrinv  18842  smndex2hbas  18843  pwmnd  18864  releqg  19107  ga0  19230  psgnunilem3  19426  psgnunilem4  19427  pmtrsn  19449  efgval  19647  efger  19648  efgsval2  19663  efgsp1  19667  efgsfo  19669  efgredleme  19673  efgredlem  19677  efgred  19678  cygctb  19822  gsum2d2lem  19903  gsum2d2  19904  gsumcom2  19905  dprd2d2  19976  pgpfaclem1  20013  reldvdsr  20269  fldhmsubc  20694  00lsp  20887  cnfldfun  21278  cnfldfunALT  21279  cnfldfunOLD  21291  cnfldfunALTOLD  21292  xrsmgm  21318  pzriprnglem8  21398  pzriprnglem13  21403  pzriprnglem14  21404  pzriprngALT  21405  resubdrg  21517  ocv0  21586  cssval  21591  islinds2  21722  psrvscafval  21857  psrbag0  21969  psdmvr  22056  00ply1bas  22124  ply1plusgfvi  22126  m2detleib  22518  tgdom  22865  tgidm  22867  indistps2ALT  22901  restbas  23045  resttopon  23048  rest0  23056  leordtval2  23099  iocpnfordt  23102  icomnfordt  23103  iooordt  23104  ist1-3  23236  1stcfb  23332  comppfsc  23419  1stckgen  23441  ptbasfi  23468  dfac14  23505  opnfbas  23729  hauspwpwf1  23874  alexsubALT  23938  ptcmplem5  23943  cnextrel  23950  ust0  24107  0met  24254  prdsdsf  24255  prdsxmetlem  24256  prdsmet  24258  prdsbl  24379  qtopbaslem  24646  xrtgioo  24695  xrsdsre  24699  zcld  24702  recld2  24703  reperflem  24707  retopconn  24718  iccpnfcnv  24842  bndth  24857  nmoleub2lem2  25016  zclmncvs  25048  recmet  25223  resscdrg  25258  ishl2  25270  recms  25280  volf  25430  iundisj2  25450  volsup  25457  icombl  25465  ioombl  25466  ismbf3d  25555  0plef  25573  0pledm  25574  itg1ge0  25587  mbfi1fseqlem5  25620  itg2addlem  25659  reldv  25771  limciun  25795  dvexp  25857  dveflem  25883  lhop1lem  25918  lhop  25921  elply2  26101  elplyd  26107  ply1term  26109  ply0  26113  plymullem  26121  qaa  26231  pserulm  26331  pserdvlem2  26338  efcn  26353  sincosq1lem  26406  tangtx  26414  sincos4thpi  26422  pigt3  26427  pige3ALT  26429  efif1olem4  26454  logf1o  26473  relogf1o  26475  log1  26494  loge  26495  logi  26496  relogiso  26507  dvrelog  26546  relogcn  26547  logcn  26556  cxpcn3  26658  resqrtcn  26659  rtprmirr  26670  2logb9irr  26705  leibpi  26852  log2ublem1  26856  birthday  26864  emcllem5  26910  harmonicbnd  26914  harmonicbnd2  26915  harmonicbnd3  26918  lgamgulm2  26946  lgamcvglem  26950  gamf  26953  ppiltx  27087  ppiublem1  27113  ppiub  27115  bclbnd  27191  bpos1lem  27193  bposlem8  27202  lgsquadlem2  27292  2sqlem9  27338  2sqlem10  27339  addsqnreup  27354  chebbnd1  27383  selberg2lem  27461  pntrsumo1  27476  selbergsb  27486  pntpbnd  27499  sltval2  27568  noxp1o  27575  nosepnelem  27591  noetasuplem2  27646  noetainflem2  27650  0slt1s  27741  addsf  27889  precsexlem1  28109  precsexlem2  28110  precsexlem3  28111  precsexlem4  28112  precsexlem5  28113  precsexlem9  28117  precsexlem10  28118  precsexlem11  28119  elons2  28159  onscutlt  28165  onsiso  28169  onswe  28170  onsse  28171  onaddscl  28174  onmulscl  28175  eln0s  28251  0zs  28276  zseo  28308  twocut  28309  lngndxnitvndx  28370  istrkg2ld  28387  tgcgr4  28458  ax5seglem7  28862  axlowdimlem4  28872  axlowdimlem6  28874  axlowdimlem7  28875  axlowdimlem10  28878  axlowdimlem13  28881  axlowdimlem16  28884  uhgr0e  28998  uhgr0  29000  upgrbi  29020  umgrbi  29028  usgr0  29170  lfuhgr1v0e  29181  usgrexmpllem  29187  usgrexmpl  29190  griedg0prc  29191  cplgr0  29352  usgrexilem  29367  cffldtocusgr  29374  cffldtocusgrOLD  29375  rgrusgrprc  29517  rusgrprc  29518  rgrprcx  29520  rgrx0ndm  29521  usgr2pthlem  29693  pthdlem2  29698  uspgrn2crct  29738  wwlksnext  29823  clwwlknondisj  30040  0ewlk  30043  0wlk  30045  0pth  30054  1pthdlem1  30064  1trld  30071  wlk2v2elem2  30085  wlk2v2e  30086  upgr3v3e3cycl  30109  upgr4cycl4dv4e  30114  dfconngr1  30117  0conngr  30121  konigsbergumgr  30180  2wspmdisj  30266  2clwwlk2clwwlk  30279  numclwwlk3lem2lem  30312  numclwwlk3lem2  30313  ex-dif  30352  ex-in  30354  ex-eprel  30362  ex-id  30363  ex-fl  30376  ex-mod  30378  ex-hash  30382  ex-fpar  30391  avril1  30392  2bornot2b  30393  0vfval  30535  vsfval  30562  ajmoi  30787  ajfuni  30788  normlem2  31040  norm3adifii  31077  hhip  31106  hlim0  31164  hlimcaui  31165  hlimf  31166  hhssnv  31193  shscli  31246  shsval2i  31316  h1de2i  31482  fh3i  31552  fh4i  31553  cm2mi  31555  qlaxr3i  31565  mayetes3i  31658  ho0f  31680  hoif  31683  hodidi  31716  ho0subi  31724  hosd1i  31751  adjmo  31761  nmopsetn0  31794  nmfnsetn0  31807  funadj  31815  funcnvadj  31822  nmcexi  31955  cnlnadjlem8  32003  nmoptri2i  32028  opsqrlem4  32072  hmopidmchi  32080  pjoci  32109  pjinvari  32120  abrexdomjm  32436  elim2ifim  32474  iundisj2f  32519  rinvf1o  32554  dfcnv2  32600  snct  32637  fzodif2  32714  iundisj2fi  32720  dp2lt10  32804  dp2ltc  32807  dplti  32825  dpgti  32826  dpexpp1  32828  s1chn  32936  chnub  32938  gsumle  33038  xrge0slmod  33319  isconstr  33726  zarcls  33864  zartopn  33865  xrge0pluscn  33930  qqhre  34010  esumrnmpt2  34058  esumfsup  34060  esumpcvgval  34068  hasheuni  34075  esumcvg  34076  esumcvgsum  34078  esumsup  34079  esum2d  34083  dmsigagen  34134  ldgenpisyslem3  34155  measvuni  34204  voliune  34219  volfiniune  34220  br2base  34260  dya2iocuni  34274  eulerpartlem1  34358  eulerpartlemt  34362  eulerpartgbij  34363  fib0  34390  coinfliprv  34474  ballotlem2  34480  ballotlemic  34498  ballotlem7  34527  ballotth  34529  plymul02  34537  rpsqrtcn  34584  chtvalz  34620  circlemethnat  34632  circlevma  34633  circlemethhgt  34634  hgt750lem  34642  bnj226  34724  bnj1101  34774  bnj110  34848  bnj149  34865  bnj150  34866  bnj151  34867  bnj517  34875  bnj580  34903  bnj865  34913  bnj900  34919  bnj996  34946  bnj1110  34972  bnj1133  34979  bnj1128  34980  bnj1145  34983  bnj1137  34985  bnj1171  34990  bnj1176  34995  f1resfz0f1d  35101  subfacp1lem5  35171  subfacp1lem6  35172  kur14lem9  35201  cvmcov2  35262  cvmliftlem1  35272  cvmliftlem4  35275  cvmliftlem5  35276  gonanegoal  35339  satfv0  35345  satfv0fun  35358  fmlan0  35378  gonan0  35379  fmla0disjsuc  35385  ex-sategoelel12  35414  msrfo  35533  problem5  35656  brtpid1  35708  brtpid2  35709  brtpid3  35710  faclimlem1  35730  axextndbi  35792  txprel  35867  relsset  35876  relbigcup  35885  fvbigcup  35890  fnsingle  35907  fvsingle  35908  snelsingles  35910  funimage  35916  fullfunfnv  35934  imagesset  35941  funtransport  36019  colinrel  36045  funray  36128  funline  36130  0hf  36165  neibastop2lem  36348  filnetlem3  36368  nrmo  36398  waj-ax  36402  lukshef-ax2  36403  arg-ax  36404  limsucncmpi  36433  dnizeq0  36463  knoppcnlem8  36488  knoppcnlem11  36491  cnndvlem1  36525  bj-babylob  36592  bj-ax12ssb  36646  bj-nnfnth  36731  bj-snsetex  36951  bj-0eltag  36966  bj-2upln0  37011  bj-2upln1upl  37012  bj-snexg  37022  bj-unexg  37026  bj-adjg1  37031  f1omptsnlem  37324  f1omptsn  37325  icoreresf  37340  relowlssretop  37351  relowlpssretop  37352  domalom  37392  matunitlindf  37612  poimirlem3  37617  poimirlem9  37623  poimirlem16  37630  poimirlem17  37631  poimirlem18  37632  poimirlem19  37633  poimirlem20  37634  poimirlem26  37640  mblfinlem1  37651  mblfinlem2  37652  ismblfin  37655  voliunnfl  37658  cnambfre  37662  abrexdom  37724  fdc  37739  cncfres  37759  heibor1lem  37803  grposnOLD  37876  bicontr  38074  an12i  38092  tsim1  38124  ac6s6f  38167  vvdifopab  38249  brcnvrabga  38324  opabf  38350  xrnrel  38355  relcoels  38415  cnvcosseq  38428  refrelcoss3  38454  refrelcoss2  38455  symrelcoss2  38457  refrelcoss  38514  symrelcoss  38551  n0eldmqs  38639  ax13fromc9  38899  dedths  38955  renegclALT  38956  12gcd5e1  41991  60gcd7e1  41993  lcmineqlem23  42039  dvrelog2  42052  dvrelog3  42053  dvrelog2b  42054  aks4d1p1p6  42061  aks4d1p1p7  42062  aks4d1p1  42064  sticksstones22  42156  sn-axprlem3  42205  acos1half  42346  moxfr  42680  mapfzcons1  42705  diophrw  42747  0dioph  42766  vdioph  42767  rabren3dioph  42803  2nn0ind  42934  rpnnen3  43021  kelac2lem  43053  frlmpwfi  43087  oaordnrex  43284  omnord1ex  43293  oenord1ex  43304  oaomoencom  43306  ifpbiidcor2  43472  iscard4  43522  sqrtcval  43630  resqrtvalex  43634  eliunov2  43668  xphe  43770  0he  43771  he0  43773  snhesn  43775  idhe  43776  frege54cor1c  43904  clsk1independent  44035  neicvgnvor  44105  amgm2d  44187  amgm3d  44188  amgm4d  44189  ismnushort  44290  lhe4.4ex1a  44318  rusbcALT  44428  ipo0  44438  ifr0  44439  vk15.4j  44518  2sb5nd  44550  dfvd1ir  44563  dfvd2anir  44574  dfvd2ir  44576  dfvd3ir  44583  dfvd3anir  44586  iden2  44604  e0bir  44766  uun2221p1  44803  uun2221p2  44804  2sb5ndVD  44899  2sb5ndALT  44921  iunconnlem2  44924  trwf  44949  wfaxext  44983  wfaxpow  44987  wfaxinf2  44991  wfac8prim  44992  permaxinf2lem  45002  nregmodelf1o  45005  fnchoice  45023  unisn0  45048  eliincex  45104  icof  45213  fnmptif  45259  supminfxr  45460  rexanuz2nf  45488  fsumiunss  45573  climlimsupcex  45767  liminfltlimsupex  45779  liminflelimsupcex  45795  xlimrel  45818  xlimfun  45853  resincncf  45873  dvnprodlem3  45946  volioc  45970  volico  45981  dmvolss  45983  volioof  45985  stoweidlem13  46011  stoweidlem34  46032  stirlinglem5  46076  stirlinglem13  46084  stirlingr  46088  fourierdlem42  46147  fourierdlem62  46166  fouriersw  46229  etransc  46281  salexct  46332  salexct2  46337  salgencntex  46341  sge0rnn0  46366  gsumge0cl  46369  sge00  46374  sge0resplit  46404  sge0reuz  46445  omeiunle  46515  0ome  46527  icoresmbl  46541  ovn0lem  46563  ovnhoilem1  46599  hspmbl  46627  nsssmfmbf  46777  mbfpsssmf  46781  smfresal  46786  smfmullem4  46792  smfpimbor1lem1  46796  smfpimbor1lem2  46797  lambert0  46888  lamberte  46889  cjnpoly  46890  tannpoly  46891  sinnpoly  46892  aistia  46898  aisfina  46899  aiffnbandciffatnotciffb  46905  axorbciffatcxorb  46906  abnotbtaxb  46916  abnotataxb  46917  eusnsn  47027  aiotaval  47096  aiota0ndef  47098  fundcmpsurinjimaid  47412  ichv  47450  ichf  47451  ichid  47452  icht  47453  ichcircshi  47455  icheq  47463  spr0nelg  47477  m3prm  47593  m7prm  47601  0noddALTV  47690  2noddALTV  47694  341fppr2  47735  9fppr8  47738  nfermltl8rev  47743  nfermltl2rev  47744  nfermltlrev  47745  sbgoldbo  47788  nnsum3primes4  47789  evengpop3  47799  stgr1  47960  usgrexmpl1lem  48012  usgrexmpl1  48013  usgrexmpl1tri  48016  usgrexmpl2lem  48017  usgrexmpl2  48018  usgrexmpl2nb0  48022  usgrexmpl2nb1  48023  usgrexmpl2nb2  48024  usgrexmpl2nb3  48025  usgrexmpl2nb4  48026  usgrexmpl2nb5  48027  gpgedg2ov  48057  gpgedg2iv  48058  gpg5nbgrvtx03starlem1  48059  gpg5nbgrvtx03starlem2  48060  gpg5nbgrvtx03starlem3  48061  gpg5nbgrvtx13starlem1  48062  gpg5nbgrvtx13starlem2  48063  gpg5nbgrvtx13starlem3  48064  gpg5grlic  48084  gpgprismgr4cycllem2  48086  gpgprismgr4cycllem7  48091  pg4cyclnex  48117  oddinmgm  48163  nn0mnd  48167  2zrngamgm  48233  2zrngaabl  48238  2zrngmmgm  48240  2zrngnring  48246  fldhmsubcALTV  48321  eliunxp2  48322  zlmodzxzldeplem  48487  zlmodzxzldep  48493  ldepslinc  48498  rrx2xpreen  48708  rrx2plordisom  48712  line2ylem  48740  line2  48741  line2x  48743  inlinecirc02plem  48775  mosn  48801  mof0  48826  mof0ALT  48828  tposrescnv  48867  tposres3  48869  tposideq2  48877  f1omoOLD  48882  nelsubc3  49060  reldmxpc  49235  reldmprcof1  49370  setc1onsubc  49591  reldmlmd2  49642  reldmcmd2  49643  rellmd  49648  relcmd  49649  ex-gte  49718  empty-surprise  49771  eximp-surprise2  49774  amgmw2d  49793