MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  bitri Unicode version

Theorem bitri 241
Description: An inference from transitive law for logical equivalence. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 13-Oct-2012.)
Hypotheses
Ref Expression
bitri.1  |-  ( ph  <->  ps )
bitri.2  |-  ( ps  <->  ch )
Assertion
Ref Expression
bitri  |-  ( ph  <->  ch )

Proof of Theorem bitri
StepHypRef Expression
1 bitri.1 . . . 4  |-  ( ph  <->  ps )
21biimpi 187 . . 3  |-  ( ph  ->  ps )
3 bitri.2 . . 3  |-  ( ps  <->  ch )
42, 3sylib 189 . 2  |-  ( ph  ->  ch )
53biimpri 198 . . 3  |-  ( ch 
->  ps )
65, 1sylibr 204 . 2  |-  ( ch 
->  ph )
74, 6impbii 181 1  |-  ( ph  <->  ch )
Colors of variables: wff set class
Syntax hints:    <-> wb 177
This theorem is referenced by:  bitr2i  242  bitr3i  243  bitr4i  244  bitrd  245  3bitri  263  3bitr2i  265  3bitr3i  267  3bitr4i  269  xchbinx  302  bibi12i  307  imbi12i  317  mt2bi  329  iman  414  orbi12i  508  or42  516  pm4.71r  613  biadan2  624  anbi2ci  678  anbi12i  679  anbi12ci  680  pm5.3  693  pm5.53  772  an42  799  orddi  840  anddi  841  rbaib  874  rbaibr  875  pm4.43  894  biluk  900  pm5.75  904  dn1  933  jaoi2  934  3orass  939  3anass  940  3ancomb  945  3anan32  948  3anan12  949  3anor  950  an6  1263  xor2  1316  falbitru  1358  falnantru  1362  truxortru  1364  truxorfal  1365  falxorfal  1367  exp3acom23g  1377  hadass  1392  hadbi  1393  hadrot  1396  cador  1397  cadan  1398  cadnot  1400  cadcomb  1402  cadrot  1403  cad1  1404  had1  1408  alex  1578  alinexa  1585  alexn  1586  exanali  1592  19.26-2  1601  19.26-3an  1602  albiim  1618  2albiim  1619  ax12bOLD  1698  alrot3  1749  alrot4  1750  exrot3  1755  exrot4  1756  19.27  1837  19.28  1838  19.21-2  1883  nf2  1885  19.36  1888  19.37  1890  19.44  1894  19.45  1895  aaan  1902  eeor  1903  19.23vv  1911  pm11.53  1912  19.41vv  1921  19.41vvv  1922  19.41vvvv  1923  19.42vv  1926  19.42vvv  1927  4exdistr  1930  4exdistrOLD  1931  eean  1932  eeeanv  1934  cbvex4v  2062  sbor  2115  sbrim  2116  sblim  2117  sban  2118  sbbi  2120  sblbis  2121  sbrbis  2122  sbrbif  2123  sbid2  2133  sbco2d  2136  sbnf2  2157  2sb5  2161  2sb6  2162  sbcom2  2163  pm11.07  2164  sb6a  2166  2sb5rf  2167  2sb6rf  2168  sbex  2178  sbalv  2179  exsbOLD  2181  2exsb  2182  eujust  2256  euf  2260  cbveu  2274  eu2  2279  mo2  2283  sbmo  2284  mo3  2285  mo4f  2286  eu4  2293  moanim  2310  2mo  2332  2mos  2333  2eu1  2334  2eu3  2336  2eu4  2337  2eu6  2339  exists1  2343  abid  2392  eleq12i  2469  abeq2  2509  abeq2i  2511  clabel  2525  abid2f  2565  sbabel  2566  neeq12i  2579  necon1abii  2618  neanior  2652  ralnex  2676  rexnal  2677  ralinexa  2711  rexanali  2712  r3al  2723  r19.26-2  2799  ralbiim  2803  r19.30  2813  ralcomf  2826  rexcomf  2827  rexrot4  2831  reean  2834  3reeanv  2836  rabbi  2846  cbvralf  2886  cbvreu  2890  cbvral2v  2900  cbvrex2v  2901  cbvral3v  2902  cbvralsv  2903  cbvrexsv  2904  sbralie  2905  rabeq2i  2913  issetf  2921  2gencl  2945  3gencl  2946  ceqsex2  2952  ceqsex3v  2954  ceqsex6v  2956  ceqsex8v  2957  gencbvex  2958  spc3gv  3001  eqvincf  3024  ceqsrex2v  3031  elrab2  3054  ralab  3055  ralrab  3056  rexab  3057  rexrab  3058  ralab2  3059  rexab2  3061  eueq3  3069  morex  3078  euxfr2  3079  euxfr  3080  euind  3081  reu2  3082  reu6  3083  rmo4  3087  reu4  3088  reu7  3089  rmoim  3093  2reuswap  3096  reuind  3097  2reu5lem1  3099  2reu5lem2  3100  2reu5  3102  sbcco  3143  sbccomlem  3191  sbccom  3192  ra5  3205  rmo3  3208  csbco  3220  sbnfc2  3269  csbabg  3270  cbvralcsf  3271  cbvreucsf  3273  dfss  3295  dfss2f  3299  ss2ab  3371  dfpss2  3392  dfpss3  3393  psseq12i  3398  sspsstri  3409  difeqri  3427  raldifb  3447  uneqri  3449  ssequn2  3480  unss  3481  rexun  3487  ralunb  3488  elin2  3491  ineqri  3494  dfss1  3505  dfss5  3506  nsspssun  3534  indifdir  3557  inrab2  3574  rabun2  3580  reuun2  3584  eq0  3602  0el  3604  abn0  3606  0pss  3625  disjr  3629  disj1  3630  disjpss  3638  undif4  3644  difin0ss  3654  inssdif0  3655  uneqdifeq  3676  r19.3rz  3679  r19.3rzv  3681  ralidm  3691  pwss  3773  dfpr2  3790  ralsns  3804  rexsns  3805  eltpg  3811  ralprg  3817  rexprg  3818  raltpg  3819  rextpg  3820  rabrsn  3834  euabsn2  3835  eusn  3840  eldifsn  3887  rexdifsn  3891  tppreqb  3899  difsnpss  3901  pwpw0  3906  ssunsn  3919  eqsn  3920  sstp  3923  tpss  3924  prel12  3935  prnebg  3939  preqsn  3940  pwsnALT  3970  pwtp  3972  eluniab  3987  elunirab  3988  unipr  3989  dfnfc2  3993  uniun  3994  uniin  3995  unissb  4005  elintab  4021  elintrab  4022  ssintab  4027  ssintrab  4033  intun  4042  intpr  4043  elrint  4051  iuncom4  4060  iuneq2  4069  dfiun2g  4083  ssiinf  4100  elriin  4123  iunxiun  4133  pwssb  4137  iunpwss  4140  dfdisj2  4144  disjor  4156  disjors  4158  disjiun  4162  disjxiun  4169  disjxun  4170  cbvopab1  4238  dftr5  4265  trint  4277  inex1  4304  inuni  4322  axpweq  4336  nfnid  4353  zfpair2  4364  moabex  4382  exss  4386  elop  4389  otth  4400  copsex4g  4405  opeqsn  4412  opthwiener  4418  opelopabsbOLD  4423  brabga  4429  opelopabaf  4438  opabn0  4445  iunopab  4446  pwunss  4448  dfid3  4459  pocl  4470  sotric  4489  isso2i  4495  somo  4497  frminex  4522  dfepfr  4527  wefrc  4536  ordtri3or  4573  ordtri2  4576  elsuci  4607  elsucg  4608  sucel  4614  on0eqel  4658  uniuni  4675  reusv2lem4  4686  reusv2lem5  4687  reusv2  4688  reusv3  4690  reuxfr2d  4705  elpwun  4715  iunpw  4718  dfwe2  4721  onintrab2  4741  ordpwsuc  4754  ordzsl  4784  dflim4  4787  tfindsg  4799  tfindes  4801  findsg  4831  elxp  4854  opelxp  4867  brxp  4868  rabxp  4873  opthprc  4884  brab2a  4886  opeliunxp  4888  xpundi  4889  xpundir  4890  elvvv  4896  brinxp  4899  brab2ga  4910  xp0r  4915  ssrel2  4925  eqrelrel  4936  reliun  4954  reluni  4956  raliunxp  4973  rexiunxp  4974  ralxpf  4978  rexxpf  4979  iunxpf  4980  relop  4982  elcnv  5008  elcnv2  5009  dmin  5036  dmuni  5038  dmopab  5039  dmi  5043  rnopab  5074  elrnmpt1  5078  rncoeq  5098  resiexg  5147  dfima2  5164  dfima3  5165  elima2  5168  elima3  5169  imai  5177  elimasn  5188  epini  5193  dfse2  5196  cotr  5205  issref  5206  intasym  5208  asymref  5209  asymref2  5210  somin1  5229  cnvopab  5233  cnvi  5235  cnvdif  5237  imainss  5246  dfrel2  5280  dfrel3  5287  rnsnn0  5295  relsn2  5299  dmsnopg  5300  cnvcnvsn  5306  elxp4  5316  elxp5  5317  cnvresima  5318  mptpreima  5322  dfco2  5328  coundi  5330  coundir  5331  imaco  5334  coiun  5338  coi1  5344  relssdmrn  5349  relrelss  5352  ressn  5367  cnviin  5368  cnvpo  5369  cbviota  5382  dffun2  5423  dffun3  5424  dffun4  5425  dffun5  5426  dffun7  5438  dffun8  5439  dffun9  5440  funopab  5445  funun  5454  funcnvsn  5455  fntpg  5465  funcnv2  5469  funcnv  5470  fun2cnv  5472  fncnv  5474  fun11  5475  fununi  5476  imadif  5487  funimaexg  5489  fnunsn  5511  fnres  5520  fnopabg  5527  mptfng  5529  mptun  5534  fun  5566  fresaunres1  5575  fcnvres  5579  dff12  5597  f1cnvcnv  5606  funforn  5619  dff1o2  5638  dff1o5  5642  f1orn  5643  resdif  5655  ffoss  5666  f11o  5667  f1o00  5669  fo00  5670  elfv  5685  fv3  5703  dffn5f  5740  dffv2  5755  eqfnfv3  5788  fndmdifeq0  5795  fneqeql  5797  unpreima  5815  respreima  5818  dff4  5842  dffo3  5843  dffo5  5845  f1ompt  5850  ffnfvf  5854  fmptco  5860  fsn2  5867  ftpg  5875  fconst3  5914  fconst4  5915  idref  5938  abrexco  5945  opabex3d  5948  opabex3  5949  abexssex  5961  dff13  5963  dff13f  5965  foeqcnvco  5986  isocnv3  6011  isoini  6017  weniso  6034  oprabid  6064  0neqopab  6078  dfoprab2  6080  eqoprab2b  6091  dmoprab  6113  rnoprab  6115  eloprabga  6119  mpt2mptx  6123  resoprab  6125  ffnov  6133  fnov  6137  elrnmpt2  6142  ralrnmpt2  6143  rexrnmpt2  6144  oprabex3  6147  oprabrexex2  6148  ovid  6149  ov3  6169  ov6g  6170  foov  6179  ndmovdistr  6195  difxp  6339  elopaba  6368  fmpt2  6377  curry1  6397  curry2  6400  fsplit  6410  frxp  6415  xporderlem  6416  soxp  6418  mpt2xopovel  6430  brtpos2  6444  dmtpos  6450  tpostpos  6458  tpossym  6470  tposoprab  6474  sorpsscmpl  6492  opiota  6494  eusvobj2  6541  dfsmo2  6568  tfrlem3  6597  tfrlem7  6603  tfrlem9  6605  tfrlem9a  6606  tz7.48lem  6657  tz7.49c  6662  el1o  6702  dif1o  6703  ondif2  6705  brwitnlem  6710  oarec  6764  omeulem1  6784  omeu  6787  oeordi  6789  oeeui  6804  oeeu  6805  omopthlem1  6857  dfer2  6865  brdifun  6891  swoso  6895  eqerlem  6896  qsid  6929  iiner  6935  erinxp  6937  brecop  6956  eroveu  6958  erovlem  6959  ecopovsym  6965  mapval2  7002  mapsn  7014  elixp  7028  ixpeq2  7035  ixpin  7046  ixpiin  7047  mptelixpg  7058  ixpsnf1o  7061  boxriin  7063  domen  7080  isfi  7090  en1  7133  xpsnen  7151  xpcomco  7157  xpassen  7161  sbthlem9  7184  0sdomg  7195  2pwuninel  7221  ssenen  7240  nneneq  7249  php  7250  modom2  7269  ac6sfi  7310  frfi  7311  fimaxg  7313  elfpw  7366  fissuni  7369  dffi3  7394  marypha1lem  7396  marypha2lem2  7399  dfsup2  7405  dfsup2OLD  7406  wofib  7470  wemapso2lem  7475  wdom2d  7504  unxpwdom2  7512  dford2  7531  inf2  7534  inf3lem2  7540  axinf2  7551  zfinf2  7553  cantnfp1lem2  7591  oemapso  7594  cantnflem1  7601  trcl  7620  epfrs  7623  rankvalb  7679  r1elss  7688  unbndrank  7724  scott0s  7768  cplem1  7769  bnd2  7773  isnum2  7788  iscard2  7819  infxpenlem  7851  fseqenlem1  7861  acnnum  7889  infpwfien  7899  alephnbtwn2  7909  alephord2  7913  alephislim  7920  cardaleph  7926  alephval3  7947  aceq1  7954  aceq2  7956  dfac3  7958  dfac4  7959  dfac5lem1  7960  dfac5lem2  7961  dfac5lem3  7962  dfac5lem4  7963  dfac5lem5  7964  dfac2  7967  dfac0  7969  dfac1  7970  dfac8  7971  dfac9  7972  dfac12  7985  kmlem3  7988  kmlem4  7989  kmlem7  7992  kmlem8  7993  kmlem9  7994  kmlem13  7998  kmlem14  7999  kmlem15  8000  dfackm  8002  pwsdompw  8040  ackbij2lem2  8076  cf0  8087  cfval2  8096  cflim2  8099  cfss  8101  cfslb  8102  isfin3  8132  isfin5  8135  isfin6  8136  sdom2en01  8138  fin23lem25  8160  fin23lem26  8161  fin23lem40  8187  isfin1-2  8221  isfin1-3  8222  fin1a2lem5  8240  fin1a2lem6  8241  fin1a2lem12  8247  fin12  8249  domtriomlem  8278  axdc2lem  8284  axdc3lem2  8287  axdc3lem4  8289  axcclem  8293  ac6num  8315  ac6n  8321  zorn2lem6  8337  zornn0g  8341  ttukeylem6  8350  ttukey2g  8352  brdom7disj  8365  brdom6disj  8366  iunfo  8370  iundom2g  8371  konigthlem  8399  alephsuc3  8411  elgch  8453  fpwwe2lem9  8469  fpwwe2lem12  8472  fpwwe2lem13  8473  fpwwe2  8474  canth4  8478  canthwe  8482  wunex2  8569  uniwun  8571  axgroth5  8655  grothpw  8657  axgroth6  8659  grothprimlem  8664  grothprim  8665  elni  8709  ltexpi  8735  nqerf  8763  nqerid  8766  ordpipq  8775  recmulnq  8797  npomex  8829  genpnnp  8838  genpass  8842  addcompr  8854  mulcompr  8856  reclem2pr  8881  reclem3pr  8882  ltsosr  8925  ltasr  8931  mappsrpr  8939  map2psrpr  8941  opelcn  8960  elreal  8962  elreal2  8963  axaddf  8976  axmulf  8977  axicn  8981  axrrecex  8994  axpre-mulgt0  8999  xrlenlt  9099  ssxr  9101  leloe  9117  msq0i  9625  infm3  9923  supmullem2  9931  inelr  9946  arch  10174  elnnne0  10191  un0addcl  10209  un0mulcl  10210  nn0n0n1ge2b  10237  elnnz  10248  elznn0nn  10251  elznn0  10252  elznn  10253  elz2  10254  raluz2  10482  rexuz2  10484  nnwos  10500  eluz2b2  10504  eluz2b3  10505  ublbneg  10516  zmin  10526  elq  10532  ralrp  10586  rexrp  10587  ltxr  10671  xrnemnf  10674  xrleloe  10693  xrltlen  10695  xrrebnd  10712  xaddf  10766  xmullem  10799  xmullem2  10800  xrsupss  10843  xrinfmss  10844  elfzp1  11053  fzprval  11062  fztpval  11063  4fvwrd4  11076  fzm1  11082  fzolb  11100  fzolb2  11101  elfzo3  11110  fzouzsplit  11123  fzo0n0  11129  fzind2  11153  uzrdgfni  11253  subsq0i  11449  crreczi  11459  nn0le2msqi  11515  nn0opth2i  11519  hashkf  11575  hashinfxadd  11614  hashgt12el  11637  hashgt12el2  11638  hashtpg  11646  hashfun  11655  hashbclem  11656  hashbc  11657  hashf1lem2  11660  leiso  11663  iswrd  11684  f1oun2prg  11819  climeu  12304  lo1resb  12313  rlimresb  12314  o1resb  12315  climmpt2  12322  fsum2dlem  12509  rpnnen2  12780  sqr2irr  12803  divides  12809  odd2np1  12863  divalglem1  12869  divalglem6  12873  divalglem10  12877  divalgb  12879  bitsval2  12892  bitsmod  12903  bitscmp  12905  smueqlem  12957  isprm2  13042  isprm3  13043  isprm4  13044  isprm5  13067  pythagtriplem19  13162  pythagtrip  13163  pceu  13175  prmreclem2  13240  4sqlem2  13272  4sqlem12  13279  vdwpc  13303  vdwnn  13321  dec5dvds2  13356  pwsle  13669  imasleval  13721  xpsfrnel  13743  xpsfrnel2  13745  xpsle  13761  isacs2  13833  mreacs  13838  iscatd2  13861  comfeq  13887  oppcsect  13954  isfunc  14016  funcoppc  14027  isffth2  14068  fucinv  14125  elhoma  14142  setcinv  14200  ispos  14359  ispos2  14360  tosso  14420  istsr2  14605  spwmo  14613  ismnd  14647  mndcl  14650  issubm  14703  gsumwspan  14746  issubg  14899  isnsg2  14925  eqger  14945  isgim2  15007  giclcl  15014  gicrcl  15015  gicsubgen  15020  gaorber  15040  resscntz  15085  cntzrec  15087  efgval2  15311  efgsfo  15326  efgrelexlemb  15337  isabl2  15375  iscyggen2  15446  iscyg2  15447  iscyg3  15451  lt6abl  15459  gsumval3eu  15468  gsum2d2  15503  dmdprdd  15515  subgdmdprd  15547  iscrng2  15634  dvdsrtr  15712  isunit  15717  isnirred  15760  isirred2  15761  isrhm  15779  isdrng2  15800  drngprop  15801  isabv  15862  issrng  15893  islmod  15909  islss  15966  lss1d  15994  islmim2  16093  lmiclcl  16097  lmicrcl  16098  lsmelval2  16112  lspsolvlem  16169  lspsncv0  16173  islpidl  16272  islpir2  16277  isnzr2  16289  isdomn2  16314  fiidomfld  16323  aspval2  16360  mplcoe1  16483  mplcoe2  16485  evlslem4  16519  xrsdsreclb  16700  unocv  16862  iunocv  16863  ishil2  16901  isobs  16902  obselocv  16910  iinopn  16930  istps4OLD  16943  istps5OLD  16944  istps  16956  istps2  16957  isbasis2g  16968  tgval2  16976  elcls  17092  neipeltop  17148  neiptopuni  17149  islpi  17167  isperf2  17170  isperf3  17171  neitr  17198  restntr  17200  ordtrest2lem  17221  cnrest  17303  ist0-3  17363  ist1-2  17365  ist1-3  17367  nrmsep3  17373  isnrm2  17376  perfcls  17383  ordthaus  17402  cmpcov2  17407  cmpsub  17417  hauscmplem  17423  cmpfi  17425  iscon2  17430  dfcon2  17435  is1stc2  17458  is2ndc  17462  1stcelcls  17477  1stccn  17479  llyi  17490  subislly  17497  iskgen3  17534  txuni2  17550  ptpjpre1  17556  ptbasin  17562  tx1cn  17594  tx2cn  17595  uptx  17610  txdis1cn  17620  ptrescn  17624  txtube  17625  txcmplem1  17626  hausdiag  17630  txkgen  17637  xkohaus  17638  xkococnlem  17644  xkoinjcn  17672  qtopeu  17701  isr0  17722  regr1lem2  17725  hmphsym  17767  elmptrab2  17813  isfbas  17814  isfbas2  17820  trfbas  17829  snfil  17849  fbunfip  17854  elfg  17856  fgcl  17863  fbasrn  17869  filuni  17870  trfil2  17872  cfinfil  17878  csdfil  17879  supfil  17880  ufinffr  17914  rnelfmlem  17937  elflim2  17949  hausflim  17966  hauspwpwf1  17972  txflf  17991  isfcls2  17998  fclsopn  17999  fclsrest  18009  alexsubALTlem2  18032  alexsubALTlem3  18033  alexsubALTlem4  18034  tmdcn2  18072  divstgplem  18103  divstgphaus  18105  tsmssubm  18125  istdrg2  18160  ustfilxp  18195  ust0  18202  fmucndlem  18274  metn0  18343  prdsxmetlem  18351  imasdsf1olem  18356  xpsdsval  18364  blres  18414  xmeterval  18415  xmeter  18416  isxms2  18431  isms2  18433  metustsymOLD  18544  metustsym  18545  dscopn  18574  isngp3  18598  isnvc2  18687  isnghm  18710  qtopbaslem  18745  xrtgioo  18790  zcld  18797  elii1  18913  pi1cpbl  19022  tchcph  19147  cmetss  19220  bcth  19235  lssbn  19257  ishl2  19277  minveclem3b  19282  minveclem6  19288  pmltpc  19300  ovolfcl  19316  ovolgelb  19329  ovolunlem1  19346  ovoliunlem1  19351  ismbl  19375  ismbl2  19376  iundisj2  19396  dyadmax  19443  dyadmbllem  19444  vitalilem2  19454  mbfimaopnlem  19500  itg1climres  19559  itg2l  19574  itg2leub  19579  iblcnlem1  19632  ellimc2  19717  ellimc3  19719  limcmpt  19723  limcres  19726  elaa  20186  aaliou3lem9  20220  taylthlem2  20243  ulmcau  20264  pilem1  20320  sincosq1lem  20358  sineq0  20382  coseq1  20383  ellogrn  20410  logtayl2  20506  cxpcn3lem  20584  cxpcn3  20585  cubic  20642  atandm  20669  atandm2  20670  atandm4  20672  atans2  20724  xrlimcnp  20760  wilthlem2  20805  dvdsflsumcom  20926  dvdsmulf1o  20932  fsumvma  20950  logfac2  20954  dchrelbas2  20974  dchrelbas3  20975  lgsdir2lem4  21063  lgsquadlem1  21091  lgsquadlem2  21092  2sqlem1  21100  pntlem3  21256  ostth  21286  usgra2edg1  21356  usgraedg4  21359  nbgrasym  21402  nb3grapr  21415  nb3grapr2  21416  cusgra2v  21424  cusgra3v  21426  uvtx01vtx  21454  trls  21489  0wlk  21498  0trl  21499  wlkntrllem1  21512  wlkntrllem2  21513  is2wlk  21518  3v3e3cycl1  21584  3v3e3cycl2  21604  vdgrun  21625  vdgrfiun  21626  eupath  21656  avril1  21710  grpoidinvlem3  21747  issubgo  21844  islno  22207  nmoubi  22226  nmobndseqi  22233  siii  22307  minvecolem5  22336  minvecolem6  22337  hvsubaddi  22521  normsub0i  22590  bcsiALT  22634  hcau  22639  hlimadd  22648  hhcmpl  22655  hhcms  22658  issh2  22664  isch2  22679  hlim0  22691  isch3  22697  norm1exi  22705  elch0  22709  hhsssh2  22723  choc0  22781  pjhtheu  22849  pjpreeq  22853  omlsilem  22857  pjoc2i  22893  chsscon1i  22917  spanuni  22999  h1deoi  23004  h1dei  23005  elspansni  23013  cmcm4i  23050  cmbr3i  23055  cmbr4i  23056  osumcor2i  23099  5oalem7  23115  3oalem3  23119  pjss2i  23135  mayete3iOLD  23184  elcnop  23313  ellnop  23314  elhmop  23329  elcnfn  23338  ellnfn  23339  cnvadj  23348  nmopub  23364  nmfnleub  23381  eleigvec  23413  nmop0  23442  nmfn0  23443  nmopun  23470  lncnopbd  23493  riesz2  23522  nmopcoadj0i  23559  rnbra  23563  pjnmopi  23604  pjssdif1i  23631  pjin2i  23649  pjin3i  23650  pjclem1  23651  cvbr2  23739  cvnbtwn3  23744  cvnbtwn4  23745  mdsl2bi  23779  mdsldmd1i  23787  elat2  23796  chrelat2i  23821  atomli  23838  chirredi  23850  mdsymlem6  23864  mdsymlem8  23866  sumdmdii  23871  dmdbr5ati  23878  cdj3i  23897  xfree2  23901  abeq2f  23913  r19.41vv  23923  mo5f  23925  nmo  23926  2reuswap2  23928  reuxfr3d  23929  rexunirn  23931  rmo3f  23935  rmo4fOLD  23936  rmo4f  23937  difeq  23951  disjorf  23974  disjorsf  23975  iundisj2f  23983  dfrel4  23987  suppss2f  24002  abfmpunirn  24017  fmptdF  24022  mptfnf  24026  fmptcof2  24029  ofpreima  24034  funcnvmptOLD  24035  funcnvmpt  24036  funcnv5mpt  24037  gtiso  24041  disjdsct  24043  iundisj2fi  24106  elxrge02  24131  toslub  24144  tosglb  24145  ofldsqr  24193  isarchi  24205  eldiftp  24346  esumnul  24396  esumpfinvalf  24419  isrnsigaOLD  24448  isrnsiga  24449  measiuns  24524  elunirnmbfm  24556  1stmbfm  24563  2ndmbfm  24564  dya2iocnrect  24584  sibfof  24607  ballotlemelo  24698  ballotlemodife  24708  ballotlem4  24709  eldmgm  24759  subfacp1lem5  24823  subfacp1lem6  24824  cvmscld  24913  cvmlift2lem12  24954  ghomgrpilem2  25050  axextprim  25103  axrepprim  25104  axunprim  25105  axpowprim  25106  axregprim  25107  axinfprim  25108  axacprim  25109  untangtr  25116  biimpexp  25126  dfid4  25136  divelunit  25138  divcnvshft  25164  divcnvlin  25165  ntrivcvgmul  25183  prodsn  25239  fprod2dlem  25257  dftr6  25321  coep  25322  coepr  25323  dffr5  25324  dfpo2  25326  cnvco1  25331  cnvco2  25332  eldm3  25333  fundmpss  25336  dfdm5  25346  dfrn5  25347  elpotr  25351  dford5reg  25352  dfon2lem5  25357  dfon2lem6  25358  dfon2lem8  25360  dfon2lem9  25361  dfon2  25362  wfi  25421  eltrpred  25443  frind  25457  poseq  25467  soseq  25468  wfrlem4  25473  wfrlem5  25474  wfrlem9  25478  wfrlem11  25480  wfrlem12  25481  wfrlem13  25482  wfrlem14  25483  wfrlem15  25484  tfrALTlem  25490  tfr3ALT  25493  frrlem5  25499  frrlem5e  25503  frrlem11  25507  nosgnn0  25526  nodenselem5  25553  nobnddown  25569  nofulllem5  25574  elsymdif  25581  brsymdif  25586  brtxp  25634  brpprod  25639  brpprod3b  25641  brsset  25643  idsset  25644  dfon3  25646  brtxpsd  25648  brtxpsd2  25649  brbigcup  25652  elfix  25657  dffix2  25659  ellimits  25664  dffun10  25667  elfuns  25668  snelsingles  25675  dfiota3  25676  brcart  25685  brimg  25690  brapply  25691  brcup  25692  brcap  25693  brsuccf  25694  funpartlem  25695  funpartfun  25696  fullfunfnv  25699  brrestrict  25702  dfrdg4  25703  tfrqfree  25704  altopthsn  25710  altopelaltxp  25725  altxpsspw  25726  mptelee  25738  brbtwn2  25748  colinearalg  25753  ax5seg  25781  axpasch  25784  axlowdimlem6  25790  axlowdimlem13  25797  axeuclidlem  25805  axeuclid  25806  axcontlem3  25809  axcontlem4  25810  axcontlem12  25818  brcolinear2  25896  broutsideof  25959  outsideofcom  25966  fvray  25979  fvline  25982  lineunray  25985  linecom  25988  linerflx2  25989  ellines  25990  bpoly2  26007  bpoly3  26008  rankeq1o  26016  elhf  26019  elhf2  26020  supadd  26138  mblfinlem  26143  ovoliunnfl  26147  voliunnfl  26149  mbfposadd  26153  cnambfre  26154  itg2addnclem2  26156  itg2addnclem3  26157  itg2addnc  26158  ecase13d  26206  trer  26209  elicc3  26210  finminlem  26211  opnrebl  26213  nn0prpw  26216  clsun  26221  fneval  26257  fnessref  26263  neibastop1  26278  neifg  26290  filnetlem4  26300  f1opr  26316  inixp  26320  sdclem2  26336  sdclem1  26337  fdc  26339  neificl  26349  istotbnd3  26370  sstotbnd3  26375  isbndx  26381  isbnd3b  26384  cntotbnd  26395  heibor1lem  26408  heibor1  26409  isdrngo2  26464  isdrngo3  26465  iscrngo2  26498  smprngopr  26552  isdmn2  26555  isfldidl2  26569  ispridlc  26570  isdmn3  26574  an43OLD  26586  prtlem70  26588  prtlem100  26594  n0el  26598  prter2  26620  funsnfsup  26633  cmpfiiin  26641  isnacs2  26650  elmzpcl  26673  diophrex  26724  2sbcrex  26733  sbcrot3  26737  sbcrot5  26738  3rexfrabdioph  26747  4rexfrabdioph  26748  6rexfrabdioph  26749  7rexfrabdioph  26750  fphpd  26767  fiphp3d  26770  rencldnfilem  26771  jm2.23  26957  expdiophlem1  26982  expdiophlem2  26983  expdioph  26984  dford4  26990  wopprc  26991  ttac  26997  fnwe2lem2  27016  islmodfg  27035  islnm2  27044  lnmlmic  27054  uvcvv0  27107  isnumbasgrplem1  27134  dfacbasgrp  27141  islinds2  27151  lmiclbs  27175  islnr2  27186  islnr3  27187  f1omvdco3  27260  issdrg2  27374  sdrgacs  27377  phisum  27386  isdomn3  27391  pm10.541  27430  pm10.542  27431  19.21vv  27442  19.36vv  27449  19.31vv  27450  19.37vv  27451  19.28vv  27452  pm11.6  27459  pm11.62  27461  pm14.12  27489  elnev  27506  evth2f  27553  elunif  27554  evthf  27565  stoweidlem31  27647  stoweidlem34  27650  stoweidlem51  27667  stoweidlem59  27675  aiffbbtat  27736  aisbbisfaisf  27737  aiffnbandciffatnotciffb  27739  abnotbtaxb  27751  mdandyvr0  27777  mdandyvr1  27778  mdandyvr2  27779  mdandyvr3  27780  mdandyvr4  27781  mdandyvr5  27782  mdandyvr6  27783  mdandyvr7  27784  rexrsb  27814  2rexsb  27815  2rexrsb  27816  cbvral2  27817  cbvrex2  27818  2ralbiim  27819  2reu5a  27822  rmoanim  27824  2rmoswap  27829  2reu1  27831  2reu3  27833  2reu4a  27834  afvpcfv0  27877  ffnaov  27930  ndmaovass  27937  ndmaovdistr  27938  raldifsnb  27946  rexdifpr  27947  dff14a  27959  dff14b  27960  f13dfv  27962  nn0fz0  27979  swrdnd  28001  usgra2pthspth  28035  usgra2pthlem1  28040  el2wlkonotot0  28069  usg2spthonot0  28086  frisusgranb  28101  frgra3v  28106  2pthfrgrarn  28113  2pthfrgra  28115  frgrawopreglem3  28149  frgrawopreglem4  28150  frgrawopreg  28152  frgrawopreg2  28154  usg2spot2nb  28168  usgreg2spot  28170  gte-lteh  28183  gt-lth  28184  sgnn  28238  onfrALTlem5  28339  onfrALTlem4  28340  onfrALTlem1  28345  2uasbanh  28359  dfvd2  28380  dfvd2an  28383  dfvd3  28392  dfvd3an  28395  eelT00  28517  eelTTT  28518  eelT12  28524  uunT1  28601  uunT1p1  28602  uun132p1  28607  un2122  28611  uunTT1p1  28615  uunTT1p2  28616  uunT11p1  28618  uunT11p2  28619  uunT12  28620  uunT12p1  28621  uunT12p2  28622  uunT12p3  28623  uunT12p4  28624  uunT12p5  28625  uun2221  28634  uun2221p1  28635  uun2221p2  28636  undif3VD  28703  onfrALTlem5VD  28706  onfrALTlem4VD  28707  onfrALTlem1VD  28711  2uasbanhVD  28732  bnj170  28768  bnj248  28770  bnj251  28772  bnj256  28776  bnj258  28778  bnj291  28781  bnj422  28785  bnj432  28786  bnj23  28789  bnj89  28792  bnj132  28797  bnj156  28801  bnj158  28802  bnj538  28814  bnj563  28817  bnj945  28850  bnj946  28851  bnj976  28854  bnj1098  28860  bnj1138  28865  bnj1209  28874  bnj1476  28924  bnj1542  28934  bnj110  28935  bnj91  28938  bnj92  28939  bnj106  28945  bnj118  28946  bnj124  28948  bnj125  28949  bnj153  28957  bnj207  28958  bnj222  28960  bnj518  28963  bnj535  28967  bnj539  28968  bnj543  28970  bnj553  28975  bnj556  28977  bnj558  28979  bnj571  28983  bnj605  28984  bnj591  28988  bnj594  28989  bnj580  28990  bnj609  28994  bnj611  28995  bnj865  29000  bnj849  29002  bnj916  29010  bnj917  29011  bnj934  29012  bnj929  29013  bnj944  29015  bnj953  29016  bnj1000  29018  bnj969  29023  bnj970  29024  bnj978  29026  bnj983  29028  bnj984  29029  bnj985  29030  bnj986  29031  bnj1021  29041  bnj1033  29044  bnj1049  29049  bnj1052  29050  bnj1083  29053  bnj1112  29058  bnj1030  29062  bnj1137  29070  bnj1189  29084  bnj1204  29087  bnj1253  29092  bnj1279  29093  bnj1373  29105  bnj1388  29108  bnj1398  29109  bnj1450  29125  sborNEW7  29270  sbrimNEW7  29271  sblimNEW7  29272  sbanNEW7  29273  sbbiNEW7  29274  sbid2NEW7  29286  sbco2dwAUX7  29289  sb8ewAUX7  29295  exsbOLDNEW7  29301  sbnf2NEW7  29309  2sb5NEW7  29310  2sb6NEW7  29311  sb6aNEW7  29312  sbexNEW7  29318  sbalvNEW7  29319  sblbisNEW7  29342  sbrbisNEW7  29343  sbrbifNEW7  29344  alrot3OLD7  29366  alrot4OLD7  29367  exrot3OLD7  29380  exrot4OLD7  29381  aaanOLD7  29382  eeorOLD7  29383  pm11.53OLD7  29384  eeanOLD7  29386  cbvex4vOLD7  29422  sbco2dOLD7  29437  sb8eOLD7  29441  sbcom2OLD7  29445  2sb5rfOLD7  29446  2sb6rfOLD7  29447  2exsbOLD7  29452  lsateln0  29478  islshpat  29500  lcvbr2  29505  lcvbr3  29506  lcvnbtwn3  29511  islfl  29543  lshpsmreu  29592  lub0N  29672  glb0N  29676  cvrnbtwn3  29759  leat2  29777  isat3  29790  iscvlat2N  29807  ishlat2  29836  ishlat3N  29837  hlrelat5N  29883  hlrelat2  29885  3dim0  29939  2dim  29952  islpln5  30017  islvol5  30061  4atlem3  30078  dalem20  30175  ispsubsp2  30228  snatpsubN  30232  pmapglb  30252  elpadd  30281  paddasslem17  30318  dalawlem13  30365  pclfinN  30382  polval2N  30388  pclfinclN  30432  lhpex2leN  30495  isltrn2N  30602  cdleme0nex  30772  cdleme22b  30823  cdlemftr3  31047  dibopelvalN  31626  dibopelval2  31628  dibelval3  31630  diblsmopel  31654  dicelval3  31663  dihglb2  31825  doch11  31856  islpolN  31966  lcfls1N  32018  mapdval4N  32115  mapdrvallem2  32128
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 178
  Copyright terms: Public domain W3C validator