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  271  con4bii  320  imnani  401  mpbir2an  709  imorri  853  orri  860  mpbir3an  1341  xorexmid  1527  tru  1545  had1  1604  nic-mpALT  1674  nic-ax  1675  nic-axALT  1676  nfi  1790  mpgbir  1801  nfxfr  1855  19.35ri  1882  ax5e  1915  ax6ev  1973  sbt  2069  equsb1v  2103  ax13  2374  ax13ALT  2424  moanmo  2618  axi12  2701  axbnd  2702  axexte  2704  axextmo  2707  nulmo  2708  vexw  2715  eqeltri  2829  nfcxfr  2901  neir  2943  neirr  2949  eqnetri  3011  nelir  3049  mprgbir  3068  cbvrexdva2OLD  3346  issetri  3490  moeq  3703  rmoeq  3734  cdeqi  3761  eqsstri  4016  3sstr4i  4025  rmo0  4359  rabnc  4387  reuprg  4707  tpid1  4772  tpid2  4774  mosneq  4843  pwv  4905  uni0  4939  int0  4966  eqbrtri  5169  tr0  5278  trv  5279  zfrep4  5296  axnulALT  5304  0ex  5307  inex1  5317  elpwi2  5346  elpwi2OLD  5347  0elpw  5354  axpow2  5365  axpow3  5366  dvdemo1  5371  vpwex  5375  zfpair2  5428  exss  5463  brv  5472  opwo0id  5497  moop2  5502  0sn0ep  5584  po0  5605  epse  5659  relxp  5694  rel0  5799  relopabiv  5820  relopabi  5822  relopabiALT  5823  eliunxp  5837  opeliunxp2  5838  dmi  5921  dmep  5923  xpidtr  6123  xpima  6181  dmsn0  6208  cnvsn0  6209  0elon  6418  funmpt  6586  funmpt2  6587  funcnv0  6614  isarep2  6639  fresaunres2  6763  f0  6772  f10d  6867  f1o00  6868  f1oi  6871  f1osn  6873  brprcneu  6881  brprcneuALT  6882  opabiotafun  6972  fvopab3ig  6994  opabex  7224  eufnfv  7233  isof1oopb  7324  ncanth  7365  mpofun  7534  mpofunOLD  7535  reldmmpo  7545  ovid  7551  ovidig  7552  ovidi  7553  ovig  7556  ov3  7572  caovmo  7646  relmptopab  7658  porpss  7719  uniex2  7730  tfinds2  7855  finds  7891  finds2  7893  oprabex  7965  oprabex3  7966  f1stres  8001  f2ndres  8002  relmpoopab  8082  fsplitfpar  8106  poseq  8146  opeliunxp2f  8197  tpos0  8243  wfrrelOLD  8316  wfrlem14OLD  8324  wfrlem16OLD  8326  issmo  8350  tfrlem6  8384  tfrlem8  8386  tfrlem16  8395  tfr1a  8396  tfr1  8399  tz7.44lem1  8407  seqomlem2  8453  seqomlem3  8454  seqomlem4  8455  fnseqom  8457  ord3  8485  0lt1o  8506  0we1  8508  naddf  8682  eqer  8740  ecopover  8817  mapsnf1o3  8891  ssdomg  8998  en0  9015  en0OLD  9016  en0r  9018  ensn1  9019  ensn1OLD  9020  snfi  9046  enrefnn  9049  xpcomf1o  9063  map2xp  9149  limensuci  9155  1sdom2  9242  sdom1  9244  sdom1OLD  9245  unblem4  9300  fidomdm  9331  marypha1lem  9430  hartogslem1  9539  hartogs  9541  card2on  9551  nelaneq  9596  epinid0  9597  ruALT  9600  disjcsn  9601  elnanel  9604  cnvepnep  9605  inf2  9620  inf3lem6  9630  infeq5i  9633  zfinf2  9639  cantnflt  9669  cnfcom  9697  trcl  9725  tz9.1c  9727  tc2  9739  r1funlim  9763  r1fnon  9764  karden  9892  tskwe  9947  cardprclem  9976  pm54.43  9998  r0weon  10009  iunmapdisj  10020  alephfnon  10062  alephfplem4  10104  alephfp  10105  alephval3  10107  kmlem2  10148  dju1dif  10169  ackbij1  10235  ackbij2lem2  10237  ackbij2  10240  infpssrlem3  10302  hsmexlem4  10426  hsmexlem5  10427  ac2  10458  axac3  10461  ac6  10477  axdclem2  10517  dmct  10521  ondomon  10560  alephsucpw  10567  pwcfsdom  10580  cfpwsdom  10581  smobeth  10583  axpowndlem3  10596  zfcndun  10612  zfcndpow  10613  zfcndinf  10615  zfcndac  10616  wunex2  10735  uniwun  10737  wuncval2  10744  grur1  10817  axgroth5  10821  axgroth2  10822  axgroth6  10825  axgroth3  10828  grothtsk  10832  inaprc  10833  ltsopi  10885  dmaddpi  10887  dmmulpi  10888  1lt2pi  10902  nqerf  10927  addnqf  10945  mulnqf  10946  1lt2nq  10970  m1p1sr  11089  m1m1sr  11090  0lt1sr  11092  axaddf  11142  axmulf  11143  ax1cn  11146  subaddrii  11551  ixi  11845  recgt0ii  12122  nn1suc  12236  neg1lt0  12331  4d2e2  12384  arch  12471  un0mulcl  12508  pnf0xnn0  12553  3halfnz  12643  nummac  12724  indstr  12902  mnfltpnf  13108  ioof  13426  0nelfz1  13522  fzp1disj  13562  fzp1nel  13587  fzof  13631  om2uzrani  13919  om2uzf1oi  13920  uzrdglem  13924  uzrdgfni  13925  uzrdg0i  13926  ltwenn  13929  hashgf1o  13938  axdc4uzlem  13950  sq0  14158  irec  14167  facmapnn  14247  hashkf  14294  hashfxnn0  14299  hashf  14300  hash0  14329  prhash2ex  14361  hashsslei  14388  hashxplem  14395  hashbclem  14413  hashf1lem1  14417  hashf1lem1OLD  14418  s1dm  14560  eqs1  14564  ccat2s1p1  14581  cats1un  14673  revs1  14717  0csh0  14745  cshw1  14774  cats1fvn  14811  funcnvs1  14865  pfx2  14900  relexp0g  14971  relexpsucnnr  14974  rtrclreclem1  15006  dfrtrclrec2  15007  rtrclreclem2  15008  rtrclreclem4  15010  dfrtrcl2  15011  climmo  15503  fsumcom2  15722  ackbijnn  15776  incexclem  15784  infcvgaux1i  15805  fprodcom2  15930  bpolylem  15994  bpoly3  16004  bpoly4  16005  efcvgfsum  16031  cos1bnd  16132  cos2bnd  16133  znnen  16157  qnnen  16158  aleph1re  16190  3dvds  16276  n2dvdsm1  16314  divalglem5  16342  flodddiv4  16358  sadcaddlem  16400  sadadd2lem  16402  sadadd3  16404  sadaddlem  16409  lcmf0  16573  lcmfunsnlem2lem1  16577  lcmfunsnlem2  16579  coprmprod  16600  coprmproddvdslem  16601  2prm  16631  3lcm2e6  16670  phicl2  16703  pockthi  16842  unbenlem  16843  prmrec  16857  vdwlem13  16928  vdwnn  16933  ramcl2  16951  prmgapprmo  16997  mod2xnegi  17006  modsubi  17007  structcnvcnv  17088  strleun  17092  setsres  17113  strfv  17139  starvndxnbasendx  17251  starvndxnplusgndx  17252  starvndxnmulrndx  17253  scandxnbasendx  17263  scandxnplusgndx  17264  scandxnmulrndx  17265  vscandxnbasendx  17268  vscandxnplusgndx  17269  vscandxnmulrndx  17270  vscandxnscandx  17271  ipndxnbasendx  17279  ipndxnplusgndx  17280  ipndxnmulrndx  17281  slotsdifipndx  17282  tsetndxnplusgndx  17304  tsetndxnmulrndx  17305  tsetndxnstarvndx  17306  slotstnscsi  17307  plendxnplusgndx  17318  plendxnmulrndx  17319  plendxnscandx  17320  plendxnvscandx  17321  slotsdifplendx  17322  basendxnocndx  17330  plendxnocndx  17331  dsndxnplusgndx  17337  dsndxnmulrndx  17338  slotsdnscsi  17339  dsndxntsetndx  17340  slotsdifdsndx  17341  unifndxntsetndx  17347  slotsdifunifndx  17348  slotsdifplendx2  17364  slotsdifocndx  17365  0rest  17377  firest  17380  restid  17381  prdsval  17403  prdsbas  17405  prdsplusg  17406  prdsmulr  17407  prdsvsca  17408  imasaddfnlem  17476  imasvscafn  17485  oppchomfvalOLD  17661  oppcbasOLD  17666  2oppchomf  17672  rescbasOLD  17779  resccoOLD  17783  rescabsOLD  17785  0ssc  17789  0subcat  17790  idfucl  17833  homarel  17988  dmaf  18001  cdaf  18002  setc2ohom  18047  catcfuccl  18071  catcfucclOLD  18072  relxpchom  18135  catcxpccl  18161  catcxpcclOLD  18162  oppchofcl  18215  oyoncl  18225  odubasOLD  18247  letsr  18548  mgmidmo  18581  efmndmgm  18768  smndex1ibas  18783  smndex1mgm  18790  smndex1mnd  18793  smndex2dbas  18797  smndex2dnrinv  18798  smndex2hbas  18799  pwmnd  18820  releqg  19057  ga0  19164  oppglemOLD  19217  psgnunilem3  19366  psgnunilem4  19367  pmtrsn  19389  efgval  19587  efger  19588  efgsval2  19603  efgsp1  19607  efgsfo  19609  efgredleme  19613  efgredlem  19617  efgred  19618  cygctb  19762  gsum2d2lem  19843  gsum2d2  19844  gsumcom2  19845  dprd2d2  19916  pgpfaclem1  19953  mgplemOLD  19994  mgpressOLD  20005  opprlemOLD  20160  reldvdsr  20178  00lsp  20597  sralemOLD  20797  srascaOLD  20805  sravscaOLD  20807  cnfldfun  20962  cnfldfunALT  20963  cnfldfunALTOLD  20964  xrsmgm  20986  znbaslemOLD  21097  resubdrg  21167  ocv0  21236  cssval  21241  thlbasOLD  21256  thlleOLD  21258  islinds2  21374  psrvscafval  21515  opsrbaslemOLD  21611  psrbag0  21629  00ply1bas  21769  ply1plusgfvi  21771  matscaOLD  21923  m2detleib  22140  tgdom  22488  tgidm  22490  indistps2ALT  22525  restbas  22669  resttopon  22672  rest0  22680  leordtval2  22723  iocpnfordt  22726  icomnfordt  22727  iooordt  22728  ist1-3  22860  1stcfb  22956  comppfsc  23043  1stckgen  23065  ptbasfi  23092  dfac14  23129  opnfbas  23353  hauspwpwf1  23498  alexsubALT  23562  ptcmplem5  23567  cnextrel  23574  ust0  23731  tuslemOLD  23779  0met  23879  prdsdsf  23880  prdsxmetlem  23881  prdsmet  23883  setsmsbasOLD  23989  setsmsdsOLD  23991  prdsbl  24007  tngdsOLD  24172  qtopbaslem  24282  xrtgioo  24329  xrsdsre  24333  zcld  24336  recld2  24337  reperflem  24341  retopconn  24352  iccpnfcnv  24467  bndth  24481  nmoleub2lem2  24639  zclmncvs  24672  recmet  24847  resscdrg  24882  ishl2  24894  recms  24904  volf  25053  iundisj2  25073  volsup  25080  icombl  25088  ioombl  25089  ismbf3d  25178  0plef  25196  0pledm  25197  itg1ge0  25210  mbfi1fseqlem5  25244  itg2addlem  25283  reldv  25394  limciun  25418  dvexp  25477  dveflem  25503  lhop1lem  25537  lhop  25540  elply2  25717  elplyd  25723  ply1term  25725  ply0  25729  plymullem  25737  qaa  25843  pserulm  25941  pserdvlem2  25947  efcn  25962  sincosq1lem  26014  tangtx  26022  sincos4thpi  26030  pigt3  26034  pige3ALT  26036  efif1olem4  26061  logf1o  26080  relogf1o  26082  log1  26101  loge  26102  relogiso  26113  dvrelog  26152  relogcn  26153  logcn  26162  cxpcn3  26263  resqrtcn  26264  2logb9irr  26307  leibpi  26454  log2ublem1  26458  birthday  26466  emcllem5  26511  harmonicbnd  26515  harmonicbnd2  26516  harmonicbnd3  26519  lgamgulm2  26547  lgamcvglem  26551  gamf  26554  ppiltx  26688  ppiublem1  26712  ppiub  26714  bclbnd  26790  bpos1lem  26792  bposlem8  26801  lgsquadlem2  26891  2sqlem9  26937  2sqlem10  26938  addsqnreup  26953  chebbnd1  26982  selberg2lem  27060  pntrsumo1  27075  selbergsb  27085  pntpbnd  27098  sltval2  27166  noxp1o  27173  nosepnelem  27189  noetasuplem2  27244  noetainflem2  27248  0slt1s  27338  addsf  27475  precsexlem1  27663  precsexlem2  27664  precsexlem3  27665  precsexlem4  27666  precsexlem5  27667  precsexlem9  27671  precsexlem10  27672  precsexlem11  27673  elons2  27695  lngndxnitvndx  27732  istrkg2ld  27749  tgcgr4  27820  ttgvalOLD  28165  ttglemOLD  28167  cchhllemOLD  28183  ax5seglem7  28231  axlowdimlem4  28241  axlowdimlem6  28243  axlowdimlem7  28244  axlowdimlem10  28247  axlowdimlem13  28250  axlowdimlem16  28253  uhgr0e  28369  uhgr0  28371  upgrbi  28391  umgrbi  28399  usgr0  28538  lfuhgr1v0e  28549  usgrexmpllem  28555  usgrexmpl  28558  griedg0prc  28559  cplgr0  28720  usgrexilem  28735  cffldtocusgr  28742  rgrusgrprc  28884  rusgrprc  28885  rgrprcx  28887  rgrx0ndm  28888  usgr2pthlem  29058  pthdlem2  29063  uspgrn2crct  29100  wwlksnext  29185  clwwlknondisj  29402  0ewlk  29405  0wlk  29407  0pth  29416  1pthdlem1  29426  1trld  29433  wlk2v2elem2  29447  wlk2v2e  29448  upgr3v3e3cycl  29471  upgr4cycl4dv4e  29476  dfconngr1  29479  0conngr  29483  konigsbergumgr  29542  2wspmdisj  29628  2clwwlk2clwwlk  29641  numclwwlk3lem2lem  29674  numclwwlk3lem2  29675  ex-dif  29714  ex-in  29716  ex-eprel  29724  ex-id  29725  ex-fl  29738  ex-mod  29740  ex-hash  29744  ex-fpar  29753  avril1  29754  2bornot2b  29755  0vfval  29897  vsfval  29924  ajmoi  30149  ajfuni  30150  normlem2  30402  norm3adifii  30439  hhip  30468  hlim0  30526  hlimcaui  30527  hlimf  30528  hhssnv  30555  shscli  30608  shsval2i  30678  h1de2i  30844  fh3i  30914  fh4i  30915  cm2mi  30917  qlaxr3i  30927  mayetes3i  31020  ho0f  31042  hoif  31045  hodidi  31078  ho0subi  31086  hosd1i  31113  adjmo  31123  nmopsetn0  31156  nmfnsetn0  31169  funadj  31177  funcnvadj  31184  nmcexi  31317  cnlnadjlem8  31365  nmoptri2i  31390  opsqrlem4  31434  hmopidmchi  31442  pjoci  31471  pjinvari  31482  abrexdomjm  31782  elim2ifim  31815  iundisj2f  31859  rinvf1o  31892  dfcnv2  31939  snct  31976  fzodif2  32041  iundisj2fi  32046  dp2lt10  32088  dp2ltc  32091  dplti  32109  dpgti  32110  dpexpp1  32112  gsumle  32283  xrge0slmod  32504  zarcls  32923  zartopn  32924  xrge0pluscn  32989  zlmdsOLD  33012  zlmtsetOLD  33014  qqhre  33069  esumrnmpt2  33135  esumfsup  33137  esumpcvgval  33145  hasheuni  33152  esumcvg  33153  esumcvgsum  33155  esumsup  33156  esum2d  33160  dmsigagen  33211  ldgenpisyslem3  33232  measvuni  33281  voliune  33296  volfiniune  33297  br2base  33337  dya2iocuni  33351  eulerpartlem1  33435  eulerpartlemt  33439  eulerpartgbij  33440  fib0  33467  coinfliprv  33550  ballotlem2  33556  ballotlemic  33574  ballotlem7  33603  ballotth  33605  plymul02  33626  rpsqrtcn  33674  chtvalz  33710  circlemethnat  33722  circlevma  33723  circlemethhgt  33724  hgt750lem  33732  bnj226  33814  bnj1101  33864  bnj110  33938  bnj149  33955  bnj150  33956  bnj151  33957  bnj517  33965  bnj580  33993  bnj865  34003  bnj900  34009  bnj996  34036  bnj1110  34062  bnj1133  34069  bnj1128  34070  bnj1145  34073  bnj1137  34075  bnj1171  34080  bnj1176  34085  f1resfz0f1d  34172  subfacp1lem5  34244  subfacp1lem6  34245  kur14lem9  34274  cvmcov2  34335  cvmliftlem1  34345  cvmliftlem4  34348  cvmliftlem5  34349  gonanegoal  34412  satfv0  34418  satfv0fun  34431  fmlan0  34451  gonan0  34452  fmla0disjsuc  34458  ex-sategoelel12  34487  msrfo  34606  problem5  34723  brtpid1  34765  brtpid2  34766  brtpid3  34767  logi  34779  faclimlem1  34788  axextndbi  34851  txprel  34926  relsset  34935  relbigcup  34944  fvbigcup  34949  fnsingle  34966  fvsingle  34967  snelsingles  34969  funimage  34975  fullfunfnv  34993  imagesset  35000  funtransport  35078  colinrel  35104  funray  35187  funline  35189  0hf  35224  gg-cnfldfun  35272  gg-cnfldfunALT  35273  gg-cffldtocusgr  35274  neibastop2lem  35337  filnetlem3  35357  nrmo  35387  waj-ax  35391  lukshef-ax2  35392  arg-ax  35393  limsucncmpi  35422  dnizeq0  35443  knoppcnlem8  35468  knoppcnlem11  35471  cnndvlem1  35505  bj-babylob  35574  bj-ax12ssb  35627  bj-nnfnth  35713  bj-snsetex  35936  bj-0eltag  35951  bj-2upln0  35996  bj-2upln1upl  35997  bj-snexg  36007  bj-unexg  36011  bj-adjg1  36016  f1omptsnlem  36309  f1omptsn  36310  icoreresf  36325  relowlssretop  36336  relowlpssretop  36337  domalom  36377  matunitlindf  36578  poimirlem3  36583  poimirlem9  36589  poimirlem16  36596  poimirlem17  36597  poimirlem18  36598  poimirlem19  36599  poimirlem20  36600  poimirlem26  36606  mblfinlem1  36617  mblfinlem2  36618  ismblfin  36621  voliunnfl  36624  cnambfre  36628  abrexdom  36690  fdc  36705  cncfres  36725  heibor1lem  36769  grposnOLD  36842  bicontr  37040  an12i  37058  tsim1  37090  ac6s6f  37133  vvdifopab  37220  brcnvrabga  37303  opabf  37329  xrnrel  37335  relcoels  37386  cnvcosseq  37399  refrelcoss3  37425  refrelcoss2  37426  symrelcoss2  37428  refrelcoss  37485  symrelcoss  37522  n0eldmqs  37610  ax13fromc9  37868  dedths  37924  renegclALT  37925  hlhilslemOLD  40902  12gcd5e1  40960  60gcd7e1  40962  lcmineqlem23  41008  dvrelog2  41021  dvrelog3  41022  dvrelog2b  41023  aks4d1p1p6  41030  aks4d1p1p7  41031  aks4d1p1  41033  sticksstones22  41076  2xp3dxp2ge1d  41114  sn-axprlem3  41126  rtprmirr  41325  acos1half  41503  moxfr  41518  mapfzcons1  41543  diophrw  41585  0dioph  41604  vdioph  41605  rabren3dioph  41641  2nn0ind  41772  rpnnen3  41859  kelac2lem  41894  frlmpwfi  41928  oaordnrex  42133  omnord1ex  42142  oenord1ex  42153  oaomoencom  42155  ifpbiidcor2  42322  iscard4  42372  sqrtcval  42480  resqrtvalex  42484  eliunov2  42518  xphe  42620  0he  42621  he0  42623  snhesn  42625  idhe  42626  frege54cor1c  42754  clsk1independent  42885  neicvgnvor  42955  amgm2d  43038  amgm3d  43039  amgm4d  43040  ismnushort  43148  lhe4.4ex1a  43176  rusbcALT  43286  ipo0  43296  ifr0  43297  vk15.4j  43377  2sb5nd  43409  dfvd1ir  43422  dfvd2anir  43433  dfvd2ir  43435  dfvd3ir  43442  dfvd3anir  43445  iden2  43463  e0bir  43626  uun2221p1  43663  uun2221p2  43664  2sb5ndVD  43759  2sb5ndALT  43781  iunconnlem2  43784  fnchoice  43801  unisn0  43829  eliincex  43887  icof  44003  fnmptif  44055  supminfxr  44259  rexanuz2nf  44288  fsumiunss  44376  climlimsupcex  44570  liminfltlimsupex  44582  liminflelimsupcex  44598  xlimrel  44621  xlimfun  44656  resincncf  44676  dvnprodlem3  44749  volioc  44773  volico  44784  dmvolss  44786  volioof  44788  stoweidlem13  44814  stoweidlem34  44835  stirlinglem5  44879  stirlinglem13  44887  stirlingr  44891  fourierdlem42  44950  fourierdlem62  44969  fouriersw  45032  etransc  45084  salexct  45135  salexct2  45140  salgencntex  45144  sge0rnn0  45169  gsumge0cl  45172  sge00  45177  sge0resplit  45207  sge0reuz  45248  omeiunle  45318  0ome  45330  icoresmbl  45344  ovn0lem  45366  ovnhoilem1  45402  hspmbl  45430  nsssmfmbf  45580  mbfpsssmf  45584  smfresal  45589  smfmullem4  45595  smfpimbor1lem1  45599  smfpimbor1lem2  45600  aistia  45692  aisfina  45693  aiffnbandciffatnotciffb  45699  axorbciffatcxorb  45700  abnotbtaxb  45710  abnotataxb  45711  eusnsn  45821  aiotaval  45888  aiota0ndef  45890  fundcmpsurinjimaid  46164  ichv  46202  ichf  46203  ichid  46204  icht  46205  ichcircshi  46207  icheq  46215  spr0nelg  46229  m3prm  46345  m7prm  46353  0noddALTV  46442  2noddALTV  46446  341fppr2  46487  9fppr8  46490  nfermltl8rev  46495  nfermltl2rev  46496  nfermltlrev  46497  sbgoldbo  46540  nnsum3primes4  46541  evengpop3  46551  oddinmgm  46670  nn0mnd  46674  pzriprnglem8  46897  pzriprnglem13  46902  pzriprnglem14  46903  pzriprngALT  46904  2zrngamgm  46922  2zrngaabl  46927  2zrngmmgm  46929  2zrngnring  46935  fldhmsubc  47067  fldhmsubcALTV  47085  eliunxp2  47094  zlmodzxzldeplem  47263  zlmodzxzldep  47269  ldepslinc  47274  rrx2xpreen  47489  rrx2plordisom  47493  line2ylem  47521  line2  47522  line2x  47524  inlinecirc02plem  47556  mosn  47581  mof0  47588  mof0ALT  47590  f1omo  47611  prstclevalOLD  47773  prstcocvalOLD  47776  ex-gte  47858  empty-surprise  47913  eximp-surprise2  47916  amgmw2d  47935