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  710  imorri  854  orri  861  mpbir3an  1341  xorexmid  1524  tru  1541  had1  1600  nic-mpALT  1670  nic-ax  1671  nic-axALT  1672  nfi  1786  mpgbir  1797  nfxfr  1851  19.35ri  1878  ax5e  1911  ax6ev  1969  sbt  2066  equsb1v  2105  ax13  2383  ax13ALT  2433  moanmo  2625  axi12  2709  axbnd  2710  axexte  2712  axextmo  2715  nulmo  2716  vexw  2723  eqeltri  2840  nfcxfr  2906  neir  2949  neirr  2955  eqnetri  3017  nelir  3055  mprgbir  3074  cbvrexdva2OLD  3358  issetri  3507  moeq  3729  rmoeq  3760  cdeqi  3787  eqsstri  4043  3sstr4i  4052  rmo0  4385  rabnc  4414  reuprg  4728  tpid1  4793  tpid2  4795  mosneq  4867  pwv  4928  uni0  4959  int0  4986  eqbrtri  5187  tr0  5296  trv  5297  zfrep4  5314  axnulALT  5322  0ex  5325  inex1  5335  elpwi2  5353  0elpw  5374  axpow2  5385  axpow3  5386  dvdemo1  5391  vpwex  5395  zfpair2  5448  exss  5483  brv  5492  opwo0id  5516  moop2  5521  0sn0ep  5603  po0  5625  epse  5682  relxp  5718  rel0  5823  relopabiv  5844  relopabi  5846  relopabiALT  5847  eliunxp  5862  opeliunxp2  5863  dmi  5946  dmep  5948  xpidtr  6154  xpima  6213  dmsn0  6240  cnvsn0  6241  0elon  6449  funmpt  6616  funmpt2  6617  funcnv0  6644  isarep2  6669  fresaunres2  6793  f0  6802  f10d  6896  f1o00  6897  f1oi  6900  f1osn  6902  brprcneu  6910  brprcneuALT  6911  opabiotafun  7002  fvopab3ig  7025  opabex  7257  eufnfv  7266  isof1oopb  7361  ncanth  7402  mpofun  7574  reldmmpo  7584  ovid  7591  ovidig  7592  ovidi  7593  ovig  7596  ov3  7613  caovmo  7687  relmptopab  7700  porpss  7762  uniex2  7773  tfinds2  7901  finds  7936  finds2  7938  oprabex  8017  oprabex3  8018  f1stres  8054  f2ndres  8055  relmpoopab  8135  fsplitfpar  8159  poseq  8199  opeliunxp2f  8251  tpos0  8297  wfrrelOLD  8370  wfrlem14OLD  8378  wfrlem16OLD  8380  issmo  8404  tfrlem6  8438  tfrlem8  8440  tfrlem16  8449  tfr1a  8450  tfr1  8453  tz7.44lem1  8461  seqomlem2  8507  seqomlem3  8508  seqomlem4  8509  fnseqom  8511  ord3  8539  0lt1o  8560  0we1  8562  naddf  8737  eqer  8799  ecopover  8879  mapsnf1o3  8953  ssdomg  9060  en0  9078  en0OLD  9079  en0r  9081  ensn1  9082  ensn1OLD  9083  0fi  9108  snfiOLD  9110  enrefnn  9113  xpcomf1o  9127  map2xp  9213  limensuci  9219  1sdom2  9303  sdom1  9305  sdom1OLD  9306  unblem4  9359  fidomdm  9402  marypha1lem  9502  hartogslem1  9611  hartogs  9613  card2on  9623  nelaneq  9668  epinid0  9669  ruALT  9672  disjcsn  9673  elnanel  9676  cnvepnep  9677  inf2  9692  inf3lem6  9702  infeq5i  9705  zfinf2  9711  cantnflt  9741  cnfcom  9769  trcl  9797  tz9.1c  9799  tc2  9811  r1funlim  9835  r1fnon  9836  karden  9964  tskwe  10019  cardprclem  10048  pm54.43  10070  r0weon  10081  iunmapdisj  10092  alephfnon  10134  alephfplem4  10176  alephfp  10177  alephval3  10179  kmlem2  10221  dju1dif  10242  ackbij1  10306  ackbij2lem2  10308  ackbij2  10311  infpssrlem3  10374  hsmexlem4  10498  hsmexlem5  10499  ac2  10530  axac3  10533  ac6  10549  axdclem2  10589  dmct  10593  ondomon  10632  alephsucpw  10639  pwcfsdom  10652  cfpwsdom  10653  smobeth  10655  axpowndlem3  10668  zfcndun  10684  zfcndpow  10685  zfcndinf  10687  zfcndac  10688  wunex2  10807  uniwun  10809  wuncval2  10816  grur1  10889  axgroth5  10893  axgroth2  10894  axgroth6  10897  axgroth3  10900  grothtsk  10904  inaprc  10905  ltsopi  10957  dmaddpi  10959  dmmulpi  10960  1lt2pi  10974  nqerf  10999  addnqf  11017  mulnqf  11018  1lt2nq  11042  m1p1sr  11161  m1m1sr  11162  0lt1sr  11164  axaddf  11214  axmulf  11215  ax1cn  11218  subaddrii  11625  ixi  11919  recgt0ii  12201  nn1suc  12315  neg1lt0  12410  4d2e2  12463  arch  12550  un0mulcl  12587  pnf0xnn0  12632  3halfnz  12722  nummac  12803  indstr  12981  mnfltpnf  13189  ioof  13507  0nelfz1  13603  fzp1disj  13643  fzp1nel  13668  fzof  13713  fvf1tp  13840  om2uzrani  14003  om2uzf1oi  14004  uzrdglem  14008  uzrdgfni  14009  uzrdg0i  14010  ltwenn  14013  hashgf1o  14022  axdc4uzlem  14034  sq0  14241  irec  14250  facmapnn  14334  hashkf  14381  hashfxnn0  14386  hashf  14387  hash0  14416  prhash2ex  14448  hashsslei  14475  hashxplem  14482  hashbclem  14501  hashf1lem1  14504  tpf1ofv0  14545  tpfo  14549  s1dm  14656  eqs1  14660  ccat2s1p1  14677  cats1un  14769  revs1  14813  0csh0  14841  cshw1  14870  cats1fvn  14907  funcnvs1  14961  pfx2  14996  relexp0g  15071  relexpsucnnr  15074  rtrclreclem1  15106  dfrtrclrec2  15107  rtrclreclem2  15108  rtrclreclem4  15110  dfrtrcl2  15111  climmo  15603  fsumcom2  15822  ackbijnn  15876  incexclem  15884  infcvgaux1i  15905  fprodcom2  16032  bpolylem  16096  bpoly3  16106  bpoly4  16107  efcvgfsum  16134  cos1bnd  16235  cos2bnd  16236  znnen  16260  qnnen  16261  aleph1re  16293  3dvds  16379  n2dvdsm1  16417  divalglem5  16445  flodddiv4  16461  sadcaddlem  16503  sadadd2lem  16505  sadadd3  16507  sadaddlem  16512  lcmf0  16681  lcmfunsnlem2lem1  16685  lcmfunsnlem2  16687  coprmprod  16708  coprmproddvdslem  16709  2prm  16739  3lcm2e6  16779  phicl2  16815  pockthi  16954  unbenlem  16955  prmrec  16969  vdwlem13  17040  vdwnn  17045  ramcl2  17063  prmgapprmo  17109  mod2xnegi  17118  modsubi  17119  structcnvcnv  17200  strleun  17204  setsres  17225  strfv  17251  starvndxnbasendx  17363  starvndxnplusgndx  17364  starvndxnmulrndx  17365  scandxnbasendx  17375  scandxnplusgndx  17376  scandxnmulrndx  17377  vscandxnbasendx  17380  vscandxnplusgndx  17381  vscandxnmulrndx  17382  vscandxnscandx  17383  ipndxnbasendx  17391  ipndxnplusgndx  17392  ipndxnmulrndx  17393  slotsdifipndx  17394  tsetndxnplusgndx  17416  tsetndxnmulrndx  17417  tsetndxnstarvndx  17418  slotstnscsi  17419  plendxnplusgndx  17430  plendxnmulrndx  17431  plendxnscandx  17432  plendxnvscandx  17433  slotsdifplendx  17434  basendxnocndx  17442  plendxnocndx  17443  dsndxnplusgndx  17449  dsndxnmulrndx  17450  slotsdnscsi  17451  dsndxntsetndx  17452  slotsdifdsndx  17453  unifndxntsetndx  17459  slotsdifunifndx  17460  slotsdifplendx2  17476  slotsdifocndx  17477  0rest  17489  firest  17492  restid  17493  prdsval  17515  prdsbas  17517  prdsplusg  17518  prdsmulr  17519  prdsvsca  17520  imasaddfnlem  17588  imasvscafn  17597  oppchomfvalOLD  17773  oppcbasOLD  17778  2oppchomf  17784  rescbasOLD  17891  resccoOLD  17895  rescabsOLD  17897  0ssc  17901  0subcat  17902  idfucl  17945  homarel  18103  dmaf  18116  cdaf  18117  setc2ohom  18162  catcfuccl  18186  catcfucclOLD  18187  relxpchom  18250  catcxpccl  18276  catcxpcclOLD  18277  oppchofcl  18330  oyoncl  18340  odubasOLD  18362  letsr  18663  mgmidmo  18698  efmndmgm  18920  smndex1ibas  18935  smndex1mgm  18942  smndex1mnd  18945  smndex2dbas  18949  smndex2dnrinv  18950  smndex2hbas  18951  pwmnd  18972  releqg  19215  ga0  19338  oppglemOLD  19391  psgnunilem3  19538  psgnunilem4  19539  pmtrsn  19561  efgval  19759  efger  19760  efgsval2  19775  efgsp1  19779  efgsfo  19781  efgredleme  19785  efgredlem  19789  efgred  19790  cygctb  19934  gsum2d2lem  20015  gsum2d2  20016  gsumcom2  20017  dprd2d2  20088  pgpfaclem1  20125  mgplemOLD  20166  mgpressOLD  20177  opprlemOLD  20366  reldvdsr  20386  fldhmsubc  20808  00lsp  21002  sralemOLD  21199  srascaOLD  21207  sravscaOLD  21209  cnfldfun  21401  cnfldfunALT  21402  cnfldfunOLD  21414  cnfldfunALTOLD  21415  cnfldfunALTOLDOLD  21416  xrsmgm  21442  pzriprnglem8  21522  pzriprnglem13  21527  pzriprnglem14  21528  pzriprngALT  21529  znbaslemOLD  21577  resubdrg  21649  ocv0  21718  cssval  21723  thlbasOLD  21738  thlleOLD  21740  islinds2  21856  psrvscafval  21991  opsrbaslemOLD  22091  psrbag0  22109  00ply1bas  22262  ply1plusgfvi  22264  matscaOLD  22441  m2detleib  22658  tgdom  23006  tgidm  23008  indistps2ALT  23043  restbas  23187  resttopon  23190  rest0  23198  leordtval2  23241  iocpnfordt  23244  icomnfordt  23245  iooordt  23246  ist1-3  23378  1stcfb  23474  comppfsc  23561  1stckgen  23583  ptbasfi  23610  dfac14  23647  opnfbas  23871  hauspwpwf1  24016  alexsubALT  24080  ptcmplem5  24085  cnextrel  24092  ust0  24249  tuslemOLD  24297  0met  24397  prdsdsf  24398  prdsxmetlem  24399  prdsmet  24401  setsmsbasOLD  24507  setsmsdsOLD  24509  prdsbl  24525  tngdsOLD  24690  qtopbaslem  24800  xrtgioo  24847  xrsdsre  24851  zcld  24854  recld2  24855  reperflem  24859  retopconn  24870  iccpnfcnv  24994  bndth  25009  nmoleub2lem2  25168  zclmncvs  25201  recmet  25376  resscdrg  25411  ishl2  25423  recms  25433  volf  25583  iundisj2  25603  volsup  25610  icombl  25618  ioombl  25619  ismbf3d  25708  0plef  25726  0pledm  25727  itg1ge0  25740  mbfi1fseqlem5  25774  itg2addlem  25813  reldv  25925  limciun  25949  dvexp  26011  dveflem  26037  lhop1lem  26072  lhop  26075  elply2  26255  elplyd  26261  ply1term  26263  ply0  26267  plymullem  26275  qaa  26383  pserulm  26483  pserdvlem2  26490  efcn  26505  sincosq1lem  26557  tangtx  26565  sincos4thpi  26573  pigt3  26578  pige3ALT  26580  efif1olem4  26605  logf1o  26624  relogf1o  26626  log1  26645  loge  26646  logi  26647  relogiso  26658  dvrelog  26697  relogcn  26698  logcn  26707  cxpcn3  26809  resqrtcn  26810  rtprmirr  26821  2logb9irr  26856  leibpi  27003  log2ublem1  27007  birthday  27015  emcllem5  27061  harmonicbnd  27065  harmonicbnd2  27066  harmonicbnd3  27069  lgamgulm2  27097  lgamcvglem  27101  gamf  27104  ppiltx  27238  ppiublem1  27264  ppiub  27266  bclbnd  27342  bpos1lem  27344  bposlem8  27353  lgsquadlem2  27443  2sqlem9  27489  2sqlem10  27490  addsqnreup  27505  chebbnd1  27534  selberg2lem  27612  pntrsumo1  27627  selbergsb  27637  pntpbnd  27650  sltval2  27719  noxp1o  27726  nosepnelem  27742  noetasuplem2  27797  noetainflem2  27801  0slt1s  27892  addsf  28033  precsexlem1  28249  precsexlem2  28250  precsexlem3  28251  precsexlem4  28252  precsexlem5  28253  precsexlem9  28257  precsexlem10  28258  precsexlem11  28259  elons2  28299  onaddscl  28304  onmulscl  28305  eln0s  28376  0zs  28392  zseo  28424  nohalf  28425  lngndxnitvndx  28469  istrkg2ld  28486  tgcgr4  28557  ttgvalOLD  28902  ttglemOLD  28904  cchhllemOLD  28920  ax5seglem7  28968  axlowdimlem4  28978  axlowdimlem6  28980  axlowdimlem7  28981  axlowdimlem10  28984  axlowdimlem13  28987  axlowdimlem16  28990  uhgr0e  29106  uhgr0  29108  upgrbi  29128  umgrbi  29136  usgr0  29278  lfuhgr1v0e  29289  usgrexmpllem  29295  usgrexmpl  29298  griedg0prc  29299  cplgr0  29460  usgrexilem  29475  cffldtocusgr  29482  cffldtocusgrOLD  29483  rgrusgrprc  29625  rusgrprc  29626  rgrprcx  29628  rgrx0ndm  29629  usgr2pthlem  29799  pthdlem2  29804  uspgrn2crct  29841  wwlksnext  29926  clwwlknondisj  30143  0ewlk  30146  0wlk  30148  0pth  30157  1pthdlem1  30167  1trld  30174  wlk2v2elem2  30188  wlk2v2e  30189  upgr3v3e3cycl  30212  upgr4cycl4dv4e  30217  dfconngr1  30220  0conngr  30224  konigsbergumgr  30283  2wspmdisj  30369  2clwwlk2clwwlk  30382  numclwwlk3lem2lem  30415  numclwwlk3lem2  30416  ex-dif  30455  ex-in  30457  ex-eprel  30465  ex-id  30466  ex-fl  30479  ex-mod  30481  ex-hash  30485  ex-fpar  30494  avril1  30495  2bornot2b  30496  0vfval  30638  vsfval  30665  ajmoi  30890  ajfuni  30891  normlem2  31143  norm3adifii  31180  hhip  31209  hlim0  31267  hlimcaui  31268  hlimf  31269  hhssnv  31296  shscli  31349  shsval2i  31419  h1de2i  31585  fh3i  31655  fh4i  31656  cm2mi  31658  qlaxr3i  31668  mayetes3i  31761  ho0f  31783  hoif  31786  hodidi  31819  ho0subi  31827  hosd1i  31854  adjmo  31864  nmopsetn0  31897  nmfnsetn0  31910  funadj  31918  funcnvadj  31925  nmcexi  32058  cnlnadjlem8  32106  nmoptri2i  32131  opsqrlem4  32175  hmopidmchi  32183  pjoci  32212  pjinvari  32223  abrexdomjm  32535  elim2ifim  32568  iundisj2f  32612  rinvf1o  32649  dfcnv2  32694  snct  32727  fzodif2  32797  iundisj2fi  32802  dp2lt10  32848  dp2ltc  32851  dplti  32869  dpgti  32870  dpexpp1  32872  chnub  32984  gsumle  33074  xrge0slmod  33341  zarcls  33820  zartopn  33821  xrge0pluscn  33886  zlmdsOLD  33909  zlmtsetOLD  33911  qqhre  33966  esumrnmpt2  34032  esumfsup  34034  esumpcvgval  34042  hasheuni  34049  esumcvg  34050  esumcvgsum  34052  esumsup  34053  esum2d  34057  dmsigagen  34108  ldgenpisyslem3  34129  measvuni  34178  voliune  34193  volfiniune  34194  br2base  34234  dya2iocuni  34248  eulerpartlem1  34332  eulerpartlemt  34336  eulerpartgbij  34337  fib0  34364  coinfliprv  34447  ballotlem2  34453  ballotlemic  34471  ballotlem7  34500  ballotth  34502  plymul02  34523  rpsqrtcn  34570  chtvalz  34606  circlemethnat  34618  circlevma  34619  circlemethhgt  34620  hgt750lem  34628  bnj226  34710  bnj1101  34760  bnj110  34834  bnj149  34851  bnj150  34852  bnj151  34853  bnj517  34861  bnj580  34889  bnj865  34899  bnj900  34905  bnj996  34932  bnj1110  34958  bnj1133  34965  bnj1128  34966  bnj1145  34969  bnj1137  34971  bnj1171  34976  bnj1176  34981  f1resfz0f1d  35081  subfacp1lem5  35152  subfacp1lem6  35153  kur14lem9  35182  cvmcov2  35243  cvmliftlem1  35253  cvmliftlem4  35256  cvmliftlem5  35257  gonanegoal  35320  satfv0  35326  satfv0fun  35339  fmlan0  35359  gonan0  35360  fmla0disjsuc  35366  ex-sategoelel12  35395  msrfo  35514  problem5  35637  brtpid1  35683  brtpid2  35684  brtpid3  35685  faclimlem1  35705  axextndbi  35768  txprel  35843  relsset  35852  relbigcup  35861  fvbigcup  35866  fnsingle  35883  fvsingle  35884  snelsingles  35886  funimage  35892  fullfunfnv  35910  imagesset  35917  funtransport  35995  colinrel  36021  funray  36104  funline  36106  0hf  36141  neibastop2lem  36326  filnetlem3  36346  nrmo  36376  waj-ax  36380  lukshef-ax2  36381  arg-ax  36382  limsucncmpi  36411  dnizeq0  36441  knoppcnlem8  36466  knoppcnlem11  36469  cnndvlem1  36503  bj-babylob  36570  bj-ax12ssb  36624  bj-nnfnth  36709  bj-snsetex  36929  bj-0eltag  36944  bj-2upln0  36989  bj-2upln1upl  36990  bj-snexg  37000  bj-unexg  37004  bj-adjg1  37009  f1omptsnlem  37302  f1omptsn  37303  icoreresf  37318  relowlssretop  37329  relowlpssretop  37330  domalom  37370  matunitlindf  37578  poimirlem3  37583  poimirlem9  37589  poimirlem16  37596  poimirlem17  37597  poimirlem18  37598  poimirlem19  37599  poimirlem20  37600  poimirlem26  37606  mblfinlem1  37617  mblfinlem2  37618  ismblfin  37621  voliunnfl  37624  cnambfre  37628  abrexdom  37690  fdc  37705  cncfres  37725  heibor1lem  37769  grposnOLD  37842  bicontr  38040  an12i  38058  tsim1  38090  ac6s6f  38133  vvdifopab  38216  brcnvrabga  38298  opabf  38324  xrnrel  38329  relcoels  38380  cnvcosseq  38393  refrelcoss3  38419  refrelcoss2  38420  symrelcoss2  38422  refrelcoss  38479  symrelcoss  38516  n0eldmqs  38604  ax13fromc9  38862  dedths  38918  renegclALT  38919  hlhilslemOLD  41896  12gcd5e1  41960  60gcd7e1  41962  lcmineqlem23  42008  dvrelog2  42021  dvrelog3  42022  dvrelog2b  42023  aks4d1p1p6  42030  aks4d1p1p7  42031  aks4d1p1  42033  sticksstones22  42125  2xp3dxp2ge1d  42198  sn-axprlem3  42210  acos1half  42340  moxfr  42648  mapfzcons1  42673  diophrw  42715  0dioph  42734  vdioph  42735  rabren3dioph  42771  2nn0ind  42902  rpnnen3  42989  kelac2lem  43021  frlmpwfi  43055  oaordnrex  43257  omnord1ex  43266  oenord1ex  43277  oaomoencom  43279  ifpbiidcor2  43445  iscard4  43495  sqrtcval  43603  resqrtvalex  43607  eliunov2  43641  xphe  43743  0he  43744  he0  43746  snhesn  43748  idhe  43749  frege54cor1c  43877  clsk1independent  44008  neicvgnvor  44078  amgm2d  44160  amgm3d  44161  amgm4d  44162  ismnushort  44270  lhe4.4ex1a  44298  rusbcALT  44408  ipo0  44418  ifr0  44419  vk15.4j  44499  2sb5nd  44531  dfvd1ir  44544  dfvd2anir  44555  dfvd2ir  44557  dfvd3ir  44564  dfvd3anir  44567  iden2  44585  e0bir  44748  uun2221p1  44785  uun2221p2  44786  2sb5ndVD  44881  2sb5ndALT  44903  iunconnlem2  44906  trwf  44909  fnchoice  44929  unisn0  44956  eliincex  45012  icof  45126  fnmptif  45175  supminfxr  45379  rexanuz2nf  45408  fsumiunss  45496  climlimsupcex  45690  liminfltlimsupex  45702  liminflelimsupcex  45718  xlimrel  45741  xlimfun  45776  resincncf  45796  dvnprodlem3  45869  volioc  45893  volico  45904  dmvolss  45906  volioof  45908  stoweidlem13  45934  stoweidlem34  45955  stirlinglem5  45999  stirlinglem13  46007  stirlingr  46011  fourierdlem42  46070  fourierdlem62  46089  fouriersw  46152  etransc  46204  salexct  46255  salexct2  46260  salgencntex  46264  sge0rnn0  46289  gsumge0cl  46292  sge00  46297  sge0resplit  46327  sge0reuz  46368  omeiunle  46438  0ome  46450  icoresmbl  46464  ovn0lem  46486  ovnhoilem1  46522  hspmbl  46550  nsssmfmbf  46700  mbfpsssmf  46704  smfresal  46709  smfmullem4  46715  smfpimbor1lem1  46719  smfpimbor1lem2  46720  aistia  46812  aisfina  46813  aiffnbandciffatnotciffb  46819  axorbciffatcxorb  46820  abnotbtaxb  46830  abnotataxb  46831  eusnsn  46941  aiotaval  47010  aiota0ndef  47012  fundcmpsurinjimaid  47285  ichv  47323  ichf  47324  ichid  47325  icht  47326  ichcircshi  47328  icheq  47336  spr0nelg  47350  m3prm  47466  m7prm  47474  0noddALTV  47563  2noddALTV  47567  341fppr2  47608  9fppr8  47611  nfermltl8rev  47616  nfermltl2rev  47617  nfermltlrev  47618  sbgoldbo  47661  nnsum3primes4  47662  evengpop3  47672  usgrexmpl1lem  47836  usgrexmpl1  47837  usgrexmpl1tri  47840  usgrexmpl2lem  47841  usgrexmpl2  47842  usgrexmpl2nb0  47846  usgrexmpl2nb1  47847  usgrexmpl2nb2  47848  usgrexmpl2nb3  47849  usgrexmpl2nb4  47850  usgrexmpl2nb5  47851  oddinmgm  47898  nn0mnd  47902  2zrngamgm  47968  2zrngaabl  47973  2zrngmmgm  47975  2zrngnring  47981  fldhmsubcALTV  48056  eliunxp2  48058  zlmodzxzldeplem  48227  zlmodzxzldep  48233  ldepslinc  48238  rrx2xpreen  48453  rrx2plordisom  48457  line2ylem  48485  line2  48486  line2x  48488  inlinecirc02plem  48520  mosn  48544  mof0  48551  mof0ALT  48553  f1omo  48574  prstclevalOLD  48736  prstcocvalOLD  48739  ex-gte  48821  empty-surprise  48876  eximp-surprise2  48879  amgmw2d  48898