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  1556  tru  1573  had1  1632  had0  1633  had1OLD  1634  nic-mpALT  1704  nic-ax  1705  nic-axALT  1706  nfi  1820  mpgbir  1831  nfxfr  1885  19.35ri  1911  ax5e  1944  ax6ev  2001  sbt  2102  equsb1v  2141  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  3664  rmoeq  3695  cdeqi  3722  eqsstri  3955  vn0OLD  4291  rmo0  4309  ab0orv  4331  rab0  4334  rabnc  4340  pwv  4574  reuprg  4660  tpid1  4725  tpid2  4727  mosneq  4796  uni0OLD  4896  int0  4921  eqbrtri  5125  tr0  5224  trv  5225  zfrep4  5245  axnulALT  5257  0ex  5260  inex1  5277  elpwi2  5297  0elpw  5317  axpow2  5329  dvdemo1  5335  vpwex  5339  zfpair2  5392  prex  5396  exss  5431  brv  5441  opwo0id  5469  moop2  5474  0sn0ep  5555  po0  5576  epse  5633  relxp  5669  rel0  5777  relopabiv  5799  relopabi  5801  relopabiALT  5802  eliunxp  5815  opeliunxp2  5816  dmi  5904  dmep  5906  relres  5997  xpidtr  6118  xpima  6176  imadifssrn  6204  dmsn0  6213  cnvsn0  6214  0elon  6421  funmpt  6583  funmpt2  6584  funcnv0  6611  isarep2  6634  fresaunres2  6759  f0  6768  f10d  6864  f1o00  6865  f1oi  6868  f1oiOLD  6869  f1osn  6871  brprcneu  6880  brprcneuALT  6881  opabiotafun  6970  fvopab3ig  6994  opabex  7230  eufnfv  7239  isof1oopb  7337  ncanth  7379  mpofun  7548  reldmmpo  7558  ovid  7565  ovidig  7566  ovidi  7567  ovig  7570  ov3  7587  caovmo  7662  relmptopab  7675  funmpt3  7691  mpt3fvd  7692  porpss  7747  uniex2  7758  uniex2OLD  7759  tfinds2  7879  finds  7912  finds2  7914  oprabex  7992  oprabex3  7993  f1stres  8029  f2ndres  8030  relmpoopab  8110  fsplitfpar  8135  poseq  8181  opeliunxp2f  8234  tpos0  8280  issmo  8363  tfrlem6OLD  8397  tfrlem8  8399  tfrlem16  8408  tfr1a  8409  tfr1  8412  tz7.44lem1  8420  seqomlem2  8468  seqomlem3  8469  seqomlem4  8470  fnseqom  8472  ord3  8499  0lt1o  8519  0we1  8521  naddf  8698  eqer  8761  ecopover  8849  mapsnf1o3  8930  ssdomg  9034  en0  9052  en0r  9054  ensn1  9055  0fi  9077  enrefnn  9081  xpcomf1o  9092  map2xp  9173  limensuci  9179  1sdom2  9246  sdom1  9248  unblem4  9294  fidomdm  9330  marypha1lem  9432  hartogslem1  9543  hartogs  9545  card2on  9555  nelaneqOLDOLD  9605  epinid0  9606  ruALT  9610  disjcsn  9611  elnanel  9615  cnvepnep  9616  inf2  9631  inf3lem6  9641  infeq5i  9644  zfinf2  9650  cantnflt  9680  cnfcom  9708  trcl  9736  tz9.1c  9738  tc2  9748  r1funlimOLD  9777  r1fun  9778  r1dmlim  9779  r1fnon  9780  0hf  9924  karden  9966  kardenOLD  9967  tskwe  10038  cardprclem  10067  pm54.43  10089  r0weon  10098  iunmapdisj  10109  alephfnon  10151  alephfplem4  10193  alephfp  10194  alephval3  10196  kmlem2  10237  dju1dif  10258  ackbij1  10322  ackbij2lem2  10324  ackbij2  10327  infpssrlem3  10390  hsmexlem4  10514  hsmexlem5  10515  ac2  10546  axac3  10549  ac6  10565  axdclem2  10605  dmct  10609  dmctOLD  10610  ondomon  10654  alephsucpw  10662  pwcfsdom  10675  cfpwsdom  10676  smobeth  10678  axpowndlem3  10691  zfcndun  10707  zfcndpow  10708  zfcndinf  10710  zfcndac  10711  wunex2  10830  uniwun  10832  wuncval2  10839  grur1  10912  axgroth5  10916  axgroth2  10917  axgroth6  10920  axgroth3  10923  grothtsk  10927  inaprc  10928  ltsopi  10980  dmaddpi  10982  dmmulpi  10983  1lt2pi  10997  nqerf  11022  addnqf  11040  mulnqf  11041  1lt2nq  11065  m1p1sr  11184  m1m1sr  11185  0lt1sr  11187  axaddf  11237  axmulf  11238  ax1cn  11241  subaddrii  11654  ixi  11952  recgt0ii  12230  nn1suc  12364  4div2e2  12521  arch  12610  un0mulcl  12647  pnf0xnn0  12693  3halfnz  12785  nummac  12871  indstr  13050  mnfltpnf  13262  ioof  13585  0nelfz1  13683  fzp1disj  13724  fzp1nel  13752  fzof  13797  f1resfz0f1d  13934  fvf1tp  13936  om2uzrani  14102  om2uzf1oi  14103  uzrdglem  14107  uzrdgfni  14108  uzrdg0i  14109  ltwenn  14112  hashgf1o  14121  axdc4uzlem  14133  sq0  14342  irec  14352  facmapnn  14436  hashkf  14483  hashfxnn0  14488  hashf  14489  hash0  14518  prhash2ex  14550  hashsslei  14578  hashxplem  14585  hashbclem  14604  hashf1lem1  14607  tpf1ofv0  14648  tpfo  14652  s1dm  14762  eqs1  14768  ccat2s1p1  14785  cats1un  14878  revs1  14922  0csh0  14952  cshw1  14981  cats1fvn  15017  funcnvs1  15072  pfx2  15107  relexp0g  15184  relexpsucnnr  15187  rtrclreclem1  15219  dfrtrclrec2  15220  rtrclreclem2  15221  rtrclreclem4  15223  dfrtrcl2  15224  climmo  15733  fsumcom2  15949  ackbijnn  16006  incexclem  16014  infcvgaux1i  16035  fprodcom2  16160  bpolylem  16223  bpoly3  16233  bpoly4  16234  efcvgfsum  16261  cos1bnd  16364  cos2bnd  16365  znnen  16389  qnnen  16390  aleph1re  16422  3dvds  16510  n2dvdsm1  16548  divalglem5  16576  flodddiv4  16594  sadcaddlem  16636  sadadd2lem  16638  sadadd3  16640  sadaddlem  16645  lcmf0  16818  lcmfunsnlem2lem1  16822  lcmfunsnlem2  16824  coprmprod  16845  coprmproddvdslem  16846  2prm  16876  3lcm2e6  16917  phicl2  16954  pockthi  17094  unbenlem  17095  prmrec  17109  vdwlem13  17180  vdwnn  17185  ramcl2  17203  prmgapprmo  17249  mod2xnegi  17258  modsubi  17259  structcnvcnv  17340  strleun  17344  setsres  17365  strfv  17390  starvndxnbasendx  17484  starvndxnplusgndx  17485  starvndxnmulrndx  17486  scandxnbasendx  17496  scandxnplusgndx  17497  scandxnmulrndx  17498  vscandxnbasendx  17501  vscandxnplusgndx  17502  vscandxnmulrndx  17503  vscandxnscandx  17504  ipndxnbasendx  17512  ipndxnplusgndx  17513  ipndxnmulrndx  17514  slotsdifipndx  17515  tsetndxnplusgndx  17537  tsetndxnmulrndx  17538  tsetndxnstarvndx  17539  slotstnscsi  17540  plendxnplusgndx  17551  plendxnmulrndx  17552  plendxnscandx  17553  plendxnvscandx  17554  slotsdifplendx  17555  basendxnocndx  17563  plendxnocndx  17564  dsndxnplusgndx  17570  dsndxnmulrndx  17571  slotsdnscsi  17572  dsndxntsetndx  17573  slotsdifdsndx  17574  unifndxntsetndx  17580  slotsdifunifndx  17581  slotsdifplendx2  17596  slotsdifocndx  17597  0rest  17609  firest  17612  restid  17613  prdsval  17635  prdsbas  17637  prdsplusg  17638  prdsmulr  17639  prdsvsca  17640  imasaddfnlem  17709  imasvscafn  17718  2oppchomf  17907  0ssc  18021  0subcat  18022  idfucl  18065  homarel  18220  dmaf  18233  cdaf  18234  setc2ohom  18279  catcfuccl  18302  relxpchom  18364  catcxpccl  18390  oppchofcl  18443  oyoncl  18453  letsr  18776  nulchn  18802  s1chn  18803  chnub  18805  chninf  18818  ex-chn1  18820  mgmidmo  18847  efmndmgm  19090  smndex1ibas  19105  smndex1mgm  19115  smndex1mnd  19118  smndex2dbas  19122  smndex2dnrinv  19123  smndex2hbas  19124  degenmgm  19146  degenmgm2nfun  19148  degenmgm2  19149  pwmnd  19152  releqg  19394  ga0  19521  psgnunilem3  19719  psgnunilem4  19720  pmtrsn  19742  efgval  19940  efger  19941  efgsval2  19956  efgsp1  19960  efgsfo  19962  efgredleme  19966  efgredlem  19970  efgred  19971  cygctb  20115  gsum2d2lem  20196  gsum2d2  20197  gsumcom2  20198  dprd2d2  20269  pgpfaclem1  20306  gsumle  20368  reldvdsr  20599  fldhmsubc  21051  00lsp  21265  cnfldfun  21701  cnfldfunALT  21702  xrsmgm  21722  pzriprnglem8  21803  pzriprnglem13  21808  pzriprnglem14  21809  pzriprngALT  21810  resubdrg  21923  ocv0  21992  cssval  21997  islinds2  22128  psrvscafval  22265  psrbag0  22380  psdmvr  22499  00ply1bas  22566  ply1plusgfvi  22568  m2detleib  22955  matunitlindf  23005  tgdom  23305  tgidm  23307  indistps2ALT  23341  restbas  23485  resttopon  23488  rest0  23496  leordtval2  23539  iocpnfordt  23542  icomnfordt  23543  iooordt  23544  ist1-3  23676  1stcfb  23772  comppfsc  23860  1stckgen  23882  ptbasfi  23909  dfac14  23946  opnfbas  24170  hauspwpwf1  24315  alexsubALT  24379  ptcmplem5  24384  cnextrel  24391  ust0  24548  0met  24694  prdsdsf  24695  prdsxmetlem  24696  prdsmet  24698  prdsbl  24819  qtopbaslem  25086  xrtgioo  25135  xrsdsre  25139  zcld  25142  recld2  25143  reperflem  25147  retopconn  25158  iccpnfcnv  25274  bndth  25288  nmoleub2lem2  25446  zclmncvs  25478  recmet  25653  resscdrg  25688  ishl2  25700  recms  25710  volf  25859  iundisj2  25879  volsup  25886  icombl  25894  ioombl  25895  ismbf3d  25984  0plef  26002  0pledm  26003  itg1ge0  26016  mbfi1fseqlem5  26049  itg2addlem  26088  reldv  26199  limciun  26223  dvexp  26282  dveflem  26308  lhop1lem  26342  lhop  26345  elply2  26523  elplyd  26529  ply1term  26531  ply0  26535  plymullem  26544  plymul02  26610  qaa  26656  pserulm  26758  pserdvlem2  26764  efcn  26779  sincosq1lem  26835  tangtx  26843  sincos4thpi  26851  pigt3  26855  pige3ALT  26857  efif1olem4  26882  logf1o  26901  relogf1o  26903  log1  26922  loge  26923  logi  26924  relogiso  26935  dvrelog  26974  relogcn  26975  logcn  26984  cxpcn3  27085  resqrtcn  27086  rtprmirr  27097  2logb9irr  27132  leibpi  27279  log2ublem1  27283  birthday  27291  emcllem5  27336  harmonicbnd  27340  harmonicbnd2  27341  harmonicbnd3  27344  lgamgulm2  27372  lgamcvglem  27376  gamf  27379  ppiltx  27513  ppiublem1  27538  ppiub  27540  bclbnd  27616  bpos1lem  27618  bposlem8  27627  lgsquadlem2  27717  2sqlem9  27763  2sqlem10  27764  addsqnreup  27779  chebbnd1  27808  selberg2lem  27886  pntrsumo1  27901  selbergsb  27911  pntpbnd  27924  ltsval2  28022  noxp1o  28029  nosepnelem  28045  noetasuplem2  28100  noetainflem2  28104  0lt1s  28207  addsf  28377  precsexlem1  28602  precsexlem2  28603  precsexlem3  28604  precsexlem4  28605  precsexlem5  28606  precsexlem9  28610  precsexlem10  28611  precsexlem11  28612  elons2  28653  oncutlt  28659  oniso  28666  onswe  28667  onsse  28668  onaddscl  28672  onmulscl  28673  onsbnd  28676  eln0s  28756  0zs  28783  zseo  28817  twocut  28818  0reno  28891  1reno  28892  lngndxnitvndx  28914  istrkg2ld  28931  tgcgr4  29003  ax5seglem7  29522  axlowdimlem4  29532  axlowdimlem6  29534  axlowdimlem7  29535  axlowdimlem10  29538  axlowdimlem13  29541  axlowdimlem16  29544  uhgr0e  29658  uhgr0  29660  upgrbi  29680  umgrbi  29688  usgr0  29833  lfuhgr1v0e  29844  usgrexmpllem  29850  usgrexmpl  29853  griedg0prc  29854  cplgr0  30015  usgrexilem  30030  cffldtocusgr  30037  rgrusgrprc  30179  rusgrprc  30180  rgrprcx  30182  rgrx0ndm  30183  usgr2pthlem  30358  pthdlem2  30363  uspgrn2crct  30406  wwlksnext  30491  clwwlknondisj  30711  0ewlk  30714  0wlk  30716  0pth  30725  1pthdlem1  30735  1trld  30742  wlk2v2elem2  30766  wlk2v2e  30767  upgr3v3e3cycl  30790  upgr4cycl4dv4e  30795  dfconngr1  30798  0conngr  30802  konigsbergumgr  30861  2wspmdisj  30947  2clwwlk2clwwlk  30960  numclwwlk3lem2lem  30993  numclwwlk3lem2  30994  ex-dif  31033  ex-in  31035  ex-eprel  31043  ex-id  31044  ex-fl  31057  ex-mod  31059  ex-hash  31063  ex-fpar  31072  avril1  31073  2bornot2b  31074  0vfval  31217  vsfval  31244  ajmoi  31469  ajfuni  31470  normlem2  31722  norm3adifii  31759  hhip  31788  hlim0  31846  hlimcaui  31847  hlimf  31848  hhssnv  31875  shscli  31928  shsval2i  31998  h1de2i  32164  fh3i  32234  fh4i  32235  cm2mi  32237  qlaxr3i  32247  mayetes3i  32340  ho0f  32362  hoif  32365  hodidi  32398  ho0subi  32406  hosd1i  32433  adjmo  32443  nmopsetn0  32476  nmfnsetn0  32489  funadj  32497  funcnvadj  32504  nmcexi  32637  cnlnadjlem8  32685  nmoptri2i  32710  opsqrlem4  32754  hmopidmchi  32762  pjoci  32791  pjinvari  32802  abrexdomjm  33154  elim2ifim  33192  iundisj2f  33235  rinvf1o  33275  dfcnv2  33320  snct  33356  fzodif2  33433  iundisj2fi  33439  dp2lt10  33500  dp2ltc  33503  dplti  33521  dpgti  33522  dpexpp1  33524  xrge0slmod  33959  isconstr  34418  zarcls  34556  zartopn  34557  xrge0pluscn  34622  qqhre  34702  esumrnmpt2  34750  esumfsup  34752  esumpcvgval  34760  hasheuni  34767  esumcvg  34768  esumcvgsum  34770  esumsup  34771  esum2d  34775  dmsigagen  34827  ldgenpisyslem3  34848  measvuni  34897  voliune  34912  volfiniune  34913  br2base  34951  dya2iocuni  34965  eulerpartlem1  35049  eulerpartlemt  35053  eulerpartgbij  35054  fib0  35081  coinfliprv  35165  ballotlem2  35171  ballotlemic  35189  ballotlem7  35218  ballotth  35220  rpsqrtcn  35272  chtvalz  35308  circlemethnat  35320  circlevma  35321  circlemethhgt  35322  hgt750lem  35330  bnj226  35415  bnj1101  35465  bnj110  35538  bnj149  35555  bnj150  35556  bnj151  35557  bnj517  35565  bnj580  35593  bnj865  35603  bnj900  35609  bnj996  35636  bnj1110  35662  bnj1133  35669  bnj1128  35670  bnj1145  35673  bnj1137  35675  bnj1171  35680  bnj1176  35685  axnulALT2  35764  rankse  35797  fineqvnttrclse  35852  setinds2regs  35859  tz9.1regs  35862  j0iso  35947  onprcf1acwevdlem2  35969  vsmext  36012  subfacp1lem5  36039  subfacp1lem6  36040  kur14lem9  36069  cvmcov2  36130  cvmliftlem1  36140  cvmliftlem4  36143  cvmliftlem5  36144  gonanegoal  36207  satfv0  36213  satfv0fun  36226  fmlan0  36246  gonan0  36247  fmla0disjsuc  36253  ex-sategoelel12  36282  msrfo  36401  problem5  36524  brtpid1  36582  brtpid2  36583  brtpid3  36584  faclimlem1  36604  axextndbi  36662  txprel  36737  relsset  36746  relbigcup  36755  fvbigcup  36760  fnsingle  36777  fvsingle  36778  snelsingles  36780  funimage  36786  fullfunfnv  36806  imagesset  36813  funtransport  36892  colinrel  36918  funray  37001  funline  37003  nmulr0  37040  neibastop2lem  37244  filnetlem3  37264  nrmo  37294  waj-ax  37298  lukshef-ax2  37299  arg-ax  37300  limsucncmpi  37329  ttctr  37377  dfttc2g  37390  ttcuniun  37394  ttcuni  37397  dfttc4lem2  37413  regsfromregtco  37422  dnizeq0  37437  knoppcnlem8  37462  knoppcnlem11  37465  cnndvlem1  37499  bj-babylob  37570  bj-ax12ssb  37653  bj-nnfnth  37749  bj-snsetex  37972  bj-0eltag  37987  bj-2upln0  38032  bj-2upln1upl  38033  bj-snexg  38043  bj-unexg  38047  bj-adjg1  38052  bj-axseprep  38098  f1omptsnlem  38368  f1omptsn  38369  icoreresf  38384  relowlssretop  38395  relowlpssretop  38396  domalom  38436  poimirlem3  38650  poimirlem9  38656  poimirlem16  38663  poimirlem17  38664  poimirlem18  38665  poimirlem19  38666  poimirlem20  38667  poimirlem26  38673  mblfinlem1  38684  mblfinlem2  38685  ismblfin  38688  voliunnfl  38691  cnambfre  38695  abrexdom  38773  fdc  38788  cncfres  38808  heibor1lem  38852  grposnOLD  38925  bicontr  39123  an12i  39139  tsim1  39171  ac6s6f  39214  vvdifopab  39306  brcnvrabga  39383  opabf  39417  xrnrel  39423  relqmap  39493  dmsucmap  39509  mopre  39512  relcoels  39555  cnvcosseq  39568  refrelcoss3  39594  refrelcoss2  39595  symrelcoss2  39597  refrelcoss  39644  symrelcoss  39685  n0eldmqs  39773  ax13fromc9  40072  dedths  40128  renegclALT  40129  12gcd5e1  43162  60gcd7e1  43164  lcmineqlem23  43210  dvrelog2  43223  dvrelog3  43224  dvrelog2b  43225  aks4d1p1p6  43232  aks4d1p1p7  43233  aks4d1p1  43235  sticksstones22  43327  25or6to4  43365  sn-axprlem3  43381  acos1half  43518  omexcn  43810  moxfr  43812  mapfzcons1  43837  diophrw  43879  0dioph  43898  vdioph  43899  rabren3dioph  43931  2nn0ind  44061  rpnnen3  44148  kelac2lem  44175  frlmpwfi  44209  oaordnrex  44406  omnord1ex  44415  oenord1ex  44426  oaomoencom  44428  ifpbiidcor2  44593  iscard4  44643  sqrtcval  44750  resqrtvalex  44754  eliunov2  44788  xphe  44890  0he  44891  he0  44893  snhesn  44895  idhe  44896  frege54cor1c  45024  clsk1independent  45155  neicvgnvor  45225  amgm2d  45307  amgm3d  45308  amgm4d  45309  ismnushort  45394  lhe4.4ex1a  45422  rusbcALT  45530  ipo0  45540  ifr0  45541  vk15.4j  45619  2sb5nd  45651  dfvd1ir  45664  dfvd2anir  45675  dfvd2ir  45677  dfvd3ir  45684  dfvd3anir  45687  iden2  45705  e0bir  45867  uun2221p1  45904  uun2221p2  45905  2sb5ndVD  46000  2sb5ndALT  46022  iunconnlem2  46025  trwf  46057  wfaxext  46091  wfaxpow  46095  wfaxinf2  46099  wfac8prim  46100  permaxinf2lem  46110  nregmodelf1o  46113  fnchoice  46154  unisn0  46179  eliincex  46233  icof  46340  fnmptif  46385  supminfxr  46582  rexanuz2nf  46610  fsumiunss  46695  climlimsupcex  46887  liminfltlimsupex  46899  liminflelimsupcex  46915  xlimrel  46938  xlimfun  46973  resincncf  46993  dvnprodlem3  47066  volioc  47090  volico  47101  dmvolss  47103  volioof  47105  stoweidlem13  47131  stoweidlem34  47152  stirlinglem5  47196  stirlinglem13  47204  stirlingr  47208  fourierdlem42  47267  fourierdlem62  47286  fouriersw  47349  etransc  47401  salexct  47452  salexct2  47457  salgencntex  47461  sge0rnn0  47486  gsumge0cl  47489  sge00  47494  sge0resplit  47524  sge0reuz  47565  omeiunle  47635  0ome  47647  icoresmbl  47661  ovn0lem  47683  ovnhoilem1  47719  hspmbl  47747  nsssmfmbf  47897  mbfpsssmf  47901  smfresal  47906  smfmullem4  47912  smfpimbor1lem1  47916  smfpimbor1lem2  47917  quantgodel  47992  numtowerdt  48024  goldratmolem2  48041  goldratmolem3  48042  goldratval  48044  lambert0  48045  lamberte  48046  cjnpoly  48047  aistia  48075  aisfina  48076  aiffnbandciffatnotciffb  48082  axorbciffatcxorb  48083  abnotbtaxb  48093  abnotataxb  48094  eusnsn  48204  aiotaval  48273  aiota0ndef  48275  fundcmpsurinjimaid  48601  ichv  48639  ichf  48640  ichid  48641  icht  48642  ichcircshi  48644  icheq  48652  spr0nelg  48666  m3prm  48785  m7prm  48793  0noddALTV  48895  2noddALTV  48899  341fppr2  48940  9fppr8  48943  nfermltl8rev  48948  nfermltl2rev  48949  nfermltlrev  48950  sbgoldbo  48993  nnsum3primes4  48994  evengpop3  49004  stgr1  49167  usgrexmpl1lem  49227  usgrexmpl1  49228  usgrexmpl1tri  49231  usgrexmpl2lem  49232  usgrexmpl2  49233  usgrexmpl2nb0  49237  usgrexmpl2nb1  49238  usgrexmpl2nb2  49239  usgrexmpl2nb3  49240  usgrexmpl2nb4  49241  usgrexmpl2nb5  49242  gpgedg2ov  49272  gpgedg2iv  49273  gpg5nbgrvtx03starlem1  49274  gpg5nbgrvtx03starlem2  49275  gpg5nbgrvtx03starlem3  49276  gpg5nbgrvtx13starlem1  49277  gpg5nbgrvtx13starlem2  49278  gpg5nbgrvtx13starlem3  49279  gpg5grlim  49299  gpg5grlic  49300  gpgprismgr4cycllem2  49302  gpgprismgr4cycllem7  49307  pg4cyclnex  49333  gpg5edgnedg  49336  grlimedgnedg  49337  oddinmgm  49380  nn0mnd  49384  2zrngamgm  49450  2zrngaabl  49455  2zrngmmgm  49457  2zrngnring  49463  fldhmsubcALTV  49538  eliunxp2  49554  zlmodzxzldeplem  49718  zlmodzxzldep  49724  ldepslinc  49729  rrx2xpreen  49940  rrx2plordisom  49944  line2ylem  49971  line2  49972  mosn  50032  mof0  50057  mof0ALT  50059  tposrescnv  50100  tposres3  50102  tposideq2  50110  f1omoOLD  50116  nelsubc3  50293  reldmxpc  50476  fucoisfunc  50595  fucoisfunc2lem1  50596  reldmprcof1  50624  setc1onsubc  50848  reldmlmd2  50944  reldmcmd2  50945  rellmd  50950  relcmd  50951  ex-gte  51005  dvsec  51039  dvcsc  51040  dvcot  51041  empty-surprise  51061  eximp-surprise2  51064  amgmw2d  51172