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  sbt  2071  equsb1v  2110  ax13  2377  ax13ALT  2427  moanmo  2619  axi12  2703  axbnd  2704  axexte  2706  axextmo  2709  nulmo  2710  vexw  2717  eqeltri  2829  nfcxfr  2893  neir  2932  neirr  2938  eqnetri  2999  nelir  3036  mprgbir  3055  issetri  3456  moeq  3662  rmoeq  3693  cdeqi  3720  eqsstri  3977  vn0  4294  rmo0  4311  ab0orv  4332  rabnc  4340  reuprg  4655  tpid1  4720  tpid2  4722  mosneq  4793  pwv  4855  uni0OLD  4887  int0  4912  eqbrtri  5114  tr0  5212  trv  5213  zfrep4  5233  axnulALT  5244  0ex  5247  inex1  5257  elpwi2  5275  0elpw  5296  axpow2  5307  dvdemo1  5313  vpwex  5317  zfpair2  5373  exss  5406  brv  5415  opwo0id  5440  moop2  5445  0sn0ep  5523  po0  5544  epse  5601  relxp  5637  rel0  5743  relopabiv  5764  relopabi  5766  relopabiALT  5767  eliunxp  5781  opeliunxp2  5782  dmi  5865  dmep  5867  xpidtr  6073  xpima  6134  dmsn0  6161  cnvsn0  6162  0elon  6366  funmpt  6524  funmpt2  6525  funcnv0  6552  isarep2  6576  fresaunres2  6700  f0  6709  f10d  6802  f1o00  6803  f1oi  6806  f1oiOLD  6807  f1osn  6809  brprcneu  6818  brprcneuALT  6819  opabiotafun  6908  fvopab3ig  6931  opabex  7160  eufnfv  7169  isof1oopb  7265  ncanth  7307  mpofun  7476  reldmmpo  7486  ovid  7493  ovidig  7494  ovidi  7495  ovig  7498  ov3  7515  caovmo  7589  relmptopab  7602  porpss  7666  uniex2  7677  tfinds2  7800  finds  7832  finds2  7834  oprabex  7914  oprabex3  7915  f1stres  7951  f2ndres  7952  relmpoopab  8030  fsplitfpar  8054  poseq  8094  opeliunxp2f  8146  tpos0  8192  issmo  8274  tfrlem6  8307  tfrlem8  8309  tfrlem16  8318  tfr1a  8319  tfr1  8322  tz7.44lem1  8330  seqomlem2  8376  seqomlem3  8377  seqomlem4  8378  fnseqom  8380  ord3  8406  0lt1o  8425  0we1  8427  naddf  8602  eqer  8664  ecopover  8751  mapsnf1o3  8825  ssdomg  8929  en0  8947  en0r  8949  ensn1  8950  0fi  8971  enrefnn  8975  xpcomf1o  8986  map2xp  9067  limensuci  9073  1sdom2  9139  sdom1  9141  unblem4  9186  fidomdm  9225  marypha1lem  9324  hartogslem1  9435  hartogs  9437  card2on  9447  nelaneqOLD  9495  epinid0  9496  ruALT  9499  disjcsn  9500  elnanel  9504  cnvepnep  9505  inf2  9520  inf3lem6  9530  infeq5i  9533  zfinf2  9539  cantnflt  9569  cnfcom  9597  trcl  9625  tz9.1c  9627  tc2  9637  r1funlim  9666  r1fnon  9667  karden  9795  tskwe  9850  cardprclem  9879  pm54.43  9901  r0weon  9910  iunmapdisj  9921  alephfnon  9963  alephfplem4  10005  alephfp  10006  alephval3  10008  kmlem2  10050  dju1dif  10071  ackbij1  10135  ackbij2lem2  10137  ackbij2  10140  infpssrlem3  10203  hsmexlem4  10327  hsmexlem5  10328  ac2  10359  axac3  10362  ac6  10378  axdclem2  10418  dmct  10422  ondomon  10461  alephsucpw  10468  pwcfsdom  10481  cfpwsdom  10482  smobeth  10484  axpowndlem3  10497  zfcndun  10513  zfcndpow  10514  zfcndinf  10516  zfcndac  10517  wunex2  10636  uniwun  10638  wuncval2  10645  grur1  10718  axgroth5  10722  axgroth2  10723  axgroth6  10726  axgroth3  10729  grothtsk  10733  inaprc  10734  ltsopi  10786  dmaddpi  10788  dmmulpi  10789  1lt2pi  10803  nqerf  10828  addnqf  10846  mulnqf  10847  1lt2nq  10871  m1p1sr  10990  m1m1sr  10991  0lt1sr  10993  axaddf  11043  axmulf  11044  ax1cn  11047  subaddrii  11457  ixi  11753  recgt0ii  12035  nn1suc  12154  4div2e2  12297  arch  12385  un0mulcl  12422  pnf0xnn0  12468  3halfnz  12558  nummac  12639  indstr  12816  mnfltpnf  13027  ioof  13349  0nelfz1  13445  fzp1disj  13485  fzp1nel  13513  fzof  13558  fvf1tp  13695  om2uzrani  13861  om2uzf1oi  13862  uzrdglem  13866  uzrdgfni  13867  uzrdg0i  13868  ltwenn  13871  hashgf1o  13880  axdc4uzlem  13892  sq0  14101  irec  14110  facmapnn  14194  hashkf  14241  hashfxnn0  14246  hashf  14247  hash0  14276  prhash2ex  14308  hashsslei  14335  hashxplem  14342  hashbclem  14361  hashf1lem1  14364  tpf1ofv0  14405  tpfo  14409  s1dm  14518  eqs1  14522  ccat2s1p1  14539  cats1un  14630  revs1  14674  0csh0  14702  cshw1  14731  cats1fvn  14767  funcnvs1  14821  pfx2  14856  relexp0g  14931  relexpsucnnr  14934  rtrclreclem1  14966  dfrtrclrec2  14967  rtrclreclem2  14968  rtrclreclem4  14970  dfrtrcl2  14971  climmo  15466  fsumcom2  15683  ackbijnn  15737  incexclem  15745  infcvgaux1i  15766  fprodcom2  15893  bpolylem  15957  bpoly3  15967  bpoly4  15968  efcvgfsum  15995  cos1bnd  16098  cos2bnd  16099  znnen  16123  qnnen  16124  aleph1re  16156  3dvds  16244  n2dvdsm1  16282  divalglem5  16310  flodddiv4  16328  sadcaddlem  16370  sadadd2lem  16372  sadadd3  16374  sadaddlem  16379  lcmf0  16547  lcmfunsnlem2lem1  16551  lcmfunsnlem2  16553  coprmprod  16574  coprmproddvdslem  16575  2prm  16605  3lcm2e6  16645  phicl2  16681  pockthi  16821  unbenlem  16822  prmrec  16836  vdwlem13  16907  vdwnn  16912  ramcl2  16930  prmgapprmo  16976  mod2xnegi  16985  modsubi  16986  structcnvcnv  17066  strleun  17070  setsres  17091  strfv  17116  starvndxnbasendx  17210  starvndxnplusgndx  17211  starvndxnmulrndx  17212  scandxnbasendx  17222  scandxnplusgndx  17223  scandxnmulrndx  17224  vscandxnbasendx  17227  vscandxnplusgndx  17228  vscandxnmulrndx  17229  vscandxnscandx  17230  ipndxnbasendx  17238  ipndxnplusgndx  17239  ipndxnmulrndx  17240  slotsdifipndx  17241  tsetndxnplusgndx  17263  tsetndxnmulrndx  17264  tsetndxnstarvndx  17265  slotstnscsi  17266  plendxnplusgndx  17277  plendxnmulrndx  17278  plendxnscandx  17279  plendxnvscandx  17280  slotsdifplendx  17281  basendxnocndx  17289  plendxnocndx  17290  dsndxnplusgndx  17296  dsndxnmulrndx  17297  slotsdnscsi  17298  dsndxntsetndx  17299  slotsdifdsndx  17300  unifndxntsetndx  17306  slotsdifunifndx  17307  slotsdifplendx2  17322  slotsdifocndx  17323  0rest  17335  firest  17338  restid  17339  prdsval  17361  prdsbas  17363  prdsplusg  17364  prdsmulr  17365  prdsvsca  17366  imasaddfnlem  17434  imasvscafn  17443  2oppchomf  17632  0ssc  17746  0subcat  17747  idfucl  17790  homarel  17945  dmaf  17958  cdaf  17959  setc2ohom  18004  catcfuccl  18027  relxpchom  18089  catcxpccl  18115  oppchofcl  18168  oyoncl  18178  letsr  18501  nulchn  18527  s1chn  18528  chnub  18530  chninf  18543  ex-chn1  18545  mgmidmo  18570  efmndmgm  18795  smndex1ibas  18810  smndex1mgm  18817  smndex1mnd  18820  smndex2dbas  18824  smndex2dnrinv  18825  smndex2hbas  18826  pwmnd  18847  releqg  19089  ga0  19212  psgnunilem3  19410  psgnunilem4  19411  pmtrsn  19433  efgval  19631  efger  19632  efgsval2  19647  efgsp1  19651  efgsfo  19653  efgredleme  19657  efgredlem  19661  efgred  19662  cygctb  19806  gsum2d2lem  19887  gsum2d2  19888  gsumcom2  19889  dprd2d2  19960  pgpfaclem1  19997  gsumle  20059  reldvdsr  20280  fldhmsubc  20702  00lsp  20916  cnfldfun  21307  cnfldfunALT  21308  cnfldfunOLD  21320  cnfldfunALTOLD  21321  xrsmgm  21345  pzriprnglem8  21427  pzriprnglem13  21432  pzriprnglem14  21433  pzriprngALT  21434  resubdrg  21547  ocv0  21616  cssval  21621  islinds2  21752  psrvscafval  21887  psrbag0  21998  psdmvr  22085  00ply1bas  22153  ply1plusgfvi  22155  m2detleib  22547  tgdom  22894  tgidm  22896  indistps2ALT  22930  restbas  23074  resttopon  23077  rest0  23085  leordtval2  23128  iocpnfordt  23131  icomnfordt  23132  iooordt  23133  ist1-3  23265  1stcfb  23361  comppfsc  23448  1stckgen  23470  ptbasfi  23497  dfac14  23534  opnfbas  23758  hauspwpwf1  23903  alexsubALT  23967  ptcmplem5  23972  cnextrel  23979  ust0  24136  0met  24282  prdsdsf  24283  prdsxmetlem  24284  prdsmet  24286  prdsbl  24407  qtopbaslem  24674  xrtgioo  24723  xrsdsre  24727  zcld  24730  recld2  24731  reperflem  24735  retopconn  24746  iccpnfcnv  24870  bndth  24885  nmoleub2lem2  25044  zclmncvs  25076  recmet  25251  resscdrg  25286  ishl2  25298  recms  25308  volf  25458  iundisj2  25478  volsup  25485  icombl  25493  ioombl  25494  ismbf3d  25583  0plef  25601  0pledm  25602  itg1ge0  25615  mbfi1fseqlem5  25648  itg2addlem  25687  reldv  25799  limciun  25823  dvexp  25885  dveflem  25911  lhop1lem  25946  lhop  25949  elply2  26129  elplyd  26135  ply1term  26137  ply0  26141  plymullem  26149  qaa  26259  pserulm  26359  pserdvlem2  26366  efcn  26381  sincosq1lem  26434  tangtx  26442  sincos4thpi  26450  pigt3  26455  pige3ALT  26457  efif1olem4  26482  logf1o  26501  relogf1o  26503  log1  26522  loge  26523  logi  26524  relogiso  26535  dvrelog  26574  relogcn  26575  logcn  26584  cxpcn3  26686  resqrtcn  26687  rtprmirr  26698  2logb9irr  26733  leibpi  26880  log2ublem1  26884  birthday  26892  emcllem5  26938  harmonicbnd  26942  harmonicbnd2  26943  harmonicbnd3  26946  lgamgulm2  26974  lgamcvglem  26978  gamf  26981  ppiltx  27115  ppiublem1  27141  ppiub  27143  bclbnd  27219  bpos1lem  27221  bposlem8  27230  lgsquadlem2  27320  2sqlem9  27366  2sqlem10  27367  addsqnreup  27382  chebbnd1  27411  selberg2lem  27489  pntrsumo1  27504  selbergsb  27514  pntpbnd  27527  sltval2  27596  noxp1o  27603  nosepnelem  27619  noetasuplem2  27674  noetainflem2  27678  0slt1s  27774  addsf  27926  precsexlem1  28146  precsexlem2  28147  precsexlem3  28148  precsexlem4  28149  precsexlem5  28150  precsexlem9  28154  precsexlem10  28155  precsexlem11  28156  elons2  28196  onscutlt  28202  onsiso  28206  onswe  28207  onsse  28208  onaddscl  28211  onmulscl  28212  eln0s  28288  0zs  28313  zseo  28346  twocut  28347  lngndxnitvndx  28422  istrkg2ld  28439  tgcgr4  28510  ax5seglem7  28915  axlowdimlem4  28925  axlowdimlem6  28927  axlowdimlem7  28928  axlowdimlem10  28931  axlowdimlem13  28934  axlowdimlem16  28937  uhgr0e  29051  uhgr0  29053  upgrbi  29073  umgrbi  29081  usgr0  29223  lfuhgr1v0e  29234  usgrexmpllem  29240  usgrexmpl  29243  griedg0prc  29244  cplgr0  29405  usgrexilem  29420  cffldtocusgr  29427  cffldtocusgrOLD  29428  rgrusgrprc  29570  rusgrprc  29571  rgrprcx  29573  rgrx0ndm  29574  usgr2pthlem  29743  pthdlem2  29748  uspgrn2crct  29788  wwlksnext  29873  clwwlknondisj  30093  0ewlk  30096  0wlk  30098  0pth  30107  1pthdlem1  30117  1trld  30124  wlk2v2elem2  30138  wlk2v2e  30139  upgr3v3e3cycl  30162  upgr4cycl4dv4e  30167  dfconngr1  30170  0conngr  30174  konigsbergumgr  30233  2wspmdisj  30319  2clwwlk2clwwlk  30332  numclwwlk3lem2lem  30365  numclwwlk3lem2  30366  ex-dif  30405  ex-in  30407  ex-eprel  30415  ex-id  30416  ex-fl  30429  ex-mod  30431  ex-hash  30435  ex-fpar  30444  avril1  30445  2bornot2b  30446  0vfval  30588  vsfval  30615  ajmoi  30840  ajfuni  30841  normlem2  31093  norm3adifii  31130  hhip  31159  hlim0  31217  hlimcaui  31218  hlimf  31219  hhssnv  31246  shscli  31299  shsval2i  31369  h1de2i  31535  fh3i  31605  fh4i  31606  cm2mi  31608  qlaxr3i  31618  mayetes3i  31711  ho0f  31733  hoif  31736  hodidi  31769  ho0subi  31777  hosd1i  31804  adjmo  31814  nmopsetn0  31847  nmfnsetn0  31860  funadj  31868  funcnvadj  31875  nmcexi  32008  cnlnadjlem8  32056  nmoptri2i  32081  opsqrlem4  32125  hmopidmchi  32133  pjoci  32162  pjinvari  32173  abrexdomjm  32489  elim2ifim  32527  iundisj2f  32572  rinvf1o  32614  dfcnv2  32660  snct  32699  fzodif2  32778  iundisj2fi  32784  dp2lt10  32871  dp2ltc  32874  dplti  32892  dpgti  32893  dpexpp1  32895  xrge0slmod  33320  isconstr  33770  zarcls  33908  zartopn  33909  xrge0pluscn  33974  qqhre  34054  esumrnmpt2  34102  esumfsup  34104  esumpcvgval  34112  hasheuni  34119  esumcvg  34120  esumcvgsum  34122  esumsup  34123  esum2d  34127  dmsigagen  34178  ldgenpisyslem3  34199  measvuni  34248  voliune  34263  volfiniune  34264  br2base  34303  dya2iocuni  34317  eulerpartlem1  34401  eulerpartlemt  34405  eulerpartgbij  34406  fib0  34433  coinfliprv  34517  ballotlem2  34523  ballotlemic  34541  ballotlem7  34570  ballotth  34572  plymul02  34580  rpsqrtcn  34627  chtvalz  34663  circlemethnat  34675  circlevma  34676  circlemethhgt  34677  hgt750lem  34685  bnj226  34767  bnj1101  34817  bnj110  34891  bnj149  34908  bnj150  34909  bnj151  34910  bnj517  34918  bnj580  34946  bnj865  34956  bnj900  34962  bnj996  34989  bnj1110  35015  bnj1133  35022  bnj1128  35023  bnj1145  35026  bnj1137  35028  bnj1171  35033  bnj1176  35038  setinds2regs  35150  tz9.1regs  35151  fineqvnttrclse  35165  f1resfz0f1d  35179  subfacp1lem5  35249  subfacp1lem6  35250  kur14lem9  35279  cvmcov2  35340  cvmliftlem1  35350  cvmliftlem4  35353  cvmliftlem5  35354  gonanegoal  35417  satfv0  35423  satfv0fun  35436  fmlan0  35456  gonan0  35457  fmla0disjsuc  35463  ex-sategoelel12  35492  msrfo  35611  problem5  35734  brtpid1  35786  brtpid2  35787  brtpid3  35788  faclimlem1  35808  axextndbi  35867  txprel  35942  relsset  35951  relbigcup  35960  fvbigcup  35965  fnsingle  35982  fvsingle  35983  snelsingles  35985  funimage  35991  fullfunfnv  36011  imagesset  36018  funtransport  36096  colinrel  36122  funray  36205  funline  36207  0hf  36242  neibastop2lem  36425  filnetlem3  36445  nrmo  36475  waj-ax  36479  lukshef-ax2  36480  arg-ax  36481  limsucncmpi  36510  dnizeq0  36540  knoppcnlem8  36565  knoppcnlem11  36568  cnndvlem1  36602  bj-babylob  36669  bj-ax12ssb  36723  bj-nnfnth  36808  bj-snsetex  37028  bj-0eltag  37043  bj-2upln0  37088  bj-2upln1upl  37089  bj-snexg  37099  bj-unexg  37103  bj-adjg1  37108  f1omptsnlem  37401  f1omptsn  37402  icoreresf  37417  relowlssretop  37428  relowlpssretop  37429  domalom  37469  matunitlindf  37678  poimirlem3  37683  poimirlem9  37689  poimirlem16  37696  poimirlem17  37697  poimirlem18  37698  poimirlem19  37699  poimirlem20  37700  poimirlem26  37706  mblfinlem1  37717  mblfinlem2  37718  ismblfin  37721  voliunnfl  37724  cnambfre  37728  abrexdom  37790  fdc  37805  cncfres  37825  heibor1lem  37869  grposnOLD  37942  bicontr  38140  an12i  38158  tsim1  38190  ac6s6f  38233  vvdifopab  38317  brcnvrabga  38394  opabf  38420  xrnrel  38426  dmsucmap  38501  mopre  38504  relcoels  38546  cnvcosseq  38559  refrelcoss3  38585  refrelcoss2  38586  symrelcoss2  38588  refrelcoss  38635  symrelcoss  38676  n0eldmqs  38765  ax13fromc9  39025  dedths  39081  renegclALT  39082  12gcd5e1  42116  60gcd7e1  42118  lcmineqlem23  42164  dvrelog2  42177  dvrelog3  42178  dvrelog2b  42179  aks4d1p1p6  42186  aks4d1p1p7  42187  aks4d1p1  42189  sticksstones22  42281  sn-axprlem3  42335  acos1half  42476  moxfr  42809  mapfzcons1  42834  diophrw  42876  0dioph  42895  vdioph  42896  rabren3dioph  42932  2nn0ind  43062  rpnnen3  43149  kelac2lem  43181  frlmpwfi  43215  oaordnrex  43412  omnord1ex  43421  oenord1ex  43432  oaomoencom  43434  ifpbiidcor2  43600  iscard4  43650  sqrtcval  43758  resqrtvalex  43762  eliunov2  43796  xphe  43898  0he  43899  he0  43901  snhesn  43903  idhe  43904  frege54cor1c  44032  clsk1independent  44163  neicvgnvor  44233  amgm2d  44315  amgm3d  44316  amgm4d  44317  ismnushort  44418  lhe4.4ex1a  44446  rusbcALT  44555  ipo0  44565  ifr0  44566  vk15.4j  44645  2sb5nd  44677  dfvd1ir  44690  dfvd2anir  44701  dfvd2ir  44703  dfvd3ir  44710  dfvd3anir  44713  iden2  44731  e0bir  44893  uun2221p1  44930  uun2221p2  44931  2sb5ndVD  45026  2sb5ndALT  45048  iunconnlem2  45051  trwf  45076  wfaxext  45110  wfaxpow  45114  wfaxinf2  45118  wfac8prim  45119  permaxinf2lem  45129  nregmodelf1o  45132  fnchoice  45150  unisn0  45175  eliincex  45231  icof  45340  fnmptif  45386  supminfxr  45586  rexanuz2nf  45614  fsumiunss  45699  climlimsupcex  45891  liminfltlimsupex  45903  liminflelimsupcex  45919  xlimrel  45942  xlimfun  45977  resincncf  45997  dvnprodlem3  46070  volioc  46094  volico  46105  dmvolss  46107  volioof  46109  stoweidlem13  46135  stoweidlem34  46156  stirlinglem5  46200  stirlinglem13  46208  stirlingr  46212  fourierdlem42  46271  fourierdlem62  46290  fouriersw  46353  etransc  46405  salexct  46456  salexct2  46461  salgencntex  46465  sge0rnn0  46490  gsumge0cl  46493  sge00  46498  sge0resplit  46528  sge0reuz  46569  omeiunle  46639  0ome  46651  icoresmbl  46665  ovn0lem  46687  ovnhoilem1  46723  hspmbl  46751  nsssmfmbf  46901  mbfpsssmf  46905  smfresal  46910  smfmullem4  46916  smfpimbor1lem1  46920  smfpimbor1lem2  46921  nthrucw  47008  lambert0  47011  lamberte  47012  cjnpoly  47013  tannpoly  47014  sinnpoly  47015  aistia  47021  aisfina  47022  aiffnbandciffatnotciffb  47028  axorbciffatcxorb  47029  abnotbtaxb  47039  abnotataxb  47040  eusnsn  47150  aiotaval  47219  aiota0ndef  47221  fundcmpsurinjimaid  47535  ichv  47573  ichf  47574  ichid  47575  icht  47576  ichcircshi  47578  icheq  47586  spr0nelg  47600  m3prm  47716  m7prm  47724  0noddALTV  47813  2noddALTV  47817  341fppr2  47858  9fppr8  47861  nfermltl8rev  47866  nfermltl2rev  47867  nfermltlrev  47868  sbgoldbo  47911  nnsum3primes4  47912  evengpop3  47922  stgr1  48085  usgrexmpl1lem  48145  usgrexmpl1  48146  usgrexmpl1tri  48149  usgrexmpl2lem  48150  usgrexmpl2  48151  usgrexmpl2nb0  48155  usgrexmpl2nb1  48156  usgrexmpl2nb2  48157  usgrexmpl2nb3  48158  usgrexmpl2nb4  48159  usgrexmpl2nb5  48160  gpgedg2ov  48190  gpgedg2iv  48191  gpg5nbgrvtx03starlem1  48192  gpg5nbgrvtx03starlem2  48193  gpg5nbgrvtx03starlem3  48194  gpg5nbgrvtx13starlem1  48195  gpg5nbgrvtx13starlem2  48196  gpg5nbgrvtx13starlem3  48197  gpg5grlim  48217  gpg5grlic  48218  gpgprismgr4cycllem2  48220  gpgprismgr4cycllem7  48225  pg4cyclnex  48251  gpg5edgnedg  48254  grlimedgnedg  48255  oddinmgm  48299  nn0mnd  48303  2zrngamgm  48369  2zrngaabl  48374  2zrngmmgm  48376  2zrngnring  48382  fldhmsubcALTV  48457  eliunxp2  48458  zlmodzxzldeplem  48623  zlmodzxzldep  48629  ldepslinc  48634  rrx2xpreen  48844  rrx2plordisom  48848  line2ylem  48876  line2  48877  line2x  48879  inlinecirc02plem  48911  mosn  48937  mof0  48962  mof0ALT  48964  tposrescnv  49003  tposres3  49005  tposideq2  49013  f1omoOLD  49018  nelsubc3  49196  reldmxpc  49371  reldmprcof1  49506  setc1onsubc  49727  reldmlmd2  49778  reldmcmd2  49779  rellmd  49784  relcmd  49785  ex-gte  49854  empty-surprise  49907  eximp-surprise2  49910  amgmw2d  49929