Theorem mpbir 230

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 227	. 2 ⊢ (𝜓 → 𝜑)
4	1, 3	ax-mp 5	1 ⊢ 𝜑

Syntax hints:   ↔ wb 205

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 206

This theorem is referenced by:  pm5.74ri  272  con4bii  321  imnani  400  mpbir2an  710  imorri  854  orri  861  mpbir3an  1339  xorexmid  1521  tru  1538  had1  1597  nic-mpALT  1667  nic-ax  1668  nic-axALT  1669  nfi  1783  mpgbir  1794  nfxfr  1848  19.35ri  1875  ax5e  1908  ax6ev  1966  sbt  2062  equsb1v  2096  ax13  2369  ax13ALT  2419  moanmo  2613  axi12  2696  axbnd  2697  axexte  2699  axextmo  2702  nulmo  2703  vexw  2710  eqeltri  2824  nfcxfr  2896  neir  2938  neirr  2944  eqnetri  3006  nelir  3044  mprgbir  3063  cbvrexdva2OLD  3341  issetri  3486  moeq  3700  rmoeq  3731  cdeqi  3758  eqsstri  4012  3sstr4i  4021  rmo0  4355  rabnc  4383  reuprg  4703  tpid1  4768  tpid2  4770  mosneq  4839  pwv  4900  uni0  4933  int0  4960  eqbrtri  5163  tr0  5272  trv  5273  zfrep4  5290  axnulALT  5298  0ex  5301  inex1  5311  elpwi2  5342  elpwi2OLD  5343  0elpw  5350  axpow2  5361  axpow3  5362  dvdemo1  5367  vpwex  5371  zfpair2  5424  exss  5459  brv  5468  opwo0id  5493  moop2  5498  0sn0ep  5580  po0  5601  epse  5655  relxp  5690  rel0  5795  relopabiv  5816  relopabi  5818  relopabiALT  5819  eliunxp  5834  opeliunxp2  5835  dmi  5918  dmep  5920  xpidtr  6122  xpima  6180  dmsn0  6207  cnvsn0  6208  0elon  6417  funmpt  6585  funmpt2  6586  funcnv0  6613  isarep2  6638  fresaunres2  6763  f0  6772  f10d  6867  f1o00  6868  f1oi  6871  f1osn  6873  brprcneu  6881  brprcneuALT  6882  opabiotafun  6973  fvopab3ig  6995  opabex  7226  eufnfv  7235  isof1oopb  7327  ncanth  7368  mpofun  7537  mpofunOLD  7538  reldmmpo  7548  ovid  7554  ovidig  7555  ovidi  7556  ovig  7559  ov3  7576  caovmo  7650  relmptopab  7663  porpss  7724  uniex2  7735  tfinds2  7860  finds  7896  finds2  7898  oprabex  7972  oprabex3  7973  f1stres  8009  f2ndres  8010  relmpoopab  8091  fsplitfpar  8115  poseq  8155  opeliunxp2f  8207  tpos0  8253  wfrrelOLD  8326  wfrlem14OLD  8334  wfrlem16OLD  8336  issmo  8360  tfrlem6  8394  tfrlem8  8396  tfrlem16  8405  tfr1a  8406  tfr1  8409  tz7.44lem1  8417  seqomlem2  8463  seqomlem3  8464  seqomlem4  8465  fnseqom  8467  ord3  8495  0lt1o  8516  0we1  8518  naddf  8693  eqer  8751  ecopover  8829  mapsnf1o3  8903  ssdomg  9010  en0  9027  en0OLD  9028  en0r  9030  ensn1  9031  ensn1OLD  9032  snfi  9058  enrefnn  9061  xpcomf1o  9075  map2xp  9161  limensuci  9167  1sdom2  9254  sdom1  9256  sdom1OLD  9257  unblem4  9312  fidomdm  9343  marypha1lem  9442  hartogslem1  9551  hartogs  9553  card2on  9563  nelaneq  9608  epinid0  9609  ruALT  9612  disjcsn  9613  elnanel  9616  cnvepnep  9617  inf2  9632  inf3lem6  9642  infeq5i  9645  zfinf2  9651  cantnflt  9681  cnfcom  9709  trcl  9737  tz9.1c  9739  tc2  9751  r1funlim  9775  r1fnon  9776  karden  9904  tskwe  9959  cardprclem  9988  pm54.43  10010  r0weon  10021  iunmapdisj  10032  alephfnon  10074  alephfplem4  10116  alephfp  10117  alephval3  10119  kmlem2  10160  dju1dif  10181  ackbij1  10247  ackbij2lem2  10249  ackbij2  10252  infpssrlem3  10314  hsmexlem4  10438  hsmexlem5  10439  ac2  10470  axac3  10473  ac6  10489  axdclem2  10529  dmct  10533  ondomon  10572  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  11565  ixi  11859  recgt0ii  12136  nn1suc  12250  neg1lt0  12345  4d2e2  12398  arch  12485  un0mulcl  12522  pnf0xnn0  12567  3halfnz  12657  nummac  12738  indstr  12916  mnfltpnf  13124  ioof  13442  0nelfz1  13538  fzp1disj  13578  fzp1nel  13603  fzof  13647  om2uzrani  13935  om2uzf1oi  13936  uzrdglem  13940  uzrdgfni  13941  uzrdg0i  13942  ltwenn  13945  hashgf1o  13954  axdc4uzlem  13966  sq0  14173  irec  14182  facmapnn  14262  hashkf  14309  hashfxnn0  14314  hashf  14315  hash0  14344  prhash2ex  14376  hashsslei  14403  hashxplem  14410  hashbclem  14429  hashf1lem1  14433  hashf1lem1OLD  14434  s1dm  14576  eqs1  14580  ccat2s1p1  14597  cats1un  14689  revs1  14733  0csh0  14761  cshw1  14790  cats1fvn  14827  funcnvs1  14881  pfx2  14916  relexp0g  14987  relexpsucnnr  14990  rtrclreclem1  15022  dfrtrclrec2  15023  rtrclreclem2  15024  rtrclreclem4  15026  dfrtrcl2  15027  climmo  15519  fsumcom2  15738  ackbijnn  15792  incexclem  15800  infcvgaux1i  15821  fprodcom2  15946  bpolylem  16010  bpoly3  16020  bpoly4  16021  efcvgfsum  16048  cos1bnd  16149  cos2bnd  16150  znnen  16174  qnnen  16175  aleph1re  16207  3dvds  16293  n2dvdsm1  16331  divalglem5  16359  flodddiv4  16375  sadcaddlem  16417  sadadd2lem  16419  sadadd3  16421  sadaddlem  16426  lcmf0  16590  lcmfunsnlem2lem1  16594  lcmfunsnlem2  16596  coprmprod  16617  coprmproddvdslem  16618  2prm  16648  3lcm2e6  16689  phicl2  16722  pockthi  16861  unbenlem  16862  prmrec  16876  vdwlem13  16947  vdwnn  16952  ramcl2  16970  prmgapprmo  17016  mod2xnegi  17025  modsubi  17026  structcnvcnv  17107  strleun  17111  setsres  17132  strfv  17158  starvndxnbasendx  17270  starvndxnplusgndx  17271  starvndxnmulrndx  17272  scandxnbasendx  17282  scandxnplusgndx  17283  scandxnmulrndx  17284  vscandxnbasendx  17287  vscandxnplusgndx  17288  vscandxnmulrndx  17289  vscandxnscandx  17290  ipndxnbasendx  17298  ipndxnplusgndx  17299  ipndxnmulrndx  17300  slotsdifipndx  17301  tsetndxnplusgndx  17323  tsetndxnmulrndx  17324  tsetndxnstarvndx  17325  slotstnscsi  17326  plendxnplusgndx  17337  plendxnmulrndx  17338  plendxnscandx  17339  plendxnvscandx  17340  slotsdifplendx  17341  basendxnocndx  17349  plendxnocndx  17350  dsndxnplusgndx  17356  dsndxnmulrndx  17357  slotsdnscsi  17358  dsndxntsetndx  17359  slotsdifdsndx  17360  unifndxntsetndx  17366  slotsdifunifndx  17367  slotsdifplendx2  17383  slotsdifocndx  17384  0rest  17396  firest  17399  restid  17400  prdsval  17422  prdsbas  17424  prdsplusg  17425  prdsmulr  17426  prdsvsca  17427  imasaddfnlem  17495  imasvscafn  17504  oppchomfvalOLD  17680  oppcbasOLD  17685  2oppchomf  17691  rescbasOLD  17798  resccoOLD  17802  rescabsOLD  17804  0ssc  17808  0subcat  17809  idfucl  17852  homarel  18010  dmaf  18023  cdaf  18024  setc2ohom  18069  catcfuccl  18093  catcfucclOLD  18094  relxpchom  18157  catcxpccl  18183  catcxpcclOLD  18184  oppchofcl  18237  oyoncl  18247  odubasOLD  18269  letsr  18570  mgmidmo  18605  efmndmgm  18822  smndex1ibas  18837  smndex1mgm  18844  smndex1mnd  18847  smndex2dbas  18851  smndex2dnrinv  18852  smndex2hbas  18853  pwmnd  18874  releqg  19114  ga0  19233  oppglemOLD  19286  psgnunilem3  19435  psgnunilem4  19436  pmtrsn  19458  efgval  19656  efger  19657  efgsval2  19672  efgsp1  19676  efgsfo  19678  efgredleme  19682  efgredlem  19686  efgred  19687  cygctb  19831  gsum2d2lem  19912  gsum2d2  19913  gsumcom2  19914  dprd2d2  19985  pgpfaclem1  20022  mgplemOLD  20063  mgpressOLD  20074  opprlemOLD  20261  reldvdsr  20281  fldhmsubc  20655  00lsp  20847  sralemOLD  21044  srascaOLD  21052  sravscaOLD  21054  cnfldfun  21273  cnfldfunALT  21274  cnfldfunOLD  21286  cnfldfunALTOLD  21287  cnfldfunALTOLDOLD  21288  xrsmgm  21314  pzriprnglem8  21394  pzriprnglem13  21399  pzriprnglem14  21400  pzriprngALT  21401  znbaslemOLD  21449  resubdrg  21520  ocv0  21589  cssval  21594  thlbasOLD  21609  thlleOLD  21611  islinds2  21727  psrvscafval  21870  opsrbaslemOLD  21966  psrbag0  21984  00ply1bas  22132  ply1plusgfvi  22134  matscaOLD  22290  m2detleib  22507  tgdom  22855  tgidm  22857  indistps2ALT  22892  restbas  23036  resttopon  23039  rest0  23047  leordtval2  23090  iocpnfordt  23093  icomnfordt  23094  iooordt  23095  ist1-3  23227  1stcfb  23323  comppfsc  23410  1stckgen  23432  ptbasfi  23459  dfac14  23496  opnfbas  23720  hauspwpwf1  23865  alexsubALT  23929  ptcmplem5  23934  cnextrel  23941  ust0  24098  tuslemOLD  24146  0met  24246  prdsdsf  24247  prdsxmetlem  24248  prdsmet  24250  setsmsbasOLD  24356  setsmsdsOLD  24358  prdsbl  24374  tngdsOLD  24539  qtopbaslem  24649  xrtgioo  24696  xrsdsre  24700  zcld  24703  recld2  24704  reperflem  24708  retopconn  24719  iccpnfcnv  24843  bndth  24858  nmoleub2lem2  25017  zclmncvs  25050  recmet  25225  resscdrg  25260  ishl2  25272  recms  25282  volf  25432  iundisj2  25452  volsup  25459  icombl  25467  ioombl  25468  ismbf3d  25557  0plef  25575  0pledm  25576  itg1ge0  25589  mbfi1fseqlem5  25623  itg2addlem  25662  reldv  25773  limciun  25797  dvexp  25859  dveflem  25885  lhop1lem  25920  lhop  25923  elply2  26104  elplyd  26110  ply1term  26112  ply0  26116  plymullem  26124  qaa  26232  pserulm  26332  pserdvlem2  26339  efcn  26354  sincosq1lem  26406  tangtx  26414  sincos4thpi  26422  pigt3  26426  pige3ALT  26428  efif1olem4  26453  logf1o  26472  relogf1o  26474  log1  26493  loge  26494  logi  26495  relogiso  26506  dvrelog  26545  relogcn  26546  logcn  26555  cxpcn3  26657  resqrtcn  26658  2logb9irr  26701  leibpi  26848  log2ublem1  26852  birthday  26860  emcllem5  26906  harmonicbnd  26910  harmonicbnd2  26911  harmonicbnd3  26914  lgamgulm2  26942  lgamcvglem  26946  gamf  26949  ppiltx  27083  ppiublem1  27109  ppiub  27111  bclbnd  27187  bpos1lem  27189  bposlem8  27198  lgsquadlem2  27288  2sqlem9  27334  2sqlem10  27335  addsqnreup  27350  chebbnd1  27379  selberg2lem  27457  pntrsumo1  27472  selbergsb  27482  pntpbnd  27495  sltval2  27563  noxp1o  27570  nosepnelem  27586  noetasuplem2  27641  noetainflem2  27645  0slt1s  27736  addsf  27873  precsexlem1  28079  precsexlem2  28080  precsexlem3  28081  precsexlem4  28082  precsexlem5  28083  precsexlem9  28087  precsexlem10  28088  precsexlem11  28089  elons2  28125  lngndxnitvndx  28221  istrkg2ld  28238  tgcgr4  28309  ttgvalOLD  28654  ttglemOLD  28656  cchhllemOLD  28672  ax5seglem7  28720  axlowdimlem4  28730  axlowdimlem6  28732  axlowdimlem7  28733  axlowdimlem10  28736  axlowdimlem13  28739  axlowdimlem16  28742  uhgr0e  28858  uhgr0  28860  upgrbi  28880  umgrbi  28888  usgr0  29030  lfuhgr1v0e  29041  usgrexmpllem  29047  usgrexmpl  29050  griedg0prc  29051  cplgr0  29212  usgrexilem  29227  cffldtocusgr  29234  cffldtocusgrOLD  29235  rgrusgrprc  29377  rusgrprc  29378  rgrprcx  29380  rgrx0ndm  29381  usgr2pthlem  29551  pthdlem2  29556  uspgrn2crct  29593  wwlksnext  29678  clwwlknondisj  29895  0ewlk  29898  0wlk  29900  0pth  29909  1pthdlem1  29919  1trld  29926  wlk2v2elem2  29940  wlk2v2e  29941  upgr3v3e3cycl  29964  upgr4cycl4dv4e  29969  dfconngr1  29972  0conngr  29976  konigsbergumgr  30035  2wspmdisj  30121  2clwwlk2clwwlk  30134  numclwwlk3lem2lem  30167  numclwwlk3lem2  30168  ex-dif  30207  ex-in  30209  ex-eprel  30217  ex-id  30218  ex-fl  30231  ex-mod  30233  ex-hash  30237  ex-fpar  30246  avril1  30247  2bornot2b  30248  0vfval  30390  vsfval  30417  ajmoi  30642  ajfuni  30643  normlem2  30895  norm3adifii  30932  hhip  30961  hlim0  31019  hlimcaui  31020  hlimf  31021  hhssnv  31048  shscli  31101  shsval2i  31171  h1de2i  31337  fh3i  31407  fh4i  31408  cm2mi  31410  qlaxr3i  31420  mayetes3i  31513  ho0f  31535  hoif  31538  hodidi  31571  ho0subi  31579  hosd1i  31606  adjmo  31616  nmopsetn0  31649  nmfnsetn0  31662  funadj  31670  funcnvadj  31677  nmcexi  31810  cnlnadjlem8  31858  nmoptri2i  31883  opsqrlem4  31927  hmopidmchi  31935  pjoci  31964  pjinvari  31975  abrexdomjm  32275  elim2ifim  32308  iundisj2f  32352  rinvf1o  32385  dfcnv2  32432  snct  32466  fzodif2  32531  iundisj2fi  32536  dp2lt10  32576  dp2ltc  32579  dplti  32597  dpgti  32598  dpexpp1  32600  gsumle  32769  xrge0slmod  32987  zarcls  33398  zartopn  33399  xrge0pluscn  33464  zlmdsOLD  33487  zlmtsetOLD  33489  qqhre  33544  esumrnmpt2  33610  esumfsup  33612  esumpcvgval  33620  hasheuni  33627  esumcvg  33628  esumcvgsum  33630  esumsup  33631  esum2d  33635  dmsigagen  33686  ldgenpisyslem3  33707  measvuni  33756  voliune  33771  volfiniune  33772  br2base  33812  dya2iocuni  33826  eulerpartlem1  33910  eulerpartlemt  33914  eulerpartgbij  33915  fib0  33942  coinfliprv  34025  ballotlem2  34031  ballotlemic  34049  ballotlem7  34078  ballotth  34080  plymul02  34101  rpsqrtcn  34148  chtvalz  34184  circlemethnat  34196  circlevma  34197  circlemethhgt  34198  hgt750lem  34206  bnj226  34288  bnj1101  34338  bnj110  34412  bnj149  34429  bnj150  34430  bnj151  34431  bnj517  34439  bnj580  34467  bnj865  34477  bnj900  34483  bnj996  34510  bnj1110  34536  bnj1133  34543  bnj1128  34544  bnj1145  34547  bnj1137  34549  bnj1171  34554  bnj1176  34559  f1resfz0f1d  34646  subfacp1lem5  34717  subfacp1lem6  34718  kur14lem9  34747  cvmcov2  34808  cvmliftlem1  34818  cvmliftlem4  34821  cvmliftlem5  34822  gonanegoal  34885  satfv0  34891  satfv0fun  34904  fmlan0  34924  gonan0  34925  fmla0disjsuc  34931  ex-sategoelel12  34960  msrfo  35079  problem5  35196  brtpid1  35238  brtpid2  35239  brtpid3  35240  faclimlem1  35260  axextndbi  35323  txprel  35398  relsset  35407  relbigcup  35416  fvbigcup  35421  fnsingle  35438  fvsingle  35439  snelsingles  35441  funimage  35447  fullfunfnv  35465  imagesset  35472  funtransport  35550  colinrel  35576  funray  35659  funline  35661  0hf  35696  neibastop2lem  35767  filnetlem3  35787  nrmo  35817  waj-ax  35821  lukshef-ax2  35822  arg-ax  35823  limsucncmpi  35852  dnizeq0  35873  knoppcnlem8  35898  knoppcnlem11  35901  cnndvlem1  35935  bj-babylob  36004  bj-ax12ssb  36057  bj-nnfnth  36143  bj-snsetex  36365  bj-0eltag  36380  bj-2upln0  36425  bj-2upln1upl  36426  bj-snexg  36436  bj-unexg  36440  bj-adjg1  36445  f1omptsnlem  36738  f1omptsn  36739  icoreresf  36754  relowlssretop  36765  relowlpssretop  36766  domalom  36806  matunitlindf  37013  poimirlem3  37018  poimirlem9  37024  poimirlem16  37031  poimirlem17  37032  poimirlem18  37033  poimirlem19  37034  poimirlem20  37035  poimirlem26  37041  mblfinlem1  37052  mblfinlem2  37053  ismblfin  37056  voliunnfl  37059  cnambfre  37063  abrexdom  37125  fdc  37140  cncfres  37160  heibor1lem  37204  grposnOLD  37277  bicontr  37475  an12i  37493  tsim1  37525  ac6s6f  37568  vvdifopab  37654  brcnvrabga  37737  opabf  37763  xrnrel  37769  relcoels  37820  cnvcosseq  37833  refrelcoss3  37859  refrelcoss2  37860  symrelcoss2  37862  refrelcoss  37919  symrelcoss  37956  n0eldmqs  38044  ax13fromc9  38302  dedths  38358  renegclALT  38359  hlhilslemOLD  41336  12gcd5e1  41398  60gcd7e1  41400  lcmineqlem23  41446  dvrelog2  41459  dvrelog3  41460  dvrelog2b  41461  aks4d1p1p6  41468  aks4d1p1p7  41469  aks4d1p1  41471  sticksstones22  41559  2xp3dxp2ge1d  41600  sn-axprlem3  41612  rtprmirr  41818  acos1half  42009  moxfr  42024  mapfzcons1  42049  diophrw  42091  0dioph  42110  vdioph  42111  rabren3dioph  42147  2nn0ind  42278  rpnnen3  42365  kelac2lem  42400  frlmpwfi  42434  oaordnrex  42637  omnord1ex  42646  oenord1ex  42657  oaomoencom  42659  ifpbiidcor2  42826  iscard4  42876  sqrtcval  42984  resqrtvalex  42988  eliunov2  43022  xphe  43124  0he  43125  he0  43127  snhesn  43129  idhe  43130  frege54cor1c  43258  clsk1independent  43389  neicvgnvor  43459  amgm2d  43541  amgm3d  43542  amgm4d  43543  ismnushort  43651  lhe4.4ex1a  43679  rusbcALT  43789  ipo0  43799  ifr0  43800  vk15.4j  43880  2sb5nd  43912  dfvd1ir  43925  dfvd2anir  43936  dfvd2ir  43938  dfvd3ir  43945  dfvd3anir  43948  iden2  43966  e0bir  44129  uun2221p1  44166  uun2221p2  44167  2sb5ndVD  44262  2sb5ndALT  44284  iunconnlem2  44287  fnchoice  44304  unisn0  44331  eliincex  44389  icof  44505  fnmptif  44555  supminfxr  44759  rexanuz2nf  44788  fsumiunss  44876  climlimsupcex  45070  liminfltlimsupex  45082  liminflelimsupcex  45098  xlimrel  45121  xlimfun  45156  resincncf  45176  dvnprodlem3  45249  volioc  45273  volico  45284  dmvolss  45286  volioof  45288  stoweidlem13  45314  stoweidlem34  45335  stirlinglem5  45379  stirlinglem13  45387  stirlingr  45391  fourierdlem42  45450  fourierdlem62  45469  fouriersw  45532  etransc  45584  salexct  45635  salexct2  45640  salgencntex  45644  sge0rnn0  45669  gsumge0cl  45672  sge00  45677  sge0resplit  45707  sge0reuz  45748  omeiunle  45818  0ome  45830  icoresmbl  45844  ovn0lem  45866  ovnhoilem1  45902  hspmbl  45930  nsssmfmbf  46080  mbfpsssmf  46084  smfresal  46089  smfmullem4  46095  smfpimbor1lem1  46099  smfpimbor1lem2  46100  aistia  46192  aisfina  46193  aiffnbandciffatnotciffb  46199  axorbciffatcxorb  46200  abnotbtaxb  46210  abnotataxb  46211  eusnsn  46321  aiotaval  46388  aiota0ndef  46390  fundcmpsurinjimaid  46664  ichv  46702  ichf  46703  ichid  46704  icht  46705  ichcircshi  46707  icheq  46715  spr0nelg  46729  m3prm  46845  m7prm  46853  0noddALTV  46942  2noddALTV  46946  341fppr2  46987  9fppr8  46990  nfermltl8rev  46995  nfermltl2rev  46996  nfermltlrev  46997  sbgoldbo  47040  nnsum3primes4  47041  evengpop3  47051  oddinmgm  47150  nn0mnd  47154  2zrngamgm  47220  2zrngaabl  47225  2zrngmmgm  47227  2zrngnring  47233  fldhmsubcALTV  47308  eliunxp2  47310  zlmodzxzldeplem  47479  zlmodzxzldep  47485  ldepslinc  47490  rrx2xpreen  47705  rrx2plordisom  47709  line2ylem  47737  line2  47738  line2x  47740  inlinecirc02plem  47772  mosn  47796  mof0  47803  mof0ALT  47805  f1omo  47826  prstclevalOLD  47988  prstcocvalOLD  47991  ex-gte  48073  empty-surprise  48128  eximp-surprise2  48131  amgmw2d  48150