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 ⊢ 𝜑

Syntax hints:   ↔ wb 209

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 210

This theorem is referenced by:  pm5.74ri  275  con4bii  324  imnani  405  mpbir2an  723  imorri  868  orri  875  mpbir3an  1358  xorexmid  1554  tru  1571  had1  1630  nic-mpALT  1699  nic-ax  1700  nic-axALT  1701  nfi  1815  mpgbir  1826  nfxfr  1880  19.35ri  1906  ax5e  1939  ax6ev  1996  sbt  2102  equsb1v  2146  ax13  2413  ax13ALT  2463  moanmo  2656  axi12  2739  axbnd  2740  axexte  2742  axextmo  2745  nulmo  2746  vexw  2753  eqeltri  2865  nfcxfr  2929  neir  2967  neirr  2973  eqnetri  3034  nelir  3073  mprgbir  3092  issetri  3482  moeq  3679  rmoeq  3710  cdeqi  3737  eqsstri  3991  vn0  4306  rmo0  4324  ab0orv  4345  rab0  4348  rabnc  4354  reuprg  4671  tpid1  4736  tpid2  4738  mosneq  4808  pwv  4870  uni0OLD  4903  int0  4928  eqbrtri  5133  tr0  5232  trv  5233  zfrep4  5255  axnulALT  5266  0ex  5269  inex1  5285  elpwi2  5303  0elpw  5324  axpow2  5336  dvdemo1  5342  vpwex  5346  zfpair2  5403  prex  5407  exss  5442  brv  5452  opwo0id  5478  moop2  5483  0sn0ep  5563  po0  5584  epse  5641  relxp  5677  rel0  5783  relopabiv  5805  relopabi  5807  relopabiALT  5808  eliunxp  5821  opeliunxp2  5822  dmi  5909  dmep  5911  xpidtr  6120  xpima  6178  dmsn0  6208  cnvsn0  6209  0elon  6414  funmpt  6572  funmpt2  6573  funcnv0  6600  isarep2  6623  fresaunres2  6748  f0  6757  f10d  6853  f1o00  6854  f1oi  6857  f1oiOLD  6858  f1osn  6860  brprcneu  6869  brprcneuALT  6870  opabiotafun  6959  fvopab3ig  6983  opabex  7216  eufnfv  7225  isof1oopb  7321  ncanth  7363  mpofun  7532  reldmmpo  7542  ovid  7549  ovidig  7550  ovidi  7551  ovig  7554  ov3  7571  caovmo  7645  relmptopab  7658  porpss  7722  uniex2  7733  tfinds2  7856  finds  7889  finds2  7891  oprabex  7969  oprabex3  7970  f1stres  8006  f2ndres  8007  relmpoopab  8085  fsplitfpar  8109  poseq  8150  opeliunxp2f  8202  tpos0  8248  issmo  8331  tfrlem6OLD  8365  tfrlem8  8367  tfrlem16  8376  tfr1a  8377  tfr1  8380  tz7.44lem1  8388  seqomlem2  8434  seqomlem3  8435  seqomlem4  8436  fnseqom  8438  ord3  8465  0lt1o  8485  0we1  8487  naddf  8664  eqer  8727  ecopover  8815  mapsnf1o3  8889  ssdomg  8993  en0  9011  en0r  9013  ensn1  9014  0fi  9035  enrefnn  9039  xpcomf1o  9050  map2xp  9131  limensuci  9137  1sdom2  9204  sdom1  9206  unblem4  9251  fidomdm  9287  marypha1lem  9389  hartogslem1  9500  hartogs  9502  card2on  9512  nelaneqOLDOLD  9562  epinid0  9563  ruALT  9567  disjcsn  9568  elnanel  9572  cnvepnep  9573  inf2  9588  inf3lem6  9598  infeq5i  9601  zfinf2  9607  cantnflt  9637  cnfcom  9665  trcl  9693  tz9.1c  9695  tc2  9705  r1funlim  9734  r1fnon  9735  karden  9877  tskwe  9932  cardprclem  9961  pm54.43  9983  r0weon  9992  iunmapdisj  10003  alephfnon  10045  alephfplem4  10087  alephfp  10088  alephval3  10090  kmlem2  10131  dju1dif  10152  ackbij1  10216  ackbij2lem2  10218  ackbij2  10221  infpssrlem3  10285  hsmexlem4  10409  hsmexlem5  10410  ac2  10441  axac3  10444  ac6  10460  axdclem2  10500  dmct  10504  ondomon  10543  alephsucpw  10551  pwcfsdom  10564  cfpwsdom  10565  smobeth  10567  axpowndlem3  10580  zfcndun  10596  zfcndpow  10597  zfcndinf  10599  zfcndac  10600  wunex2  10719  uniwun  10721  wuncval2  10728  grur1  10801  axgroth5  10805  axgroth2  10806  axgroth6  10809  axgroth3  10812  grothtsk  10816  inaprc  10817  ltsopi  10869  dmaddpi  10871  dmmulpi  10872  1lt2pi  10886  nqerf  10911  addnqf  10929  mulnqf  10930  1lt2nq  10954  m1p1sr  11073  m1m1sr  11074  0lt1sr  11076  axaddf  11126  axmulf  11127  ax1cn  11130  subaddrii  11543  ixi  11839  recgt0ii  12117  nn1suc  12251  4div2e2  12408  arch  12497  un0mulcl  12534  pnf0xnn0  12580  3halfnz  12671  nummac  12757  indstr  12936  mnfltpnf  13147  ioof  13470  0nelfz1  13567  fzp1disj  13607  fzp1nel  13635  fzof  13680  fvf1tp  13818  om2uzrani  13984  om2uzf1oi  13985  uzrdglem  13989  uzrdgfni  13990  uzrdg0i  13991  ltwenn  13994  hashgf1o  14003  axdc4uzlem  14015  sq0  14224  irec  14233  facmapnn  14317  hashkf  14364  hashfxnn0  14369  hashf  14370  hash0  14399  prhash2ex  14431  hashsslei  14459  hashxplem  14466  hashbclem  14485  hashf1lem1  14488  tpf1ofv0  14529  tpfo  14533  s1dm  14642  eqs1  14646  ccat2s1p1  14663  cats1un  14754  revs1  14798  0csh0  14826  cshw1  14855  cats1fvn  14891  funcnvs1  14945  pfx2  14980  relexp0g  15055  relexpsucnnr  15058  rtrclreclem1  15090  dfrtrclrec2  15091  rtrclreclem2  15092  rtrclreclem4  15094  dfrtrcl2  15095  climmo  15604  fsumcom2  15821  ackbijnn  15878  incexclem  15886  infcvgaux1i  15907  fprodcom2  16034  bpolylem  16098  bpoly3  16108  bpoly4  16109  efcvgfsum  16136  cos1bnd  16239  cos2bnd  16240  znnen  16264  qnnen  16265  aleph1re  16297  3dvds  16385  n2dvdsm1  16423  divalglem5  16451  flodddiv4  16469  sadcaddlem  16511  sadadd2lem  16513  sadadd3  16515  sadaddlem  16520  lcmf0  16688  lcmfunsnlem2lem1  16692  lcmfunsnlem2  16694  coprmprod  16715  coprmproddvdslem  16716  2prm  16746  3lcm2e6  16787  phicl2  16823  pockthi  16963  unbenlem  16964  prmrec  16978  vdwlem13  17049  vdwnn  17054  ramcl2  17072  prmgapprmo  17118  mod2xnegi  17127  modsubi  17128  structcnvcnv  17209  strleun  17213  setsres  17234  strfv  17259  starvndxnbasendx  17353  starvndxnplusgndx  17354  starvndxnmulrndx  17355  scandxnbasendx  17365  scandxnplusgndx  17366  scandxnmulrndx  17367  vscandxnbasendx  17370  vscandxnplusgndx  17371  vscandxnmulrndx  17372  vscandxnscandx  17373  ipndxnbasendx  17381  ipndxnplusgndx  17382  ipndxnmulrndx  17383  slotsdifipndx  17384  tsetndxnplusgndx  17406  tsetndxnmulrndx  17407  tsetndxnstarvndx  17408  slotstnscsi  17409  plendxnplusgndx  17420  plendxnmulrndx  17421  plendxnscandx  17422  plendxnvscandx  17423  slotsdifplendx  17424  basendxnocndx  17432  plendxnocndx  17433  dsndxnplusgndx  17439  dsndxnmulrndx  17440  slotsdnscsi  17441  dsndxntsetndx  17442  slotsdifdsndx  17443  unifndxntsetndx  17449  slotsdifunifndx  17450  slotsdifplendx2  17465  slotsdifocndx  17466  0rest  17478  firest  17481  restid  17482  prdsval  17504  prdsbas  17506  prdsplusg  17507  prdsmulr  17508  prdsvsca  17509  imasaddfnlem  17578  imasvscafn  17587  2oppchomf  17776  0ssc  17890  0subcat  17891  idfucl  17934  homarel  18089  dmaf  18102  cdaf  18103  setc2ohom  18148  catcfuccl  18171  relxpchom  18233  catcxpccl  18259  oppchofcl  18312  oyoncl  18322  letsr  18645  nulchn  18671  s1chn  18672  chnub  18674  chninf  18687  ex-chn1  18689  mgmidmo  18714  efmndmgm  18940  smndex1ibas  18955  smndex1mgm  18965  smndex1mnd  18968  smndex2dbas  18972  smndex2dnrinv  18973  smndex2hbas  18974  pwmnd  18995  releqg  19237  ga0  19364  psgnunilem3  19562  psgnunilem4  19563  pmtrsn  19585  efgval  19783  efger  19784  efgsval2  19799  efgsp1  19803  efgsfo  19805  efgredleme  19809  efgredlem  19813  efgred  19814  cygctb  19958  gsum2d2lem  20039  gsum2d2  20040  gsumcom2  20041  dprd2d2  20112  pgpfaclem1  20149  gsumle  20211  reldvdsr  20438  fldhmsubc  20862  00lsp  21076  cnfldfun  21501  cnfldfunALT  21502  xrsmgm  21522  pzriprnglem8  21603  pzriprnglem13  21608  pzriprnglem14  21609  pzriprngALT  21610  resubdrg  21723  ocv0  21792  cssval  21797  islinds2  21928  psrvscafval  22063  psrbag0  22178  psdmvr  22297  00ply1bas  22364  ply1plusgfvi  22366  m2detleib  22753  tgdom  23100  tgidm  23102  indistps2ALT  23136  restbas  23280  resttopon  23283  rest0  23291  leordtval2  23334  iocpnfordt  23337  icomnfordt  23338  iooordt  23339  ist1-3  23471  1stcfb  23567  comppfsc  23654  1stckgen  23676  ptbasfi  23703  dfac14  23740  opnfbas  23964  hauspwpwf1  24109  alexsubALT  24173  ptcmplem5  24178  cnextrel  24185  ust0  24342  0met  24488  prdsdsf  24489  prdsxmetlem  24490  prdsmet  24492  prdsbl  24613  qtopbaslem  24880  xrtgioo  24929  xrsdsre  24933  zcld  24936  recld2  24937  reperflem  24941  retopconn  24952  iccpnfcnv  25068  bndth  25082  nmoleub2lem2  25240  zclmncvs  25272  recmet  25447  resscdrg  25482  ishl2  25494  recms  25504  volf  25653  iundisj2  25673  volsup  25680  icombl  25688  ioombl  25689  ismbf3d  25778  0plef  25796  0pledm  25797  itg1ge0  25810  mbfi1fseqlem5  25843  itg2addlem  25882  reldv  25994  limciun  26018  dvexp  26077  dveflem  26103  lhop1lem  26137  lhop  26140  elply2  26318  elplyd  26324  ply1term  26326  ply0  26330  plymullem  26338  plymul02  26406  qaa  26449  pserulm  26547  pserdvlem2  26553  efcn  26568  sincosq1lem  26624  tangtx  26632  sincos4thpi  26640  pigt3  26645  pige3ALT  26647  efif1olem4  26672  logf1o  26691  relogf1o  26693  log1  26712  loge  26713  logi  26714  relogiso  26725  dvrelog  26764  relogcn  26765  logcn  26774  cxpcn3  26875  resqrtcn  26876  rtprmirr  26887  2logb9irr  26922  leibpi  27069  log2ublem1  27073  birthday  27081  emcllem5  27126  harmonicbnd  27130  harmonicbnd2  27131  harmonicbnd3  27134  lgamgulm2  27162  lgamcvglem  27166  gamf  27169  ppiltx  27303  ppiublem1  27328  ppiub  27330  bclbnd  27406  bpos1lem  27408  bposlem8  27417  lgsquadlem2  27507  2sqlem9  27553  2sqlem10  27554  addsqnreup  27569  chebbnd1  27598  selberg2lem  27676  pntrsumo1  27691  selbergsb  27701  pntpbnd  27714  ltsval2  27782  noxp1o  27789  nosepnelem  27805  noetasuplem2  27860  noetainflem2  27864  0lt1s  27967  addsf  28137  precsexlem1  28362  precsexlem2  28363  precsexlem3  28364  precsexlem4  28365  precsexlem5  28366  precsexlem9  28370  precsexlem10  28371  precsexlem11  28372  elons2  28413  oncutlt  28419  oniso  28426  onswe  28427  onsse  28428  onaddscl  28432  onmulscl  28433  onsbnd  28436  eln0s  28516  0zs  28543  zseo  28577  twocut  28578  0reno  28651  1reno  28652  lngndxnitvndx  28674  istrkg2ld  28691  tgcgr4  28762  ax5seglem7  29222  axlowdimlem4  29232  axlowdimlem6  29234  axlowdimlem7  29235  axlowdimlem10  29238  axlowdimlem13  29241  axlowdimlem16  29244  uhgr0e  29358  uhgr0  29360  upgrbi  29380  umgrbi  29388  usgr0  29530  lfuhgr1v0e  29541  usgrexmpllem  29547  usgrexmpl  29550  griedg0prc  29551  cplgr0  29712  usgrexilem  29727  cffldtocusgr  29734  rgrusgrprc  29876  rusgrprc  29877  rgrprcx  29879  rgrx0ndm  29880  usgr2pthlem  30049  pthdlem2  30054  uspgrn2crct  30094  wwlksnext  30179  clwwlknondisj  30399  0ewlk  30402  0wlk  30404  0pth  30413  1pthdlem1  30423  1trld  30430  wlk2v2elem2  30444  wlk2v2e  30445  upgr3v3e3cycl  30468  upgr4cycl4dv4e  30473  dfconngr1  30476  0conngr  30480  konigsbergumgr  30539  2wspmdisj  30625  2clwwlk2clwwlk  30638  numclwwlk3lem2lem  30671  numclwwlk3lem2  30672  ex-dif  30711  ex-in  30713  ex-eprel  30721  ex-id  30722  ex-fl  30735  ex-mod  30737  ex-hash  30741  ex-fpar  30750  avril1  30751  2bornot2b  30752  0vfval  30895  vsfval  30922  ajmoi  31147  ajfuni  31148  normlem2  31400  norm3adifii  31437  hhip  31466  hlim0  31524  hlimcaui  31525  hlimf  31526  hhssnv  31553  shscli  31606  shsval2i  31676  h1de2i  31842  fh3i  31912  fh4i  31913  cm2mi  31915  qlaxr3i  31925  mayetes3i  32018  ho0f  32040  hoif  32043  hodidi  32076  ho0subi  32084  hosd1i  32111  adjmo  32121  nmopsetn0  32154  nmfnsetn0  32167  funadj  32175  funcnvadj  32182  nmcexi  32315  cnlnadjlem8  32363  nmoptri2i  32388  opsqrlem4  32432  hmopidmchi  32440  pjoci  32469  pjinvari  32480  abrexdomjm  32790  elim2ifim  32828  iundisj2f  32872  rinvf1o  32912  dfcnv2  32957  snct  32994  fzodif2  33073  iundisj2fi  33079  dp2lt10  33140  dp2ltc  33143  dplti  33161  dpgti  33162  dpexpp1  33164  xrge0slmod  33607  isconstr  34067  zarcls  34205  zartopn  34206  xrge0pluscn  34271  qqhre  34351  esumrnmpt2  34399  esumfsup  34401  esumpcvgval  34409  hasheuni  34416  esumcvg  34417  esumcvgsum  34419  esumsup  34420  esum2d  34424  dmsigagen  34475  ldgenpisyslem3  34496  measvuni  34545  voliune  34560  volfiniune  34561  br2base  34600  dya2iocuni  34614  eulerpartlem1  34698  eulerpartlemt  34702  eulerpartgbij  34703  fib0  34730  coinfliprv  34814  ballotlem2  34820  ballotlemic  34838  ballotlem7  34867  ballotth  34869  rpsqrtcn  34921  chtvalz  34957  circlemethnat  34969  circlevma  34970  circlemethhgt  34971  hgt750lem  34979  bnj226  35064  bnj1101  35114  bnj110  35187  bnj149  35204  bnj150  35205  bnj151  35206  bnj517  35214  bnj580  35242  bnj865  35252  bnj900  35258  bnj996  35285  bnj1110  35311  bnj1133  35318  bnj1128  35319  bnj1145  35322  bnj1137  35324  bnj1171  35329  bnj1176  35334  axnulALT2  35411  fineqvnttrclse  35456  setinds2regs  35463  tz9.1regs  35466  f1resfz0f1d  35500  subfacp1lem5  35571  subfacp1lem6  35572  kur14lem9  35601  cvmcov2  35662  cvmliftlem1  35672  cvmliftlem4  35675  cvmliftlem5  35676  gonanegoal  35739  satfv0  35745  satfv0fun  35758  fmlan0  35778  gonan0  35779  fmla0disjsuc  35785  ex-sategoelel12  35814  msrfo  35933  problem5  36056  brtpid1  36108  brtpid2  36109  brtpid3  36110  faclimlem1  36130  axextndbi  36189  txprel  36264  relsset  36273  relbigcup  36282  fvbigcup  36287  fnsingle  36304  fvsingle  36305  snelsingles  36307  funimage  36313  fullfunfnv  36333  imagesset  36340  funtransport  36418  colinrel  36444  funray  36527  funline  36529  0hf  36564  nmulr0  36582  neibastop2lem  36756  filnetlem3  36776  nrmo  36806  waj-ax  36810  lukshef-ax2  36811  arg-ax  36812  limsucncmpi  36841  ttctr  36889  dfttc2g  36902  ttcuniun  36906  ttcuni  36909  dfttc4lem2  36925  regsfromregtco  36934  dnizeq0  36949  knoppcnlem8  36974  knoppcnlem11  36977  cnndvlem1  37011  bj-babylob  37082  bj-ax12ssb  37165  bj-nnfnth  37261  bj-snsetex  37483  bj-0eltag  37498  bj-2upln0  37543  bj-2upln1upl  37544  bj-snexg  37554  bj-unexg  37558  bj-adjg1  37563  bj-axseprep  37594  f1omptsnlem  37865  f1omptsn  37866  icoreresf  37881  relowlssretop  37892  relowlpssretop  37893  domalom  37933  matunitlindf  38152  poimirlem3  38157  poimirlem9  38163  poimirlem16  38170  poimirlem17  38171  poimirlem18  38172  poimirlem19  38173  poimirlem20  38174  poimirlem26  38180  mblfinlem1  38191  mblfinlem2  38192  ismblfin  38195  voliunnfl  38198  cnambfre  38202  abrexdom  38264  fdc  38279  cncfres  38299  heibor1lem  38343  grposnOLD  38416  bicontr  38614  an12i  38632  tsim1  38664  ac6s6f  38707  vvdifopab  38799  brcnvrabga  38876  opabf  38910  xrnrel  38916  relqmap  38986  dmsucmap  39002  mopre  39005  relcoels  39048  cnvcosseq  39061  refrelcoss3  39087  refrelcoss2  39088  symrelcoss2  39090  refrelcoss  39137  symrelcoss  39178  n0eldmqs  39266  ax13fromc9  39565  dedths  39621  renegclALT  39622  12gcd5e1  42655  60gcd7e1  42657  lcmineqlem23  42703  dvrelog2  42716  dvrelog3  42717  dvrelog2b  42718  aks4d1p1p6  42725  aks4d1p1p7  42726  aks4d1p1  42728  sticksstones22  42820  25or6to4  42858  sn-axprlem3  42874  acos1half  43004  moxfr  43310  mapfzcons1  43335  diophrw  43377  0dioph  43396  vdioph  43397  rabren3dioph  43429  2nn0ind  43559  rpnnen3  43646  kelac2lem  43678  frlmpwfi  43712  oaordnrex  43909  omnord1ex  43918  oenord1ex  43929  oaomoencom  43931  ifpbiidcor2  44096  iscard4  44146  sqrtcval  44254  resqrtvalex  44258  eliunov2  44292  xphe  44394  0he  44395  he0  44397  snhesn  44399  idhe  44400  frege54cor1c  44528  clsk1independent  44659  neicvgnvor  44729  amgm2d  44811  amgm3d  44812  amgm4d  44813  ismnushort  44898  lhe4.4ex1a  44926  rusbcALT  45035  ipo0  45045  ifr0  45046  vk15.4j  45124  2sb5nd  45156  dfvd1ir  45169  dfvd2anir  45180  dfvd2ir  45182  dfvd3ir  45189  dfvd3anir  45192  iden2  45210  e0bir  45372  uun2221p1  45409  uun2221p2  45410  2sb5ndVD  45505  2sb5ndALT  45527  iunconnlem2  45530  trwf  45555  wfaxext  45589  wfaxpow  45593  wfaxinf2  45597  wfac8prim  45598  permaxinf2lem  45608  nregmodelf1o  45611  fnchoice  45636  unisn0  45661  eliincex  45715  icof  45822  fnmptif  45867  supminfxr  46065  rexanuz2nf  46093  fsumiunss  46178  climlimsupcex  46370  liminfltlimsupex  46382  liminflelimsupcex  46398  xlimrel  46421  xlimfun  46456  resincncf  46476  dvnprodlem3  46549  volioc  46573  volico  46584  dmvolss  46586  volioof  46588  stoweidlem13  46614  stoweidlem34  46635  stirlinglem5  46679  stirlinglem13  46687  stirlingr  46691  fourierdlem42  46750  fourierdlem62  46769  fouriersw  46832  etransc  46884  salexct  46935  salexct2  46940  salgencntex  46944  sge0rnn0  46969  gsumge0cl  46972  sge00  46977  sge0resplit  47007  sge0reuz  47048  omeiunle  47118  0ome  47130  icoresmbl  47144  ovn0lem  47166  ovnhoilem1  47202  hspmbl  47230  nsssmfmbf  47380  mbfpsssmf  47384  smfresal  47389  smfmullem4  47395  smfpimbor1lem1  47399  smfpimbor1lem2  47400  quantgodel  47475  nthrucw  47489  goldratmolem2  47507  lambert0  47508  lamberte  47509  cjnpoly  47510  tannpoly  47511  sinnpoly  47512  aistia  47518  aisfina  47519  aiffnbandciffatnotciffb  47525  axorbciffatcxorb  47526  abnotbtaxb  47536  abnotataxb  47537  eusnsn  47647  aiotaval  47716  aiota0ndef  47718  fundcmpsurinjimaid  48044  ichv  48082  ichf  48083  ichid  48084  icht  48085  ichcircshi  48087  icheq  48095  spr0nelg  48109  m3prm  48228  m7prm  48236  0noddALTV  48338  2noddALTV  48342  341fppr2  48383  9fppr8  48386  nfermltl8rev  48391  nfermltl2rev  48392  nfermltlrev  48393  sbgoldbo  48436  nnsum3primes4  48437  evengpop3  48447  stgr1  48610  usgrexmpl1lem  48670  usgrexmpl1  48671  usgrexmpl1tri  48674  usgrexmpl2lem  48675  usgrexmpl2  48676  usgrexmpl2nb0  48680  usgrexmpl2nb1  48681  usgrexmpl2nb2  48682  usgrexmpl2nb3  48683  usgrexmpl2nb4  48684  usgrexmpl2nb5  48685  gpgedg2ov  48715  gpgedg2iv  48716  gpg5nbgrvtx03starlem1  48717  gpg5nbgrvtx03starlem2  48718  gpg5nbgrvtx03starlem3  48719  gpg5nbgrvtx13starlem1  48720  gpg5nbgrvtx13starlem2  48721  gpg5nbgrvtx13starlem3  48722  gpg5grlim  48742  gpg5grlic  48743  gpgprismgr4cycllem2  48745  gpgprismgr4cycllem7  48750  pg4cyclnex  48776  gpg5edgnedg  48779  grlimedgnedg  48780  oddinmgm  48824  nn0mnd  48828  2zrngamgm  48894  2zrngaabl  48899  2zrngmmgm  48901  2zrngnring  48907  fldhmsubcALTV  48982  eliunxp2  48994  zlmodzxzldeplem  49158  zlmodzxzldep  49164  ldepslinc  49169  rrx2xpreen  49379  rrx2plordisom  49383  line2ylem  49411  line2  49412  line2x  49414  inlinecirc02plem  49446  mosn  49471  mof0  49496  mof0ALT  49498  tposrescnv  49537  tposres3  49539  tposideq2  49547  f1omoOLD  49552  nelsubc3  49729  reldmxpc  49904  reldmprcof1  50039  setc1onsubc  50260  reldmlmd2  50311  reldmcmd2  50312  rellmd  50317  relcmd  50318  ex-gte  50387  empty-surprise  50440  eximp-surprise2  50443  amgmw2d  50473