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  711  imorri  855  orri  862  mpbir3an  1342  xorexmid  1527  tru  1544  had1  1603  nic-mpALT  1672  nic-ax  1673  nic-axALT  1674  nfi  1788  mpgbir  1799  nfxfr  1853  19.35ri  1879  ax5e  1912  ax6ev  1969  equsb1v  2106  ax13  2374  ax13ALT  2424  moanmo  2616  axi12  2700  axbnd  2701  axexte  2703  axextmo  2706  nulmo  2707  vexw  2714  eqeltri  2825  nfcxfr  2890  neir  2929  neirr  2935  eqnetri  2996  nelir  3033  mprgbir  3052  cbvrexdva2OLD  3325  issetri  3469  moeq  3681  rmoeq  3712  cdeqi  3739  eqsstri  3996  rmo0  4328  rabnc  4357  reuprg  4670  tpid1  4735  tpid2  4737  mosneq  4809  pwv  4871  uni0  4902  int0  4929  eqbrtri  5131  tr0  5230  trv  5231  zfrep4  5251  axnulALT  5262  0ex  5265  inex1  5275  elpwi2  5293  0elpw  5314  axpow2  5325  dvdemo1  5331  vpwex  5335  zfpair2  5391  exss  5426  brv  5435  opwo0id  5460  moop2  5465  0sn0ep  5545  po0  5566  epse  5623  relxp  5659  rel0  5765  relopabiv  5786  relopabi  5788  relopabiALT  5789  eliunxp  5804  opeliunxp2  5805  dmi  5888  dmep  5890  xpidtr  6098  xpima  6158  dmsn0  6185  cnvsn0  6186  0elon  6390  funmpt  6557  funmpt2  6558  funcnv0  6585  isarep2  6611  fresaunres2  6735  f0  6744  f10d  6837  f1o00  6838  f1oi  6841  f1osn  6843  brprcneu  6851  brprcneuALT  6852  opabiotafun  6944  fvopab3ig  6967  opabex  7197  eufnfv  7206  isof1oopb  7303  ncanth  7345  mpofun  7516  reldmmpo  7526  ovid  7533  ovidig  7534  ovidi  7535  ovig  7538  ov3  7555  caovmo  7629  relmptopab  7642  porpss  7706  uniex2  7717  tfinds2  7843  finds  7875  finds2  7877  oprabex  7958  oprabex3  7959  f1stres  7995  f2ndres  7996  relmpoopab  8076  fsplitfpar  8100  poseq  8140  opeliunxp2f  8192  tpos0  8238  issmo  8320  tfrlem6  8353  tfrlem8  8355  tfrlem16  8364  tfr1a  8365  tfr1  8368  tz7.44lem1  8376  seqomlem2  8422  seqomlem3  8423  seqomlem4  8424  fnseqom  8426  ord3  8452  0lt1o  8471  0we1  8473  naddf  8648  eqer  8710  ecopover  8797  mapsnf1o3  8871  ssdomg  8974  en0  8992  en0r  8994  ensn1  8995  0fi  9016  snfiOLD  9018  enrefnn  9021  xpcomf1o  9035  map2xp  9117  limensuci  9123  1sdom2  9194  sdom1  9196  sdom1OLD  9197  unblem4  9249  fidomdm  9292  marypha1lem  9391  hartogslem1  9502  hartogs  9504  card2on  9514  nelaneq  9559  epinid0  9560  ruALT  9563  disjcsn  9564  elnanel  9567  cnvepnep  9568  inf2  9583  inf3lem6  9593  infeq5i  9596  zfinf2  9602  cantnflt  9632  cnfcom  9660  trcl  9688  tz9.1c  9690  tc2  9702  r1funlim  9726  r1fnon  9727  karden  9855  tskwe  9910  cardprclem  9939  pm54.43  9961  r0weon  9972  iunmapdisj  9983  alephfnon  10025  alephfplem4  10067  alephfp  10068  alephval3  10070  kmlem2  10112  dju1dif  10133  ackbij1  10197  ackbij2lem2  10199  ackbij2  10202  infpssrlem3  10265  hsmexlem4  10389  hsmexlem5  10390  ac2  10421  axac3  10424  ac6  10440  axdclem2  10480  dmct  10484  ondomon  10523  alephsucpw  10530  pwcfsdom  10543  cfpwsdom  10544  smobeth  10546  axpowndlem3  10559  zfcndun  10575  zfcndpow  10576  zfcndinf  10578  zfcndac  10579  wunex2  10698  uniwun  10700  wuncval2  10707  grur1  10780  axgroth5  10784  axgroth2  10785  axgroth6  10788  axgroth3  10791  grothtsk  10795  inaprc  10796  ltsopi  10848  dmaddpi  10850  dmmulpi  10851  1lt2pi  10865  nqerf  10890  addnqf  10908  mulnqf  10909  1lt2nq  10933  m1p1sr  11052  m1m1sr  11053  0lt1sr  11055  axaddf  11105  axmulf  11106  ax1cn  11109  subaddrii  11518  ixi  11814  recgt0ii  12096  nn1suc  12215  4d2e2  12358  arch  12446  un0mulcl  12483  pnf0xnn0  12529  3halfnz  12620  nummac  12701  indstr  12882  mnfltpnf  13093  ioof  13415  0nelfz1  13511  fzp1disj  13551  fzp1nel  13579  fzof  13624  fvf1tp  13758  om2uzrani  13924  om2uzf1oi  13925  uzrdglem  13929  uzrdgfni  13930  uzrdg0i  13931  ltwenn  13934  hashgf1o  13943  axdc4uzlem  13955  sq0  14164  irec  14173  facmapnn  14257  hashkf  14304  hashfxnn0  14309  hashf  14310  hash0  14339  prhash2ex  14371  hashsslei  14398  hashxplem  14405  hashbclem  14424  hashf1lem1  14427  tpf1ofv0  14468  tpfo  14472  s1dm  14580  eqs1  14584  ccat2s1p1  14601  cats1un  14693  revs1  14737  0csh0  14765  cshw1  14794  cats1fvn  14831  funcnvs1  14885  pfx2  14920  relexp0g  14995  relexpsucnnr  14998  rtrclreclem1  15030  dfrtrclrec2  15031  rtrclreclem2  15032  rtrclreclem4  15034  dfrtrcl2  15035  climmo  15530  fsumcom2  15747  ackbijnn  15801  incexclem  15809  infcvgaux1i  15830  fprodcom2  15957  bpolylem  16021  bpoly3  16031  bpoly4  16032  efcvgfsum  16059  cos1bnd  16162  cos2bnd  16163  znnen  16187  qnnen  16188  aleph1re  16220  3dvds  16308  n2dvdsm1  16346  divalglem5  16374  flodddiv4  16392  sadcaddlem  16434  sadadd2lem  16436  sadadd3  16438  sadaddlem  16443  lcmf0  16611  lcmfunsnlem2lem1  16615  lcmfunsnlem2  16617  coprmprod  16638  coprmproddvdslem  16639  2prm  16669  3lcm2e6  16709  phicl2  16745  pockthi  16885  unbenlem  16886  prmrec  16900  vdwlem13  16971  vdwnn  16976  ramcl2  16994  prmgapprmo  17040  mod2xnegi  17049  modsubi  17050  structcnvcnv  17130  strleun  17134  setsres  17155  strfv  17180  starvndxnbasendx  17274  starvndxnplusgndx  17275  starvndxnmulrndx  17276  scandxnbasendx  17286  scandxnplusgndx  17287  scandxnmulrndx  17288  vscandxnbasendx  17291  vscandxnplusgndx  17292  vscandxnmulrndx  17293  vscandxnscandx  17294  ipndxnbasendx  17302  ipndxnplusgndx  17303  ipndxnmulrndx  17304  slotsdifipndx  17305  tsetndxnplusgndx  17327  tsetndxnmulrndx  17328  tsetndxnstarvndx  17329  slotstnscsi  17330  plendxnplusgndx  17341  plendxnmulrndx  17342  plendxnscandx  17343  plendxnvscandx  17344  slotsdifplendx  17345  basendxnocndx  17353  plendxnocndx  17354  dsndxnplusgndx  17360  dsndxnmulrndx  17361  slotsdnscsi  17362  dsndxntsetndx  17363  slotsdifdsndx  17364  unifndxntsetndx  17370  slotsdifunifndx  17371  slotsdifplendx2  17386  slotsdifocndx  17387  0rest  17399  firest  17402  restid  17403  prdsval  17425  prdsbas  17427  prdsplusg  17428  prdsmulr  17429  prdsvsca  17430  imasaddfnlem  17498  imasvscafn  17507  2oppchomf  17692  0ssc  17806  0subcat  17807  idfucl  17850  homarel  18005  dmaf  18018  cdaf  18019  setc2ohom  18064  catcfuccl  18087  relxpchom  18149  catcxpccl  18175  oppchofcl  18228  oyoncl  18238  letsr  18559  mgmidmo  18594  efmndmgm  18819  smndex1ibas  18834  smndex1mgm  18841  smndex1mnd  18844  smndex2dbas  18848  smndex2dnrinv  18849  smndex2hbas  18850  pwmnd  18871  releqg  19114  ga0  19237  psgnunilem3  19433  psgnunilem4  19434  pmtrsn  19456  efgval  19654  efger  19655  efgsval2  19670  efgsp1  19674  efgsfo  19676  efgredleme  19680  efgredlem  19684  efgred  19685  cygctb  19829  gsum2d2lem  19910  gsum2d2  19911  gsumcom2  19912  dprd2d2  19983  pgpfaclem1  20020  reldvdsr  20276  fldhmsubc  20701  00lsp  20894  cnfldfun  21285  cnfldfunALT  21286  cnfldfunOLD  21298  cnfldfunALTOLD  21299  xrsmgm  21325  pzriprnglem8  21405  pzriprnglem13  21410  pzriprnglem14  21411  pzriprngALT  21412  resubdrg  21524  ocv0  21593  cssval  21598  islinds2  21729  psrvscafval  21864  psrbag0  21976  psdmvr  22063  00ply1bas  22131  ply1plusgfvi  22133  m2detleib  22525  tgdom  22872  tgidm  22874  indistps2ALT  22908  restbas  23052  resttopon  23055  rest0  23063  leordtval2  23106  iocpnfordt  23109  icomnfordt  23110  iooordt  23111  ist1-3  23243  1stcfb  23339  comppfsc  23426  1stckgen  23448  ptbasfi  23475  dfac14  23512  opnfbas  23736  hauspwpwf1  23881  alexsubALT  23945  ptcmplem5  23950  cnextrel  23957  ust0  24114  0met  24261  prdsdsf  24262  prdsxmetlem  24263  prdsmet  24265  prdsbl  24386  qtopbaslem  24653  xrtgioo  24702  xrsdsre  24706  zcld  24709  recld2  24710  reperflem  24714  retopconn  24725  iccpnfcnv  24849  bndth  24864  nmoleub2lem2  25023  zclmncvs  25055  recmet  25230  resscdrg  25265  ishl2  25277  recms  25287  volf  25437  iundisj2  25457  volsup  25464  icombl  25472  ioombl  25473  ismbf3d  25562  0plef  25580  0pledm  25581  itg1ge0  25594  mbfi1fseqlem5  25627  itg2addlem  25666  reldv  25778  limciun  25802  dvexp  25864  dveflem  25890  lhop1lem  25925  lhop  25928  elply2  26108  elplyd  26114  ply1term  26116  ply0  26120  plymullem  26128  qaa  26238  pserulm  26338  pserdvlem2  26345  efcn  26360  sincosq1lem  26413  tangtx  26421  sincos4thpi  26429  pigt3  26434  pige3ALT  26436  efif1olem4  26461  logf1o  26480  relogf1o  26482  log1  26501  loge  26502  logi  26503  relogiso  26514  dvrelog  26553  relogcn  26554  logcn  26563  cxpcn3  26665  resqrtcn  26666  rtprmirr  26677  2logb9irr  26712  leibpi  26859  log2ublem1  26863  birthday  26871  emcllem5  26917  harmonicbnd  26921  harmonicbnd2  26922  harmonicbnd3  26925  lgamgulm2  26953  lgamcvglem  26957  gamf  26960  ppiltx  27094  ppiublem1  27120  ppiub  27122  bclbnd  27198  bpos1lem  27200  bposlem8  27209  lgsquadlem2  27299  2sqlem9  27345  2sqlem10  27346  addsqnreup  27361  chebbnd1  27390  selberg2lem  27468  pntrsumo1  27483  selbergsb  27493  pntpbnd  27506  sltval2  27575  noxp1o  27582  nosepnelem  27598  noetasuplem2  27653  noetainflem2  27657  0slt1s  27748  addsf  27896  precsexlem1  28116  precsexlem2  28117  precsexlem3  28118  precsexlem4  28119  precsexlem5  28120  precsexlem9  28124  precsexlem10  28125  precsexlem11  28126  elons2  28166  onscutlt  28172  onsiso  28176  onswe  28177  onsse  28178  onaddscl  28181  onmulscl  28182  eln0s  28258  0zs  28283  zseo  28315  twocut  28316  lngndxnitvndx  28377  istrkg2ld  28394  tgcgr4  28465  ax5seglem7  28869  axlowdimlem4  28879  axlowdimlem6  28881  axlowdimlem7  28882  axlowdimlem10  28885  axlowdimlem13  28888  axlowdimlem16  28891  uhgr0e  29005  uhgr0  29007  upgrbi  29027  umgrbi  29035  usgr0  29177  lfuhgr1v0e  29188  usgrexmpllem  29194  usgrexmpl  29197  griedg0prc  29198  cplgr0  29359  usgrexilem  29374  cffldtocusgr  29381  cffldtocusgrOLD  29382  rgrusgrprc  29524  rusgrprc  29525  rgrprcx  29527  rgrx0ndm  29528  usgr2pthlem  29700  pthdlem2  29705  uspgrn2crct  29745  wwlksnext  29830  clwwlknondisj  30047  0ewlk  30050  0wlk  30052  0pth  30061  1pthdlem1  30071  1trld  30078  wlk2v2elem2  30092  wlk2v2e  30093  upgr3v3e3cycl  30116  upgr4cycl4dv4e  30121  dfconngr1  30124  0conngr  30128  konigsbergumgr  30187  2wspmdisj  30273  2clwwlk2clwwlk  30286  numclwwlk3lem2lem  30319  numclwwlk3lem2  30320  ex-dif  30359  ex-in  30361  ex-eprel  30369  ex-id  30370  ex-fl  30383  ex-mod  30385  ex-hash  30389  ex-fpar  30398  avril1  30399  2bornot2b  30400  0vfval  30542  vsfval  30569  ajmoi  30794  ajfuni  30795  normlem2  31047  norm3adifii  31084  hhip  31113  hlim0  31171  hlimcaui  31172  hlimf  31173  hhssnv  31200  shscli  31253  shsval2i  31323  h1de2i  31489  fh3i  31559  fh4i  31560  cm2mi  31562  qlaxr3i  31572  mayetes3i  31665  ho0f  31687  hoif  31690  hodidi  31723  ho0subi  31731  hosd1i  31758  adjmo  31768  nmopsetn0  31801  nmfnsetn0  31814  funadj  31822  funcnvadj  31829  nmcexi  31962  cnlnadjlem8  32010  nmoptri2i  32035  opsqrlem4  32079  hmopidmchi  32087  pjoci  32116  pjinvari  32127  abrexdomjm  32443  elim2ifim  32481  iundisj2f  32526  rinvf1o  32561  dfcnv2  32607  snct  32644  fzodif2  32721  iundisj2fi  32727  dp2lt10  32811  dp2ltc  32814  dplti  32832  dpgti  32833  dpexpp1  32835  s1chn  32943  chnub  32945  gsumle  33045  xrge0slmod  33326  isconstr  33733  zarcls  33871  zartopn  33872  xrge0pluscn  33937  qqhre  34017  esumrnmpt2  34065  esumfsup  34067  esumpcvgval  34075  hasheuni  34082  esumcvg  34083  esumcvgsum  34085  esumsup  34086  esum2d  34090  dmsigagen  34141  ldgenpisyslem3  34162  measvuni  34211  voliune  34226  volfiniune  34227  br2base  34267  dya2iocuni  34281  eulerpartlem1  34365  eulerpartlemt  34369  eulerpartgbij  34370  fib0  34397  coinfliprv  34481  ballotlem2  34487  ballotlemic  34505  ballotlem7  34534  ballotth  34536  plymul02  34544  rpsqrtcn  34591  chtvalz  34627  circlemethnat  34639  circlevma  34640  circlemethhgt  34641  hgt750lem  34649  bnj226  34731  bnj1101  34781  bnj110  34855  bnj149  34872  bnj150  34873  bnj151  34874  bnj517  34882  bnj580  34910  bnj865  34920  bnj900  34926  bnj996  34953  bnj1110  34979  bnj1133  34986  bnj1128  34987  bnj1145  34990  bnj1137  34992  bnj1171  34997  bnj1176  35002  f1resfz0f1d  35108  subfacp1lem5  35178  subfacp1lem6  35179  kur14lem9  35208  cvmcov2  35269  cvmliftlem1  35279  cvmliftlem4  35282  cvmliftlem5  35283  gonanegoal  35346  satfv0  35352  satfv0fun  35365  fmlan0  35385  gonan0  35386  fmla0disjsuc  35392  ex-sategoelel12  35421  msrfo  35540  problem5  35663  brtpid1  35715  brtpid2  35716  brtpid3  35717  faclimlem1  35737  axextndbi  35799  txprel  35874  relsset  35883  relbigcup  35892  fvbigcup  35897  fnsingle  35914  fvsingle  35915  snelsingles  35917  funimage  35923  fullfunfnv  35941  imagesset  35948  funtransport  36026  colinrel  36052  funray  36135  funline  36137  0hf  36172  neibastop2lem  36355  filnetlem3  36375  nrmo  36405  waj-ax  36409  lukshef-ax2  36410  arg-ax  36411  limsucncmpi  36440  dnizeq0  36470  knoppcnlem8  36495  knoppcnlem11  36498  cnndvlem1  36532  bj-babylob  36599  bj-ax12ssb  36653  bj-nnfnth  36738  bj-snsetex  36958  bj-0eltag  36973  bj-2upln0  37018  bj-2upln1upl  37019  bj-snexg  37029  bj-unexg  37033  bj-adjg1  37038  f1omptsnlem  37331  f1omptsn  37332  icoreresf  37347  relowlssretop  37358  relowlpssretop  37359  domalom  37399  matunitlindf  37619  poimirlem3  37624  poimirlem9  37630  poimirlem16  37637  poimirlem17  37638  poimirlem18  37639  poimirlem19  37640  poimirlem20  37641  poimirlem26  37647  mblfinlem1  37658  mblfinlem2  37659  ismblfin  37662  voliunnfl  37665  cnambfre  37669  abrexdom  37731  fdc  37746  cncfres  37766  heibor1lem  37810  grposnOLD  37883  bicontr  38081  an12i  38099  tsim1  38131  ac6s6f  38174  vvdifopab  38256  brcnvrabga  38331  opabf  38357  xrnrel  38362  relcoels  38422  cnvcosseq  38435  refrelcoss3  38461  refrelcoss2  38462  symrelcoss2  38464  refrelcoss  38521  symrelcoss  38558  n0eldmqs  38646  ax13fromc9  38906  dedths  38962  renegclALT  38963  12gcd5e1  41998  60gcd7e1  42000  lcmineqlem23  42046  dvrelog2  42059  dvrelog3  42060  dvrelog2b  42061  aks4d1p1p6  42068  aks4d1p1p7  42069  aks4d1p1  42071  sticksstones22  42163  sn-axprlem3  42212  acos1half  42353  moxfr  42687  mapfzcons1  42712  diophrw  42754  0dioph  42773  vdioph  42774  rabren3dioph  42810  2nn0ind  42941  rpnnen3  43028  kelac2lem  43060  frlmpwfi  43094  oaordnrex  43291  omnord1ex  43300  oenord1ex  43311  oaomoencom  43313  ifpbiidcor2  43479  iscard4  43529  sqrtcval  43637  resqrtvalex  43641  eliunov2  43675  xphe  43777  0he  43778  he0  43780  snhesn  43782  idhe  43783  frege54cor1c  43911  clsk1independent  44042  neicvgnvor  44112  amgm2d  44194  amgm3d  44195  amgm4d  44196  ismnushort  44297  lhe4.4ex1a  44325  rusbcALT  44435  ipo0  44445  ifr0  44446  vk15.4j  44525  2sb5nd  44557  dfvd1ir  44570  dfvd2anir  44581  dfvd2ir  44583  dfvd3ir  44590  dfvd3anir  44593  iden2  44611  e0bir  44773  uun2221p1  44810  uun2221p2  44811  2sb5ndVD  44906  2sb5ndALT  44928  iunconnlem2  44931  trwf  44956  wfaxext  44990  wfaxpow  44994  wfaxinf2  44998  wfac8prim  44999  permaxinf2lem  45009  nregmodelf1o  45012  fnchoice  45030  unisn0  45055  eliincex  45111  icof  45220  fnmptif  45266  supminfxr  45467  rexanuz2nf  45495  fsumiunss  45580  climlimsupcex  45774  liminfltlimsupex  45786  liminflelimsupcex  45802  xlimrel  45825  xlimfun  45860  resincncf  45880  dvnprodlem3  45953  volioc  45977  volico  45988  dmvolss  45990  volioof  45992  stoweidlem13  46018  stoweidlem34  46039  stirlinglem5  46083  stirlinglem13  46091  stirlingr  46095  fourierdlem42  46154  fourierdlem62  46173  fouriersw  46236  etransc  46288  salexct  46339  salexct2  46344  salgencntex  46348  sge0rnn0  46373  gsumge0cl  46376  sge00  46381  sge0resplit  46411  sge0reuz  46452  omeiunle  46522  0ome  46534  icoresmbl  46548  ovn0lem  46570  ovnhoilem1  46606  hspmbl  46634  nsssmfmbf  46784  mbfpsssmf  46788  smfresal  46793  smfmullem4  46799  smfpimbor1lem1  46803  smfpimbor1lem2  46804  lambert0  46895  lamberte  46896  aistia  46902  aisfina  46903  aiffnbandciffatnotciffb  46909  axorbciffatcxorb  46910  abnotbtaxb  46920  abnotataxb  46921  eusnsn  47031  aiotaval  47100  aiota0ndef  47102  fundcmpsurinjimaid  47416  ichv  47454  ichf  47455  ichid  47456  icht  47457  ichcircshi  47459  icheq  47467  spr0nelg  47481  m3prm  47597  m7prm  47605  0noddALTV  47694  2noddALTV  47698  341fppr2  47739  9fppr8  47742  nfermltl8rev  47747  nfermltl2rev  47748  nfermltlrev  47749  sbgoldbo  47792  nnsum3primes4  47793  evengpop3  47803  stgr1  47964  usgrexmpl1lem  48016  usgrexmpl1  48017  usgrexmpl1tri  48020  usgrexmpl2lem  48021  usgrexmpl2  48022  usgrexmpl2nb0  48026  usgrexmpl2nb1  48027  usgrexmpl2nb2  48028  usgrexmpl2nb3  48029  usgrexmpl2nb4  48030  usgrexmpl2nb5  48031  gpgedg2ov  48061  gpgedg2iv  48062  gpg5nbgrvtx03starlem1  48063  gpg5nbgrvtx03starlem2  48064  gpg5nbgrvtx03starlem3  48065  gpg5nbgrvtx13starlem1  48066  gpg5nbgrvtx13starlem2  48067  gpg5nbgrvtx13starlem3  48068  gpg5grlic  48088  gpgprismgr4cycllem2  48090  gpgprismgr4cycllem7  48095  pg4cyclnex  48121  oddinmgm  48167  nn0mnd  48171  2zrngamgm  48237  2zrngaabl  48242  2zrngmmgm  48244  2zrngnring  48250  fldhmsubcALTV  48325  eliunxp2  48326  zlmodzxzldeplem  48491  zlmodzxzldep  48497  ldepslinc  48502  rrx2xpreen  48712  rrx2plordisom  48716  line2ylem  48744  line2  48745  line2x  48747  inlinecirc02plem  48779  mosn  48805  mof0  48830  mof0ALT  48832  tposrescnv  48871  tposres3  48873  tposideq2  48881  f1omoOLD  48886  nelsubc3  49064  reldmxpc  49239  reldmprcof1  49374  setc1onsubc  49595  reldmlmd2  49646  reldmcmd2  49647  rellmd  49652  relcmd  49653  ex-gte  49722  empty-surprise  49775  eximp-surprise2  49778  amgmw2d  49797