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  2105  ax13  2379  ax13ALT  2429  moanmo  2621  axi12  2705  axbnd  2706  axexte  2708  axextmo  2711  nulmo  2712  vexw  2719  eqeltri  2830  nfcxfr  2896  neir  2935  neirr  2941  eqnetri  3002  nelir  3039  mprgbir  3058  cbvrexdva2OLD  3329  issetri  3478  moeq  3690  rmoeq  3721  cdeqi  3748  eqsstri  4005  rmo0  4337  rabnc  4366  reuprg  4679  tpid1  4744  tpid2  4746  mosneq  4818  pwv  4880  uni0  4911  int0  4938  eqbrtri  5140  tr0  5242  trv  5243  zfrep4  5263  axnulALT  5274  0ex  5277  inex1  5287  elpwi2  5305  0elpw  5326  axpow2  5337  dvdemo1  5343  vpwex  5347  zfpair2  5403  exss  5438  brv  5447  opwo0id  5472  moop2  5477  0sn0ep  5557  po0  5578  epse  5636  relxp  5672  rel0  5778  relopabiv  5799  relopabi  5801  relopabiALT  5802  eliunxp  5817  opeliunxp2  5818  dmi  5901  dmep  5903  xpidtr  6111  xpima  6171  dmsn0  6198  cnvsn0  6199  0elon  6407  funmpt  6573  funmpt2  6574  funcnv0  6601  isarep2  6627  fresaunres2  6749  f0  6758  f10d  6851  f1o00  6852  f1oi  6855  f1osn  6857  brprcneu  6865  brprcneuALT  6866  opabiotafun  6958  fvopab3ig  6981  opabex  7211  eufnfv  7220  isof1oopb  7317  ncanth  7358  mpofun  7529  reldmmpo  7539  ovid  7546  ovidig  7547  ovidi  7548  ovig  7551  ov3  7568  caovmo  7642  relmptopab  7655  porpss  7719  uniex2  7730  tfinds2  7857  finds  7890  finds2  7892  oprabex  7973  oprabex3  7974  f1stres  8010  f2ndres  8011  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  8514  0we1  8516  naddf  8691  eqer  8753  ecopover  8833  mapsnf1o3  8907  ssdomg  9012  en0  9030  en0r  9032  ensn1  9033  0fi  9054  snfiOLD  9056  enrefnn  9059  xpcomf1o  9073  map2xp  9159  limensuci  9165  1sdom2  9246  sdom1  9248  sdom1OLD  9249  unblem4  9301  fidomdm  9344  marypha1lem  9443  hartogslem1  9554  hartogs  9556  card2on  9566  nelaneq  9611  epinid0  9612  ruALT  9615  disjcsn  9616  elnanel  9619  cnvepnep  9620  inf2  9635  inf3lem6  9645  infeq5i  9648  zfinf2  9654  cantnflt  9684  cnfcom  9712  trcl  9740  tz9.1c  9742  tc2  9754  r1funlim  9778  r1fnon  9779  karden  9907  tskwe  9962  cardprclem  9991  pm54.43  10013  r0weon  10024  iunmapdisj  10035  alephfnon  10077  alephfplem4  10119  alephfp  10120  alephval3  10122  kmlem2  10164  dju1dif  10185  ackbij1  10249  ackbij2lem2  10251  ackbij2  10254  infpssrlem3  10317  hsmexlem4  10441  hsmexlem5  10442  ac2  10473  axac3  10476  ac6  10492  axdclem2  10532  dmct  10536  ondomon  10575  alephsucpw  10582  pwcfsdom  10595  cfpwsdom  10596  smobeth  10598  axpowndlem3  10611  zfcndun  10627  zfcndpow  10628  zfcndinf  10630  zfcndac  10631  wunex2  10750  uniwun  10752  wuncval2  10759  grur1  10832  axgroth5  10836  axgroth2  10837  axgroth6  10840  axgroth3  10843  grothtsk  10847  inaprc  10848  ltsopi  10900  dmaddpi  10902  dmmulpi  10903  1lt2pi  10917  nqerf  10942  addnqf  10960  mulnqf  10961  1lt2nq  10985  m1p1sr  11104  m1m1sr  11105  0lt1sr  11107  axaddf  11157  axmulf  11158  ax1cn  11161  subaddrii  11570  ixi  11864  recgt0ii  12146  nn1suc  12260  neg1lt0  12355  4d2e2  12408  arch  12496  un0mulcl  12533  pnf0xnn0  12579  3halfnz  12670  nummac  12751  indstr  12930  mnfltpnf  13140  ioof  13462  0nelfz1  13558  fzp1disj  13598  fzp1nel  13626  fzof  13671  fvf1tp  13804  om2uzrani  13968  om2uzf1oi  13969  uzrdglem  13973  uzrdgfni  13974  uzrdg0i  13975  ltwenn  13978  hashgf1o  13987  axdc4uzlem  13999  sq0  14208  irec  14217  facmapnn  14301  hashkf  14348  hashfxnn0  14353  hashf  14354  hash0  14383  prhash2ex  14415  hashsslei  14442  hashxplem  14449  hashbclem  14468  hashf1lem1  14471  tpf1ofv0  14512  tpfo  14516  s1dm  14624  eqs1  14628  ccat2s1p1  14645  cats1un  14737  revs1  14781  0csh0  14809  cshw1  14838  cats1fvn  14875  funcnvs1  14929  pfx2  14964  relexp0g  15039  relexpsucnnr  15042  rtrclreclem1  15074  dfrtrclrec2  15075  rtrclreclem2  15076  rtrclreclem4  15078  dfrtrcl2  15079  climmo  15571  fsumcom2  15788  ackbijnn  15842  incexclem  15850  infcvgaux1i  15871  fprodcom2  15998  bpolylem  16062  bpoly3  16072  bpoly4  16073  efcvgfsum  16100  cos1bnd  16203  cos2bnd  16204  znnen  16228  qnnen  16229  aleph1re  16261  3dvds  16348  n2dvdsm1  16386  divalglem5  16414  flodddiv4  16432  sadcaddlem  16474  sadadd2lem  16476  sadadd3  16478  sadaddlem  16483  lcmf0  16651  lcmfunsnlem2lem1  16655  lcmfunsnlem2  16657  coprmprod  16678  coprmproddvdslem  16679  2prm  16709  3lcm2e6  16749  phicl2  16785  pockthi  16925  unbenlem  16926  prmrec  16940  vdwlem13  17011  vdwnn  17016  ramcl2  17034  prmgapprmo  17080  mod2xnegi  17089  modsubi  17090  structcnvcnv  17170  strleun  17174  setsres  17195  strfv  17220  starvndxnbasendx  17316  starvndxnplusgndx  17317  starvndxnmulrndx  17318  scandxnbasendx  17328  scandxnplusgndx  17329  scandxnmulrndx  17330  vscandxnbasendx  17333  vscandxnplusgndx  17334  vscandxnmulrndx  17335  vscandxnscandx  17336  ipndxnbasendx  17344  ipndxnplusgndx  17345  ipndxnmulrndx  17346  slotsdifipndx  17347  tsetndxnplusgndx  17369  tsetndxnmulrndx  17370  tsetndxnstarvndx  17371  slotstnscsi  17372  plendxnplusgndx  17383  plendxnmulrndx  17384  plendxnscandx  17385  plendxnvscandx  17386  slotsdifplendx  17387  basendxnocndx  17395  plendxnocndx  17396  dsndxnplusgndx  17402  dsndxnmulrndx  17403  slotsdnscsi  17404  dsndxntsetndx  17405  slotsdifdsndx  17406  unifndxntsetndx  17412  slotsdifunifndx  17413  slotsdifplendx2  17428  slotsdifocndx  17429  0rest  17441  firest  17444  restid  17445  prdsval  17467  prdsbas  17469  prdsplusg  17470  prdsmulr  17471  prdsvsca  17472  imasaddfnlem  17540  imasvscafn  17549  2oppchomf  17734  0ssc  17848  0subcat  17849  idfucl  17892  homarel  18047  dmaf  18060  cdaf  18061  setc2ohom  18106  catcfuccl  18129  relxpchom  18191  catcxpccl  18217  oppchofcl  18270  oyoncl  18280  letsr  18601  mgmidmo  18636  efmndmgm  18861  smndex1ibas  18876  smndex1mgm  18883  smndex1mnd  18886  smndex2dbas  18890  smndex2dnrinv  18891  smndex2hbas  18892  pwmnd  18913  releqg  19156  ga0  19279  psgnunilem3  19475  psgnunilem4  19476  pmtrsn  19498  efgval  19696  efger  19697  efgsval2  19712  efgsp1  19716  efgsfo  19718  efgredleme  19722  efgredlem  19726  efgred  19727  cygctb  19871  gsum2d2lem  19952  gsum2d2  19953  gsumcom2  19954  dprd2d2  20025  pgpfaclem1  20062  reldvdsr  20318  fldhmsubc  20743  00lsp  20936  cnfldfun  21327  cnfldfunALT  21328  cnfldfunOLD  21340  cnfldfunALTOLD  21341  xrsmgm  21367  pzriprnglem8  21447  pzriprnglem13  21452  pzriprnglem14  21453  pzriprngALT  21454  resubdrg  21566  ocv0  21635  cssval  21640  islinds2  21771  psrvscafval  21906  psrbag0  22018  psdmvr  22105  00ply1bas  22173  ply1plusgfvi  22175  m2detleib  22567  tgdom  22914  tgidm  22916  indistps2ALT  22950  restbas  23094  resttopon  23097  rest0  23105  leordtval2  23148  iocpnfordt  23151  icomnfordt  23152  iooordt  23153  ist1-3  23285  1stcfb  23381  comppfsc  23468  1stckgen  23490  ptbasfi  23517  dfac14  23554  opnfbas  23778  hauspwpwf1  23923  alexsubALT  23987  ptcmplem5  23992  cnextrel  23999  ust0  24156  0met  24303  prdsdsf  24304  prdsxmetlem  24305  prdsmet  24307  prdsbl  24428  qtopbaslem  24695  xrtgioo  24744  xrsdsre  24748  zcld  24751  recld2  24752  reperflem  24756  retopconn  24767  iccpnfcnv  24891  bndth  24906  nmoleub2lem2  25065  zclmncvs  25098  recmet  25273  resscdrg  25308  ishl2  25320  recms  25330  volf  25480  iundisj2  25500  volsup  25507  icombl  25515  ioombl  25516  ismbf3d  25605  0plef  25623  0pledm  25624  itg1ge0  25637  mbfi1fseqlem5  25670  itg2addlem  25709  reldv  25821  limciun  25845  dvexp  25907  dveflem  25933  lhop1lem  25968  lhop  25971  elply2  26151  elplyd  26157  ply1term  26159  ply0  26163  plymullem  26171  qaa  26281  pserulm  26381  pserdvlem2  26388  efcn  26403  sincosq1lem  26456  tangtx  26464  sincos4thpi  26472  pigt3  26477  pige3ALT  26479  efif1olem4  26504  logf1o  26523  relogf1o  26525  log1  26544  loge  26545  logi  26546  relogiso  26557  dvrelog  26596  relogcn  26597  logcn  26606  cxpcn3  26708  resqrtcn  26709  rtprmirr  26720  2logb9irr  26755  leibpi  26902  log2ublem1  26906  birthday  26914  emcllem5  26960  harmonicbnd  26964  harmonicbnd2  26965  harmonicbnd3  26968  lgamgulm2  26996  lgamcvglem  27000  gamf  27003  ppiltx  27137  ppiublem1  27163  ppiub  27165  bclbnd  27241  bpos1lem  27243  bposlem8  27252  lgsquadlem2  27342  2sqlem9  27388  2sqlem10  27389  addsqnreup  27404  chebbnd1  27433  selberg2lem  27511  pntrsumo1  27526  selbergsb  27536  pntpbnd  27549  sltval2  27618  noxp1o  27625  nosepnelem  27641  noetasuplem2  27696  noetainflem2  27700  0slt1s  27791  addsf  27932  precsexlem1  28148  precsexlem2  28149  precsexlem3  28150  precsexlem4  28151  precsexlem5  28152  precsexlem9  28156  precsexlem10  28157  precsexlem11  28158  elons2  28198  onaddscl  28203  onmulscl  28204  eln0s  28275  0zs  28291  zseo  28323  nohalf  28324  lngndxnitvndx  28368  istrkg2ld  28385  tgcgr4  28456  ax5seglem7  28860  axlowdimlem4  28870  axlowdimlem6  28872  axlowdimlem7  28873  axlowdimlem10  28876  axlowdimlem13  28879  axlowdimlem16  28882  uhgr0e  28996  uhgr0  28998  upgrbi  29018  umgrbi  29026  usgr0  29168  lfuhgr1v0e  29179  usgrexmpllem  29185  usgrexmpl  29188  griedg0prc  29189  cplgr0  29350  usgrexilem  29365  cffldtocusgr  29372  cffldtocusgrOLD  29373  rgrusgrprc  29515  rusgrprc  29516  rgrprcx  29518  rgrx0ndm  29519  usgr2pthlem  29691  pthdlem2  29696  uspgrn2crct  29736  wwlksnext  29821  clwwlknondisj  30038  0ewlk  30041  0wlk  30043  0pth  30052  1pthdlem1  30062  1trld  30069  wlk2v2elem2  30083  wlk2v2e  30084  upgr3v3e3cycl  30107  upgr4cycl4dv4e  30112  dfconngr1  30115  0conngr  30119  konigsbergumgr  30178  2wspmdisj  30264  2clwwlk2clwwlk  30277  numclwwlk3lem2lem  30310  numclwwlk3lem2  30311  ex-dif  30350  ex-in  30352  ex-eprel  30360  ex-id  30361  ex-fl  30374  ex-mod  30376  ex-hash  30380  ex-fpar  30389  avril1  30390  2bornot2b  30391  0vfval  30533  vsfval  30560  ajmoi  30785  ajfuni  30786  normlem2  31038  norm3adifii  31075  hhip  31104  hlim0  31162  hlimcaui  31163  hlimf  31164  hhssnv  31191  shscli  31244  shsval2i  31314  h1de2i  31480  fh3i  31550  fh4i  31551  cm2mi  31553  qlaxr3i  31563  mayetes3i  31656  ho0f  31678  hoif  31681  hodidi  31714  ho0subi  31722  hosd1i  31749  adjmo  31759  nmopsetn0  31792  nmfnsetn0  31805  funadj  31813  funcnvadj  31820  nmcexi  31953  cnlnadjlem8  32001  nmoptri2i  32026  opsqrlem4  32070  hmopidmchi  32078  pjoci  32107  pjinvari  32118  abrexdomjm  32434  elim2ifim  32472  iundisj2f  32517  rinvf1o  32554  dfcnv2  32600  snct  32637  fzodif2  32714  iundisj2fi  32720  dp2lt10  32804  dp2ltc  32807  dplti  32825  dpgti  32826  dpexpp1  32828  s1chn  32936  chnub  32938  gsumle  33038  xrge0slmod  33309  isconstr  33716  zarcls  33851  zartopn  33852  xrge0pluscn  33917  qqhre  33997  esumrnmpt2  34045  esumfsup  34047  esumpcvgval  34055  hasheuni  34062  esumcvg  34063  esumcvgsum  34065  esumsup  34066  esum2d  34070  dmsigagen  34121  ldgenpisyslem3  34142  measvuni  34191  voliune  34206  volfiniune  34207  br2base  34247  dya2iocuni  34261  eulerpartlem1  34345  eulerpartlemt  34349  eulerpartgbij  34350  fib0  34377  coinfliprv  34461  ballotlem2  34467  ballotlemic  34485  ballotlem7  34514  ballotth  34516  plymul02  34524  rpsqrtcn  34571  chtvalz  34607  circlemethnat  34619  circlevma  34620  circlemethhgt  34621  hgt750lem  34629  bnj226  34711  bnj1101  34761  bnj110  34835  bnj149  34852  bnj150  34853  bnj151  34854  bnj517  34862  bnj580  34890  bnj865  34900  bnj900  34906  bnj996  34933  bnj1110  34959  bnj1133  34966  bnj1128  34967  bnj1145  34970  bnj1137  34972  bnj1171  34977  bnj1176  34982  f1resfz0f1d  35082  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  35684  brtpid2  35685  brtpid3  35686  faclimlem1  35706  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  36324  filnetlem3  36344  nrmo  36374  waj-ax  36378  lukshef-ax2  36379  arg-ax  36380  limsucncmpi  36409  dnizeq0  36439  knoppcnlem8  36464  knoppcnlem11  36467  cnndvlem1  36501  bj-babylob  36568  bj-ax12ssb  36622  bj-nnfnth  36707  bj-snsetex  36927  bj-0eltag  36942  bj-2upln0  36987  bj-2upln1upl  36988  bj-snexg  36998  bj-unexg  37002  bj-adjg1  37007  f1omptsnlem  37300  f1omptsn  37301  icoreresf  37316  relowlssretop  37327  relowlpssretop  37328  domalom  37368  matunitlindf  37588  poimirlem3  37593  poimirlem9  37599  poimirlem16  37606  poimirlem17  37607  poimirlem18  37608  poimirlem19  37609  poimirlem20  37610  poimirlem26  37616  mblfinlem1  37627  mblfinlem2  37628  ismblfin  37631  voliunnfl  37634  cnambfre  37638  abrexdom  37700  fdc  37715  cncfres  37735  heibor1lem  37779  grposnOLD  37852  bicontr  38050  an12i  38068  tsim1  38100  ac6s6f  38143  vvdifopab  38224  brcnvrabga  38306  opabf  38332  xrnrel  38337  relcoels  38388  cnvcosseq  38401  refrelcoss3  38427  refrelcoss2  38428  symrelcoss2  38430  refrelcoss  38487  symrelcoss  38524  n0eldmqs  38612  ax13fromc9  38870  dedths  38926  renegclALT  38927  12gcd5e1  41962  60gcd7e1  41964  lcmineqlem23  42010  dvrelog2  42023  dvrelog3  42024  dvrelog2b  42025  aks4d1p1p6  42032  aks4d1p1p7  42033  aks4d1p1  42035  sticksstones22  42127  2xp3dxp2ge1d  42200  sn-axprlem3  42214  acos1half  42348  moxfr  42662  mapfzcons1  42687  diophrw  42729  0dioph  42748  vdioph  42749  rabren3dioph  42785  2nn0ind  42916  rpnnen3  43003  kelac2lem  43035  frlmpwfi  43069  oaordnrex  43266  omnord1ex  43275  oenord1ex  43286  oaomoencom  43288  ifpbiidcor2  43454  iscard4  43504  sqrtcval  43612  resqrtvalex  43616  eliunov2  43650  xphe  43752  0he  43753  he0  43755  snhesn  43757  idhe  43758  frege54cor1c  43886  clsk1independent  44017  neicvgnvor  44087  amgm2d  44169  amgm3d  44170  amgm4d  44171  ismnushort  44273  lhe4.4ex1a  44301  rusbcALT  44411  ipo0  44421  ifr0  44422  vk15.4j  44501  2sb5nd  44533  dfvd1ir  44546  dfvd2anir  44557  dfvd2ir  44559  dfvd3ir  44566  dfvd3anir  44569  iden2  44587  e0bir  44749  uun2221p1  44786  uun2221p2  44787  2sb5ndVD  44882  2sb5ndALT  44904  iunconnlem2  44907  trwf  44932  wfaxext  44966  wfaxpow  44970  wfaxinf2  44974  wfac8prim  44975  permaxinf2lem  44985  fnchoice  45001  unisn0  45026  eliincex  45082  icof  45191  fnmptif  45237  supminfxr  45439  rexanuz2nf  45467  fsumiunss  45552  climlimsupcex  45746  liminfltlimsupex  45758  liminflelimsupcex  45774  xlimrel  45797  xlimfun  45832  resincncf  45852  dvnprodlem3  45925  volioc  45949  volico  45960  dmvolss  45962  volioof  45964  stoweidlem13  45990  stoweidlem34  46011  stirlinglem5  46055  stirlinglem13  46063  stirlingr  46067  fourierdlem42  46126  fourierdlem62  46145  fouriersw  46208  etransc  46260  salexct  46311  salexct2  46316  salgencntex  46320  sge0rnn0  46345  gsumge0cl  46348  sge00  46353  sge0resplit  46383  sge0reuz  46424  omeiunle  46494  0ome  46506  icoresmbl  46520  ovn0lem  46542  ovnhoilem1  46578  hspmbl  46606  nsssmfmbf  46756  mbfpsssmf  46760  smfresal  46765  smfmullem4  46771  smfpimbor1lem1  46775  smfpimbor1lem2  46776  lambert0  46867  lamberte  46868  aistia  46874  aisfina  46875  aiffnbandciffatnotciffb  46881  axorbciffatcxorb  46882  abnotbtaxb  46892  abnotataxb  46893  eusnsn  47003  aiotaval  47072  aiota0ndef  47074  fundcmpsurinjimaid  47373  ichv  47411  ichf  47412  ichid  47413  icht  47414  ichcircshi  47416  icheq  47424  spr0nelg  47438  m3prm  47554  m7prm  47562  0noddALTV  47651  2noddALTV  47655  341fppr2  47696  9fppr8  47699  nfermltl8rev  47704  nfermltl2rev  47705  nfermltlrev  47706  sbgoldbo  47749  nnsum3primes4  47750  evengpop3  47760  stgr1  47921  usgrexmpl1lem  47973  usgrexmpl1  47974  usgrexmpl1tri  47977  usgrexmpl2lem  47978  usgrexmpl2  47979  usgrexmpl2nb0  47983  usgrexmpl2nb1  47984  usgrexmpl2nb2  47985  usgrexmpl2nb3  47986  usgrexmpl2nb4  47987  usgrexmpl2nb5  47988  gpg5nbgrvtx03starlem1  48018  gpg5nbgrvtx03starlem2  48019  gpg5nbgrvtx03starlem3  48020  gpg5nbgrvtx13starlem1  48021  gpg5nbgrvtx13starlem2  48022  gpg5nbgrvtx13starlem3  48023  gpg5grlic  48041  gpgprismgr4cycllem2  48043  gpgprismgr4cycllem7  48048  oddinmgm  48098  nn0mnd  48102  2zrngamgm  48168  2zrngaabl  48173  2zrngmmgm  48175  2zrngnring  48181  fldhmsubcALTV  48256  eliunxp2  48257  zlmodzxzldeplem  48422  zlmodzxzldep  48428  ldepslinc  48433  rrx2xpreen  48647  rrx2plordisom  48651  line2ylem  48679  line2  48680  line2x  48682  inlinecirc02plem  48714  mosn  48739  mof0  48764  mof0ALT  48766  tposrescnv  48802  tposres3  48804  tposideq2  48812  f1omo  48816  nelsubc3  48986  reldmxpc  49111  reldmprcof1  49239  setc1onsubc  49427  reldmlmd2  49473  reldmcmd2  49474  rellmd  49477  relcmd  49478  ex-gte  49541  empty-surprise  49594  eximp-surprise2  49597  amgmw2d  49616