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

This proof depends on syntax axioms:   ↔ wb 209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210

This theorem is used by:  pm5.74ri  275  con4bii  324  imnani  406  mpbir2an  724  imorri  869  orri  876  mpbir3an  1360  xorexmid  1557  tru  1574  had1  1633  had0  1634  had1OLD  1635  nic-mpALT  1705  nic-ax  1706  nic-axALT  1707  nfi  1821  mpgbir  1832  nfxfr  1886  19.35ri  1912  ax5e  1945  ax6ev  2002  sbt  2103  equsb1v  2142  ax13  2404  ax13ALT  2454  moanmo  2647  axi12  2730  axbnd  2731  axexte  2733  axextmo  2736  nulmo  2737  vexw  2744  eqeltri  2856  nfcxfr  2920  neir  2958  neirr  2964  eqnetri  3025  nelir  3064  mprgbir  3083  issetri  3469  moeq  3665  rmoeq  3696  cdeqi  3723  eqsstri  3977  vn0OLD  4292  rmo0  4310  ab0orv  4332  rab0  4335  rabnc  4341  reuprg  4664  tpid1  4729  tpid2  4731  mosneq  4802  pwv  4864  uni0OLD  4897  int0  4922  eqbrtri  5126  tr0  5225  trv  5226  zfrep4  5248  axnulALT  5261  0ex  5264  inex1  5280  elpwi2  5300  0elpw  5320  axpow2  5332  dvdemo1  5338  vpwex  5342  zfpair2  5399  prex  5403  exss  5438  brv  5448  opwo0id  5474  moop2  5479  0sn0ep  5559  po0  5580  epse  5637  relxp  5673  rel0  5779  relopabiv  5801  relopabi  5803  relopabiALT  5804  eliunxp  5817  opeliunxp2  5818  dmi  5905  dmep  5907  xpidtr  6116  xpima  6175  dmsn0  6205  cnvsn0  6206  0elon  6413  funmpt  6571  funmpt2  6572  funcnv0  6599  isarep2  6622  fresaunres2  6747  f0  6756  f10d  6852  f1o00  6853  f1oi  6856  f1oiOLD  6857  f1osn  6859  brprcneu  6868  brprcneuALT  6869  opabiotafun  6958  fvopab3ig  6982  opabex  7219  eufnfv  7228  isof1oopb  7326  ncanth  7368  mpofun  7537  reldmmpo  7547  ovid  7554  ovidig  7555  ovidi  7556  ovig  7559  ov3  7576  caovmo  7651  relmptopab  7664  porpss  7728  uniex2  7739  uniex2OLD  7740  tfinds2  7860  finds  7893  finds2  7895  oprabex  7973  oprabex3  7974  f1stres  8010  f2ndres  8011  relmpoopab  8091  fsplitfpar  8115  poseq  8156  opeliunxp2f  8208  tpos0  8254  issmo  8337  tfrlem6OLD  8371  tfrlem8  8373  tfrlem16  8382  tfr1a  8383  tfr1  8386  tz7.44lem1  8394  seqomlem2  8440  seqomlem3  8441  seqomlem4  8442  fnseqom  8444  ord3  8471  0lt1o  8491  0we1  8493  naddf  8670  eqer  8733  ecopover  8821  mapsnf1o3  8902  ssdomg  9006  en0  9024  en0r  9026  ensn1  9027  0fi  9049  enrefnn  9053  xpcomf1o  9064  map2xp  9145  limensuci  9151  1sdom2  9218  sdom1  9220  unblem4  9265  fidomdm  9301  marypha1lem  9403  hartogslem1  9514  hartogs  9516  card2on  9526  nelaneqOLDOLD  9576  epinid0  9577  ruALT  9581  disjcsn  9582  elnanel  9586  cnvepnep  9587  inf2  9602  inf3lem6  9612  infeq5i  9615  zfinf2  9621  cantnflt  9651  cnfcom  9679  trcl  9707  tz9.1c  9709  tc2  9719  r1funlim  9748  r1fnon  9749  karden  9898  kardenOLD  9899  tskwe  9955  cardprclem  9984  pm54.43  10006  r0weon  10015  iunmapdisj  10026  alephfnon  10068  alephfplem4  10110  alephfp  10111  alephval3  10113  kmlem2  10154  dju1dif  10175  ackbij1  10239  ackbij2lem2  10241  ackbij2  10244  infpssrlem3  10307  hsmexlem4  10431  hsmexlem5  10432  ac2  10463  axac3  10466  ac6  10482  axdclem2  10522  dmct  10526  dmctOLD  10527  ondomon  10571  alephsucpw  10579  pwcfsdom  10592  cfpwsdom  10593  smobeth  10595  axpowndlem3  10608  zfcndun  10624  zfcndpow  10625  zfcndinf  10627  zfcndac  10628  wunex2  10747  uniwun  10749  wuncval2  10756  grur1  10829  axgroth5  10833  axgroth2  10834  axgroth6  10837  axgroth3  10840  grothtsk  10844  inaprc  10845  ltsopi  10897  dmaddpi  10899  dmmulpi  10900  1lt2pi  10914  nqerf  10939  addnqf  10957  mulnqf  10958  1lt2nq  10982  m1p1sr  11101  m1m1sr  11102  0lt1sr  11104  axaddf  11154  axmulf  11155  ax1cn  11158  subaddrii  11571  ixi  11867  recgt0ii  12145  nn1suc  12279  4div2e2  12436  arch  12525  un0mulcl  12562  pnf0xnn0  12608  3halfnz  12700  nummac  12786  indstr  12965  mnfltpnf  13177  ioof  13500  0nelfz1  13597  fzp1disj  13638  fzp1nel  13666  fzof  13711  f1resfz0f1d  13848  fvf1tp  13850  om2uzrani  14016  om2uzf1oi  14017  uzrdglem  14021  uzrdgfni  14022  uzrdg0i  14023  ltwenn  14026  hashgf1o  14035  axdc4uzlem  14047  sq0  14256  irec  14265  facmapnn  14349  hashkf  14396  hashfxnn0  14401  hashf  14402  hash0  14431  prhash2ex  14463  hashsslei  14491  hashxplem  14498  hashbclem  14517  hashf1lem1  14520  tpf1ofv0  14561  tpfo  14565  s1dm  14675  eqs1  14680  ccat2s1p1  14697  cats1un  14790  revs1  14834  0csh0  14864  cshw1  14893  cats1fvn  14929  funcnvs1  14983  pfx2  15018  relexp0g  15095  relexpsucnnr  15098  rtrclreclem1  15130  dfrtrclrec2  15131  rtrclreclem2  15132  rtrclreclem4  15134  dfrtrcl2  15135  climmo  15644  fsumcom2  15860  ackbijnn  15917  incexclem  15925  infcvgaux1i  15946  fprodcom2  16071  bpolylem  16134  bpoly3  16144  bpoly4  16145  efcvgfsum  16172  cos1bnd  16275  cos2bnd  16276  znnen  16300  qnnen  16301  aleph1re  16333  3dvds  16421  n2dvdsm1  16459  divalglem5  16487  flodddiv4  16505  sadcaddlem  16547  sadadd2lem  16549  sadadd3  16551  sadaddlem  16556  lcmf0  16724  lcmfunsnlem2lem1  16728  lcmfunsnlem2  16730  coprmprod  16751  coprmproddvdslem  16752  2prm  16782  3lcm2e6  16823  phicl2  16859  pockthi  16999  unbenlem  17000  prmrec  17014  vdwlem13  17085  vdwnn  17090  ramcl2  17108  prmgapprmo  17154  mod2xnegi  17163  modsubi  17164  structcnvcnv  17245  strleun  17249  setsres  17270  strfv  17295  starvndxnbasendx  17389  starvndxnplusgndx  17390  starvndxnmulrndx  17391  scandxnbasendx  17401  scandxnplusgndx  17402  scandxnmulrndx  17403  vscandxnbasendx  17406  vscandxnplusgndx  17407  vscandxnmulrndx  17408  vscandxnscandx  17409  ipndxnbasendx  17417  ipndxnplusgndx  17418  ipndxnmulrndx  17419  slotsdifipndx  17420  tsetndxnplusgndx  17442  tsetndxnmulrndx  17443  tsetndxnstarvndx  17444  slotstnscsi  17445  plendxnplusgndx  17456  plendxnmulrndx  17457  plendxnscandx  17458  plendxnvscandx  17459  slotsdifplendx  17460  basendxnocndx  17468  plendxnocndx  17469  dsndxnplusgndx  17475  dsndxnmulrndx  17476  slotsdnscsi  17477  dsndxntsetndx  17478  slotsdifdsndx  17479  unifndxntsetndx  17485  slotsdifunifndx  17486  slotsdifplendx2  17501  slotsdifocndx  17502  0rest  17514  firest  17517  restid  17518  prdsval  17540  prdsbas  17542  prdsplusg  17543  prdsmulr  17544  prdsvsca  17545  imasaddfnlem  17614  imasvscafn  17623  2oppchomf  17812  0ssc  17926  0subcat  17927  idfucl  17970  homarel  18125  dmaf  18138  cdaf  18139  setc2ohom  18184  catcfuccl  18207  relxpchom  18269  catcxpccl  18295  oppchofcl  18348  oyoncl  18358  letsr  18681  nulchn  18707  s1chn  18708  chnub  18710  chninf  18723  ex-chn1  18725  mgmidmo  18752  efmndmgm  18994  smndex1ibas  19009  smndex1mgm  19019  smndex1mnd  19022  smndex2dbas  19026  smndex2dnrinv  19027  smndex2hbas  19028  degenmgm  19050  degenmgm2nfun  19052  degenmgm2  19053  pwmnd  19056  releqg  19298  ga0  19425  psgnunilem3  19623  psgnunilem4  19624  pmtrsn  19646  efgval  19844  efger  19845  efgsval2  19860  efgsp1  19864  efgsfo  19866  efgredleme  19870  efgredlem  19874  efgred  19875  cygctb  20019  gsum2d2lem  20100  gsum2d2  20101  gsumcom2  20102  dprd2d2  20173  pgpfaclem1  20210  gsumle  20272  reldvdsr  20501  fldhmsubc  20951  00lsp  21165  cnfldfun  21599  cnfldfunALT  21600  xrsmgm  21620  pzriprnglem8  21701  pzriprnglem13  21706  pzriprnglem14  21707  pzriprngALT  21708  resubdrg  21821  ocv0  21890  cssval  21895  islinds2  22026  psrvscafval  22163  psrbag0  22278  psdmvr  22397  00ply1bas  22464  ply1plusgfvi  22466  m2detleib  22853  matunitlindf  22903  tgdom  23203  tgidm  23205  indistps2ALT  23239  restbas  23383  resttopon  23386  rest0  23394  leordtval2  23437  iocpnfordt  23440  icomnfordt  23441  iooordt  23442  ist1-3  23574  1stcfb  23670  comppfsc  23758  1stckgen  23780  ptbasfi  23807  dfac14  23844  opnfbas  24068  hauspwpwf1  24213  alexsubALT  24277  ptcmplem5  24282  cnextrel  24289  ust0  24446  0met  24592  prdsdsf  24593  prdsxmetlem  24594  prdsmet  24596  prdsbl  24717  qtopbaslem  24984  xrtgioo  25033  xrsdsre  25037  zcld  25040  recld2  25041  reperflem  25045  retopconn  25056  iccpnfcnv  25172  bndth  25186  nmoleub2lem2  25344  zclmncvs  25376  recmet  25551  resscdrg  25586  ishl2  25598  recms  25608  volf  25757  iundisj2  25777  volsup  25784  icombl  25792  ioombl  25793  ismbf3d  25882  0plef  25900  0pledm  25901  itg1ge0  25914  mbfi1fseqlem5  25947  itg2addlem  25986  reldv  26097  limciun  26121  dvexp  26180  dveflem  26206  lhop1lem  26240  lhop  26243  elply2  26421  elplyd  26427  ply1term  26429  ply0  26433  plymullem  26442  plymul02  26510  qaa  26556  pserulm  26658  pserdvlem2  26664  efcn  26679  sincosq1lem  26735  tangtx  26743  sincos4thpi  26751  pigt3  26755  pige3ALT  26757  efif1olem4  26782  logf1o  26801  relogf1o  26803  log1  26822  loge  26823  logi  26824  relogiso  26835  dvrelog  26874  relogcn  26875  logcn  26884  cxpcn3  26985  resqrtcn  26986  rtprmirr  26997  2logb9irr  27032  leibpi  27179  log2ublem1  27183  birthday  27191  emcllem5  27236  harmonicbnd  27240  harmonicbnd2  27241  harmonicbnd3  27244  lgamgulm2  27272  lgamcvglem  27276  gamf  27279  ppiltx  27413  ppiublem1  27438  ppiub  27440  bclbnd  27516  bpos1lem  27518  bposlem8  27527  lgsquadlem2  27617  2sqlem9  27663  2sqlem10  27664  addsqnreup  27679  chebbnd1  27708  selberg2lem  27786  pntrsumo1  27801  selbergsb  27811  pntpbnd  27824  ltsval2  27892  noxp1o  27899  nosepnelem  27915  noetasuplem2  27970  noetainflem2  27974  0lt1s  28077  addsf  28247  precsexlem1  28472  precsexlem2  28473  precsexlem3  28474  precsexlem4  28475  precsexlem5  28476  precsexlem9  28480  precsexlem10  28481  precsexlem11  28482  elons2  28523  oncutlt  28529  oniso  28536  onswe  28537  onsse  28538  onaddscl  28542  onmulscl  28543  onsbnd  28546  eln0s  28626  0zs  28653  zseo  28687  twocut  28688  0reno  28761  1reno  28762  lngndxnitvndx  28784  istrkg2ld  28801  tgcgr4  28873  ax5seglem7  29392  axlowdimlem4  29402  axlowdimlem6  29404  axlowdimlem7  29405  axlowdimlem10  29408  axlowdimlem13  29411  axlowdimlem16  29414  uhgr0e  29528  uhgr0  29530  upgrbi  29550  umgrbi  29558  usgr0  29703  lfuhgr1v0e  29714  usgrexmpllem  29720  usgrexmpl  29723  griedg0prc  29724  cplgr0  29885  usgrexilem  29900  cffldtocusgr  29907  rgrusgrprc  30049  rusgrprc  30050  rgrprcx  30052  rgrx0ndm  30053  usgr2pthlem  30228  pthdlem2  30233  uspgrn2crct  30276  wwlksnext  30361  clwwlknondisj  30581  0ewlk  30584  0wlk  30586  0pth  30595  1pthdlem1  30605  1trld  30612  wlk2v2elem2  30636  wlk2v2e  30637  upgr3v3e3cycl  30660  upgr4cycl4dv4e  30665  dfconngr1  30668  0conngr  30672  konigsbergumgr  30731  2wspmdisj  30817  2clwwlk2clwwlk  30830  numclwwlk3lem2lem  30863  numclwwlk3lem2  30864  ex-dif  30903  ex-in  30905  ex-eprel  30913  ex-id  30914  ex-fl  30927  ex-mod  30929  ex-hash  30933  ex-fpar  30942  avril1  30943  2bornot2b  30944  0vfval  31087  vsfval  31114  ajmoi  31339  ajfuni  31340  normlem2  31592  norm3adifii  31629  hhip  31658  hlim0  31716  hlimcaui  31717  hlimf  31718  hhssnv  31745  shscli  31798  shsval2i  31868  h1de2i  32034  fh3i  32104  fh4i  32105  cm2mi  32107  qlaxr3i  32117  mayetes3i  32210  ho0f  32232  hoif  32235  hodidi  32268  ho0subi  32276  hosd1i  32303  adjmo  32313  nmopsetn0  32346  nmfnsetn0  32359  funadj  32367  funcnvadj  32374  nmcexi  32507  cnlnadjlem8  32555  nmoptri2i  32580  opsqrlem4  32624  hmopidmchi  32632  pjoci  32661  pjinvari  32672  abrexdomjm  32982  elim2ifim  33020  iundisj2f  33063  rinvf1o  33103  dfcnv2  33148  snct  33184  fzodif2  33262  iundisj2fi  33268  dp2lt10  33329  dp2ltc  33332  dplti  33350  dpgti  33351  dpexpp1  33353  xrge0slmod  33788  isconstr  34246  zarcls  34384  zartopn  34385  xrge0pluscn  34450  qqhre  34530  esumrnmpt2  34578  esumfsup  34580  esumpcvgval  34588  hasheuni  34595  esumcvg  34596  esumcvgsum  34598  esumsup  34599  esum2d  34603  dmsigagen  34655  ldgenpisyslem3  34676  measvuni  34725  voliune  34740  volfiniune  34741  br2base  34780  dya2iocuni  34794  eulerpartlem1  34878  eulerpartlemt  34882  eulerpartgbij  34883  fib0  34910  coinfliprv  34994  ballotlem2  35000  ballotlemic  35018  ballotlem7  35047  ballotth  35049  rpsqrtcn  35101  chtvalz  35137  circlemethnat  35149  circlevma  35150  circlemethhgt  35151  hgt750lem  35159  bnj226  35244  bnj1101  35294  bnj110  35367  bnj149  35384  bnj150  35385  bnj151  35386  bnj517  35394  bnj580  35422  bnj865  35432  bnj900  35438  bnj996  35465  bnj1110  35491  bnj1133  35498  bnj1128  35499  bnj1145  35502  bnj1137  35504  bnj1171  35509  bnj1176  35514  axnulALT2  35590  fineqvnttrclse  35650  setinds2regs  35657  tz9.1regs  35660  subfacp1lem5  35763  subfacp1lem6  35764  kur14lem9  35793  cvmcov2  35854  cvmliftlem1  35864  cvmliftlem4  35867  cvmliftlem5  35868  gonanegoal  35931  satfv0  35937  satfv0fun  35950  fmlan0  35970  gonan0  35971  fmla0disjsuc  35977  ex-sategoelel12  36006  msrfo  36125  problem5  36248  brtpid1  36300  brtpid2  36301  brtpid3  36302  faclimlem1  36322  axextndbi  36381  txprel  36456  relsset  36465  relbigcup  36474  fvbigcup  36479  fnsingle  36496  fvsingle  36497  snelsingles  36499  funimage  36505  fullfunfnv  36525  imagesset  36532  funtransport  36611  colinrel  36637  funray  36720  funline  36722  0hf  36757  nmulr0  36775  neibastop2lem  36979  filnetlem3  36999  nrmo  37029  waj-ax  37033  lukshef-ax2  37034  arg-ax  37035  limsucncmpi  37064  ttctr  37112  dfttc2g  37125  ttcuniun  37129  ttcuni  37132  dfttc4lem2  37148  regsfromregtco  37157  dnizeq0  37172  knoppcnlem8  37197  knoppcnlem11  37200  cnndvlem1  37234  bj-babylob  37305  bj-ax12ssb  37388  bj-nnfnth  37484  bj-snsetex  37707  bj-0eltag  37722  bj-2upln0  37767  bj-2upln1upl  37768  bj-snexg  37778  bj-unexg  37782  bj-adjg1  37787  bj-axseprep  37819  f1omptsnlem  38090  f1omptsn  38091  icoreresf  38106  relowlssretop  38117  relowlpssretop  38118  domalom  38158  poimirlem3  38372  poimirlem9  38378  poimirlem16  38385  poimirlem17  38386  poimirlem18  38387  poimirlem19  38388  poimirlem20  38389  poimirlem26  38395  mblfinlem1  38406  mblfinlem2  38407  ismblfin  38410  voliunnfl  38413  cnambfre  38417  abrexdom  38480  fdc  38495  cncfres  38515  heibor1lem  38559  grposnOLD  38632  bicontr  38830  an12i  38846  tsim1  38878  ac6s6f  38921  vvdifopab  39013  brcnvrabga  39090  opabf  39124  xrnrel  39130  relqmap  39200  dmsucmap  39216  mopre  39219  relcoels  39262  cnvcosseq  39275  refrelcoss3  39301  refrelcoss2  39302  symrelcoss2  39304  refrelcoss  39351  symrelcoss  39392  n0eldmqs  39480  ax13fromc9  39779  dedths  39835  renegclALT  39836  12gcd5e1  42869  60gcd7e1  42871  lcmineqlem23  42917  dvrelog2  42930  dvrelog3  42931  dvrelog2b  42932  aks4d1p1p6  42939  aks4d1p1p7  42940  aks4d1p1  42942  sticksstones22  43034  25or6to4  43072  sn-axprlem3  43088  acos1half  43233  moxfr  43537  mapfzcons1  43562  diophrw  43604  0dioph  43623  vdioph  43624  rabren3dioph  43656  2nn0ind  43786  rpnnen3  43873  kelac2lem  43905  frlmpwfi  43939  oaordnrex  44136  omnord1ex  44145  oenord1ex  44156  oaomoencom  44158  ifpbiidcor2  44323  iscard4  44373  sqrtcval  44481  resqrtvalex  44485  eliunov2  44519  xphe  44621  0he  44622  he0  44624  snhesn  44626  idhe  44627  frege54cor1c  44755  clsk1independent  44886  neicvgnvor  44956  amgm2d  45038  amgm3d  45039  amgm4d  45040  ismnushort  45125  lhe4.4ex1a  45153  rusbcALT  45262  ipo0  45272  ifr0  45273  vk15.4j  45351  2sb5nd  45383  dfvd1ir  45396  dfvd2anir  45407  dfvd2ir  45409  dfvd3ir  45416  dfvd3anir  45419  iden2  45437  e0bir  45599  uun2221p1  45636  uun2221p2  45637  2sb5ndVD  45732  2sb5ndALT  45754  iunconnlem2  45757  trwf  45782  wfaxext  45816  wfaxpow  45820  wfaxinf2  45824  wfac8prim  45825  permaxinf2lem  45835  nregmodelf1o  45838  fnchoice  45863  unisn0  45888  eliincex  45942  icof  46049  fnmptif  46094  supminfxr  46292  rexanuz2nf  46320  fsumiunss  46405  climlimsupcex  46597  liminfltlimsupex  46609  liminflelimsupcex  46625  xlimrel  46648  xlimfun  46683  resincncf  46703  dvnprodlem3  46776  volioc  46800  volico  46811  dmvolss  46813  volioof  46815  stoweidlem13  46841  stoweidlem34  46862  stirlinglem5  46906  stirlinglem13  46914  stirlingr  46918  fourierdlem42  46977  fourierdlem62  46996  fouriersw  47059  etransc  47111  salexct  47162  salexct2  47167  salgencntex  47171  sge0rnn0  47196  gsumge0cl  47199  sge00  47204  sge0resplit  47234  sge0reuz  47275  omeiunle  47345  0ome  47357  icoresmbl  47371  ovn0lem  47393  ovnhoilem1  47429  hspmbl  47457  nsssmfmbf  47607  mbfpsssmf  47611  smfresal  47616  smfmullem4  47622  smfpimbor1lem1  47626  smfpimbor1lem2  47627  quantgodel  47702  numtowerdt  47734  goldratmolem2  47751  goldratmolem3  47752  goldratval  47754  lambert0  47755  lamberte  47756  cjnpoly  47757  aistia  47785  aisfina  47786  aiffnbandciffatnotciffb  47792  axorbciffatcxorb  47793  abnotbtaxb  47803  abnotataxb  47804  eusnsn  47914  aiotaval  47983  aiota0ndef  47985  fundcmpsurinjimaid  48311  ichv  48349  ichf  48350  ichid  48351  icht  48352  ichcircshi  48354  icheq  48362  spr0nelg  48376  m3prm  48495  m7prm  48503  0noddALTV  48605  2noddALTV  48609  341fppr2  48650  9fppr8  48653  nfermltl8rev  48658  nfermltl2rev  48659  nfermltlrev  48660  sbgoldbo  48703  nnsum3primes4  48704  evengpop3  48714  stgr1  48877  usgrexmpl1lem  48937  usgrexmpl1  48938  usgrexmpl1tri  48941  usgrexmpl2lem  48942  usgrexmpl2  48943  usgrexmpl2nb0  48947  usgrexmpl2nb1  48948  usgrexmpl2nb2  48949  usgrexmpl2nb3  48950  usgrexmpl2nb4  48951  usgrexmpl2nb5  48952  gpgedg2ov  48982  gpgedg2iv  48983  gpg5nbgrvtx03starlem1  48984  gpg5nbgrvtx03starlem2  48985  gpg5nbgrvtx03starlem3  48986  gpg5nbgrvtx13starlem1  48987  gpg5nbgrvtx13starlem2  48988  gpg5nbgrvtx13starlem3  48989  gpg5grlim  49009  gpg5grlic  49010  gpgprismgr4cycllem2  49012  gpgprismgr4cycllem7  49017  pg4cyclnex  49043  gpg5edgnedg  49046  grlimedgnedg  49047  oddinmgm  49090  nn0mnd  49094  2zrngamgm  49160  2zrngaabl  49165  2zrngmmgm  49167  2zrngnring  49173  fldhmsubcALTV  49248  eliunxp2  49264  zlmodzxzldeplem  49428  zlmodzxzldep  49434  ldepslinc  49439  rrx2xpreen  49649  rrx2plordisom  49653  line2ylem  49681  line2  49682  line2x  49684  inlinecirc02plem  49716  mosn  49741  mof0  49766  mof0ALT  49768  tposrescnv  49805  tposres3  49807  tposideq2  49815  f1omoOLD  49820  nelsubc3  49997  reldmxpc  50172  reldmprcof1  50307  setc1onsubc  50528  reldmlmd2  50579  reldmcmd2  50580  rellmd  50585  relcmd  50586  ex-gte  50655  dvsec  50689  dvcsc  50690  dvcot  50691  empty-surprise  50711  eximp-surprise2  50714  amgmw2d  50822