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  1697  alrot3  1745  alrot4  1746  exrot3  1751  exrot4  1752  19.27  1831  19.28  1832  19.21-2  1876  nf2  1878  19.36  1881  19.37  1883  19.44  1887  19.45  1888  aaan  1895  eeor  1896  19.23vv  1904  pm11.53  1905  19.41vv  1914  19.41vvv  1915  19.41vvvv  1916  19.42vv  1919  19.42vvv  1920  4exdistr  1923  4exdistrOLD  1924  eean  1925  eeeanv  1927  cbvex4v  2047  sbor  2100  sbrim  2101  sblim  2102  sban  2103  sbbi  2105  sblbis  2106  sbrbis  2107  sbrbif  2108  sbid2  2118  sbco2d  2121  sbnf2  2142  2sb5  2146  2sb6  2147  sbcom2  2148  pm11.07  2149  sb6a  2151  2sb5rf  2152  2sb6rf  2153  sbex  2163  sbalv  2164  exsbOLD  2166  2exsb  2167  eujust  2241  euf  2245  cbveu  2259  eu2  2264  mo2  2268  sbmo  2269  mo3  2270  mo4f  2271  eu4  2278  moanim  2295  2mo  2317  2mos  2318  2eu1  2319  2eu3  2321  2eu4  2322  2eu6  2324  exists1  2328  abid  2376  eleq12i  2453  abeq2  2493  abeq2i  2495  clabel  2509  abid2f  2549  sbabel  2550  neeq12i  2563  necon1abii  2602  neanior  2636  ralnex  2660  rexnal  2661  ralinexa  2695  rexanali  2696  r3al  2707  r19.26-2  2783  ralbiim  2787  r19.30  2797  ralcomf  2810  rexcomf  2811  rexrot4  2815  reean  2818  3reeanv  2820  rabbi  2830  cbvralf  2870  cbvreu  2874  cbvral2v  2884  cbvrex2v  2885  cbvral3v  2886  cbvralsv  2887  cbvrexsv  2888  sbralie  2889  rabeq2i  2897  issetf  2905  2gencl  2929  3gencl  2930  ceqsex2  2936  ceqsex3v  2938  ceqsex6v  2940  ceqsex8v  2941  gencbvex  2942  spc3gv  2985  eqvincf  3008  ceqsrex2v  3015  elrab2  3038  ralab  3039  ralrab  3040  rexab  3041  rexrab  3042  ralab2  3043  rexab2  3045  eueq3  3053  morex  3062  euxfr2  3063  euxfr  3064  euind  3065  reu2  3066  reu6  3067  rmo4  3071  reu4  3072  reu7  3073  rmoim  3077  2reuswap  3080  reuind  3081  2reu5lem1  3083  2reu5lem2  3084  2reu5  3086  sbcco  3127  sbccomlem  3175  sbccom  3176  ra5  3189  rmo3  3192  csbco  3204  sbnfc2  3253  csbabg  3254  cbvralcsf  3255  cbvreucsf  3257  dfss  3279  dfss2f  3283  ss2ab  3355  dfpss2  3376  dfpss3  3377  psseq12i  3382  sspsstri  3393  difeqri  3411  raldifb  3431  uneqri  3433  ssequn2  3464  unss  3465  rexun  3471  ralunb  3472  elin2  3475  ineqri  3478  dfss1  3489  dfss5  3490  nsspssun  3518  indifdir  3541  inrab2  3558  rabun2  3564  reuun2  3568  eq0  3586  0el  3588  abn0  3590  0pss  3609  disjr  3613  disj1  3614  disjpss  3622  undif4  3628  difin0ss  3638  inssdif0  3639  uneqdifeq  3660  r19.3rz  3663  r19.3rzv  3665  ralidm  3675  pwss  3757  dfpr2  3774  ralsns  3788  rexsns  3789  eltpg  3795  ralprg  3801  rexprg  3802  raltpg  3803  rextpg  3804  rabrsn  3818  euabsn2  3819  eusn  3824  eldifsn  3871  rexdifsn  3875  tppreqb  3883  difsnpss  3885  pwpw0  3890  ssunsn  3903  eqsn  3904  sstp  3907  tpss  3908  prel12  3918  prnebg  3922  preqsn  3923  pwsnALT  3953  pwtp  3955  eluniab  3970  elunirab  3971  unipr  3972  dfnfc2  3976  uniun  3977  uniin  3978  unissb  3988  elintab  4004  elintrab  4005  ssintab  4010  ssintrab  4016  intun  4025  intpr  4026  elrint  4034  iuncom4  4043  iuneq2  4052  dfiun2g  4066  ssiinf  4082  elriin  4105  iunxiun  4115  pwssb  4119  iunpwss  4122  dfdisj2  4126  disjor  4138  disjors  4140  disjiun  4144  disjxiun  4151  disjxun  4152  cbvopab1  4220  dftr5  4247  trint  4259  inex1  4286  inuni  4304  axpweq  4318  nfnid  4335  zfpair2  4346  moabex  4364  exss  4368  elop  4371  otth  4382  copsex4g  4387  opeqsn  4394  opthwiener  4400  opelopabsbOLD  4405  brabga  4411  opelopabaf  4420  opabn0  4427  iunopab  4428  pwunss  4430  dfid3  4441  pocl  4452  sotric  4471  isso2i  4477  somo  4479  frminex  4504  dfepfr  4509  wefrc  4518  ordtri3or  4555  ordtri2  4558  elsuci  4589  elsucg  4590  sucel  4596  on0eqel  4640  uniuni  4657  reusv2lem4  4668  reusv2lem5  4669  reusv2  4670  reusv3  4672  reuxfr2d  4687  elpwun  4697  iunpw  4700  dfwe2  4703  onintrab2  4723  ordpwsuc  4736  ordzsl  4766  dflim4  4769  tfindsg  4781  tfindes  4783  findsg  4813  elxp  4836  opelxp  4849  brxp  4850  rabxp  4855  opthprc  4866  brab2a  4868  opeliunxp  4870  xpundi  4871  xpundir  4872  elvvv  4878  brinxp  4881  brab2ga  4892  xp0r  4897  ssrel2  4907  eqrelrel  4918  reliun  4936  reluni  4938  raliunxp  4955  rexiunxp  4956  ralxpf  4960  rexxpf  4961  iunxpf  4962  relop  4964  elcnv  4990  elcnv2  4991  dmin  5018  dmuni  5020  dmopab  5021  dmi  5025  rnopab  5056  elrnmpt1  5060  rncoeq  5080  resiexg  5129  dfima2  5146  dfima3  5147  elima2  5150  elima3  5151  imai  5159  elimasn  5170  epini  5175  dfse2  5178  cotr  5187  issref  5188  intasym  5190  asymref  5191  asymref2  5192  somin1  5211  cnvopab  5215  cnvi  5217  cnvdif  5219  imainss  5228  dfrel2  5262  dfrel3  5269  rnsnn0  5277  relsn2  5281  dmsnopg  5282  cnvcnvsn  5288  elxp4  5298  elxp5  5299  cnvresima  5300  mptpreima  5304  dfco2  5310  coundi  5312  coundir  5313  imaco  5316  coiun  5320  coi1  5326  relssdmrn  5331  relrelss  5334  ressn  5349  cnviin  5350  cnvpo  5351  cbviota  5364  dffun2  5405  dffun3  5406  dffun4  5407  dffun5  5408  dffun7  5420  dffun8  5421  dffun9  5422  funopab  5427  funun  5436  funcnvsn  5437  fntpg  5447  funcnv2  5451  funcnv  5452  fun2cnv  5454  fncnv  5456  fun11  5457  fununi  5458  imadif  5469  funimaexg  5471  fnunsn  5493  fnres  5502  fnopabg  5509  mptfng  5511  mptun  5516  fun  5548  fresaunres1  5557  fcnvres  5561  dff12  5579  f1cnvcnv  5588  funforn  5601  dff1o2  5620  dff1o5  5624  f1orn  5625  resdif  5637  ffoss  5648  f11o  5649  f1o00  5651  fo00  5652  elfv  5667  fv3  5685  dffn5f  5721  dffv2  5736  eqfnfv3  5769  fndmdifeq0  5776  fneqeql  5778  unpreima  5796  respreima  5799  dff4  5823  dffo3  5824  dffo5  5826  f1ompt  5831  ffnfvf  5835  fmptco  5841  fsn2  5848  ftpg  5856  fconst3  5895  fconst4  5896  idref  5919  abrexco  5926  opabex3d  5929  opabex3  5930  abexssex  5942  dff13  5944  dff13f  5946  foeqcnvco  5967  isocnv3  5992  isoini  5998  weniso  6015  oprabid  6045  0neqopab  6059  dfoprab2  6061  eqoprab2b  6072  dmoprab  6094  rnoprab  6096  eloprabga  6100  mpt2mptx  6104  resoprab  6106  ffnov  6114  fnov  6118  elrnmpt2  6123  ralrnmpt2  6124  rexrnmpt2  6125  oprabex3  6128  oprabrexex2  6129  ovid  6130  ov3  6150  ov6g  6151  foov  6160  ndmovdistr  6176  difxp  6320  elopaba  6349  fmpt2  6358  curry1  6378  curry2  6381  fsplit  6391  frxp  6393  xporderlem  6394  soxp  6396  mpt2xopovel  6408  brtpos2  6422  dmtpos  6428  tpostpos  6436  tpossym  6448  tposoprab  6452  sorpsscmpl  6470  opiota  6472  eusvobj2  6519  dfsmo2  6546  tfrlem3  6575  tfrlem7  6581  tfrlem9  6583  tfrlem9a  6584  tz7.48lem  6635  tz7.49c  6640  el1o  6680  dif1o  6681  ondif2  6683  brwitnlem  6688  oarec  6742  omeulem1  6762  omeu  6765  oeordi  6767  oeeui  6782  oeeu  6783  omopthlem1  6835  dfer2  6843  brdifun  6869  swoso  6873  eqerlem  6874  qsid  6907  iiner  6913  erinxp  6915  brecop  6934  eroveu  6936  erovlem  6937  ecopovsym  6943  mapval2  6980  mapsn  6992  elixp  7006  ixpeq2  7013  ixpin  7024  ixpiin  7025  mptelixpg  7036  ixpsnf1o  7039  boxriin  7041  domen  7058  isfi  7068  en1  7111  xpsnen  7129  xpcomco  7135  xpassen  7139  sbthlem9  7162  0sdomg  7173  2pwuninel  7199  ssenen  7218  nneneq  7227  php  7228  modom2  7247  ac6sfi  7288  frfi  7289  fimaxg  7291  elfpw  7344  fissuni  7347  dffi3  7372  marypha1lem  7374  marypha2lem2  7377  dfsup2  7383  dfsup2OLD  7384  wofib  7448  wemapso2lem  7453  wdom2d  7482  unxpwdom2  7490  dford2  7509  inf2  7512  inf3lem2  7518  axinf2  7529  zfinf2  7531  cantnfp1lem2  7569  oemapso  7572  cantnflem1  7579  trcl  7598  epfrs  7601  rankvalb  7657  r1elss  7666  unbndrank  7702  scott0s  7746  cplem1  7747  bnd2  7751  isnum2  7766  iscard2  7797  infxpenlem  7829  fseqenlem1  7839  acnnum  7867  infpwfien  7877  alephnbtwn2  7887  alephord2  7891  alephislim  7898  cardaleph  7904  alephval3  7925  aceq1  7932  aceq2  7934  dfac3  7936  dfac4  7937  dfac5lem1  7938  dfac5lem2  7939  dfac5lem3  7940  dfac5lem4  7941  dfac5lem5  7942  dfac2  7945  dfac0  7947  dfac1  7948  dfac8  7949  dfac9  7950  dfac12  7963  kmlem3  7966  kmlem4  7967  kmlem7  7970  kmlem8  7971  kmlem9  7972  kmlem13  7976  kmlem14  7977  kmlem15  7978  dfackm  7980  pwsdompw  8018  ackbij2lem2  8054  cf0  8065  cfval2  8074  cflim2  8077  cfss  8079  cfslb  8080  isfin3  8110  isfin5  8113  isfin6  8114  sdom2en01  8116  fin23lem25  8138  fin23lem26  8139  fin23lem40  8165  isfin1-2  8199  isfin1-3  8200  fin1a2lem5  8218  fin1a2lem6  8219  fin1a2lem12  8225  fin12  8227  domtriomlem  8256  axdc2lem  8262  axdc3lem2  8265  axdc3lem4  8267  axcclem  8271  ac6num  8293  ac6n  8299  zorn2lem6  8315  zornn0g  8319  ttukeylem6  8328  ttukey2g  8330  brdom7disj  8343  brdom6disj  8344  iunfo  8348  iundom2g  8349  konigthlem  8377  alephsuc3  8389  elgch  8431  fpwwe2lem9  8447  fpwwe2lem12  8450  fpwwe2lem13  8451  fpwwe2  8452  canth4  8456  canthwe  8460  wunex2  8547  uniwun  8549  axgroth5  8633  grothpw  8635  axgroth6  8637  grothprimlem  8642  grothprim  8643  elni  8687  ltexpi  8713  nqerf  8741  nqerid  8744  ordpipq  8753  recmulnq  8775  npomex  8807  genpnnp  8816  genpass  8820  addcompr  8832  mulcompr  8834  reclem2pr  8859  reclem3pr  8860  ltsosr  8903  ltasr  8909  mappsrpr  8917  map2psrpr  8919  opelcn  8938  elreal  8940  elreal2  8941  axaddf  8954  axmulf  8955  axicn  8959  axrrecex  8972  axpre-mulgt0  8977  xrlenlt  9077  ssxr  9079  leloe  9095  msq0i  9602  infm3  9900  supmullem2  9908  inelr  9923  arch  10151  elnnne0  10168  un0addcl  10186  un0mulcl  10187  nn0n0n1ge2b  10214  elnnz  10225  elznn0nn  10228  elznn0  10229  elznn  10230  elz2  10231  raluz2  10459  rexuz2  10461  nnwos  10477  eluz2b2  10481  eluz2b3  10482  ublbneg  10493  zmin  10503  elq  10509  ralrp  10563  rexrp  10564  ltxr  10648  xrnemnf  10651  xrleloe  10670  xrltlen  10672  xrrebnd  10689  xaddf  10743  xmullem  10776  xmullem2  10777  xrsupss  10820  xrinfmss  10821  elfzp1  11030  fzprval  11038  fztpval  11039  4fvwrd4  11052  fzm1  11058  fzolb  11076  fzolb2  11077  elfzo3  11086  fzouzsplit  11099  fzo0n0  11103  fzind2  11126  uzrdgfni  11226  subsq0i  11422  crreczi  11432  nn0le2msqi  11488  nn0opth2i  11492  hashkf  11548  hashinfxadd  11587  hashgt12el  11610  hashgt12el2  11611  hashtpg  11619  hashfun  11628  hashbclem  11629  hashbc  11630  hashf1lem2  11633  leiso  11636  iswrd  11657  f1oun2prg  11792  climeu  12277  lo1resb  12286  rlimresb  12287  o1resb  12288  climmpt2  12295  fsum2dlem  12482  rpnnen2  12753  sqr2irr  12776  divides  12782  odd2np1  12836  divalglem1  12842  divalglem6  12846  divalglem10  12850  divalgb  12852  bitsval2  12865  bitsmod  12876  bitscmp  12878  smueqlem  12930  isprm2  13015  isprm3  13016  isprm4  13017  isprm5  13040  pythagtriplem19  13135  pythagtrip  13136  pceu  13148  prmreclem2  13213  4sqlem2  13245  4sqlem12  13252  vdwpc  13276  vdwnn  13294  dec5dvds2  13329  pwsle  13642  imasleval  13694  xpsfrnel  13716  xpsfrnel2  13718  xpsle  13734  isacs2  13806  mreacs  13811  iscatd2  13834  comfeq  13860  oppcsect  13927  isfunc  13989  funcoppc  14000  isffth2  14041  fucinv  14098  elhoma  14115  setcinv  14173  ispos  14332  ispos2  14333  tosso  14393  istsr2  14578  spwmo  14586  ismnd  14620  mndcl  14623  issubm  14676  gsumwspan  14719  issubg  14872  isnsg2  14898  eqger  14918  isgim2  14980  giclcl  14987  gicrcl  14988  gicsubgen  14993  gaorber  15013  resscntz  15058  cntzrec  15060  efgval2  15284  efgsfo  15299  efgrelexlemb  15310  isabl2  15348  iscyggen2  15419  iscyg2  15420  iscyg3  15424  lt6abl  15432  gsumval3eu  15441  gsum2d2  15476  dmdprdd  15488  subgdmdprd  15520  iscrng2  15607  dvdsrtr  15685  isunit  15690  isnirred  15733  isirred2  15734  isrhm  15752  isdrng2  15773  drngprop  15774  isabv  15835  issrng  15866  islmod  15882  islss  15939  lss1d  15967  islmim2  16066  lmiclcl  16070  lmicrcl  16071  lsmelval2  16085  lspsolvlem  16142  lspsncv0  16146  islpidl  16245  islpir2  16250  isnzr2  16262  isdomn2  16287  fiidomfld  16296  aspval2  16333  mplcoe1  16456  mplcoe2  16458  evlslem4  16492  xrsdsreclb  16669  unocv  16831  iunocv  16832  ishil2  16870  isobs  16871  obselocv  16879  iinopn  16899  istps4OLD  16912  istps5OLD  16913  istps  16925  istps2  16926  isbasis2g  16937  tgval2  16945  elcls  17061  neipeltop  17117  neiptopuni  17118  islpi  17136  isperf2  17139  isperf3  17140  neitr  17167  restntr  17169  ordtrest2lem  17190  cnrest  17272  ist0-3  17332  ist1-2  17334  ist1-3  17336  nrmsep3  17342  isnrm2  17345  perfcls  17352  ordthaus  17371  cmpcov2  17376  cmpsub  17386  hauscmplem  17392  cmpfi  17394  iscon2  17399  dfcon2  17404  is1stc2  17427  is2ndc  17431  1stcelcls  17446  1stccn  17448  llyi  17459  subislly  17466  iskgen3  17503  txuni2  17519  ptpjpre1  17525  ptbasin  17531  tx1cn  17563  tx2cn  17564  uptx  17579  txdis1cn  17589  ptrescn  17593  txtube  17594  txcmplem1  17595  hausdiag  17599  txkgen  17606  xkohaus  17607  xkococnlem  17613  xkoinjcn  17641  qtopeu  17670  isr0  17691  regr1lem2  17694  hmphsym  17736  elmptrab2  17782  isfbas  17783  isfbas2  17789  trfbas  17798  snfil  17818  fbunfip  17823  elfg  17825  fgcl  17832  fbasrn  17838  filuni  17839  trfil2  17841  cfinfil  17847  csdfil  17848  supfil  17849  ufinffr  17883  rnelfmlem  17906  elflim2  17918  hausflim  17935  hauspwpwf1  17941  txflf  17960  isfcls2  17967  fclsopn  17968  fclsrest  17978  alexsubALTlem2  18001  alexsubALTlem3  18002  alexsubALTlem4  18003  tmdcn2  18041  divstgplem  18072  divstgphaus  18074  tsmssubm  18094  istdrg2  18129  ustfilxp  18164  ust0  18171  fmucndlem  18243  metn0  18299  prdsxmetlem  18307  imasdsf1olem  18312  xpsdsval  18320  blres  18352  xmeterval  18353  xmeter  18354  isxms2  18369  isms2  18371  metustsym  18476  dscopn  18493  isngp3  18517  isnvc2  18606  isnghm  18629  qtopbaslem  18664  xrtgioo  18709  zcld  18716  elii1  18832  pi1cpbl  18941  tchcph  19066  cmetss  19139  bcth  19152  lssbn  19174  ishl2  19192  minveclem3b  19197  minveclem6  19203  pmltpc  19215  ovolfcl  19231  ovolgelb  19244  ovolunlem1  19261  ovoliunlem1  19266  ismbl  19290  ismbl2  19291  iundisj2  19311  dyadmax  19358  dyadmbllem  19359  vitalilem2  19369  mbfimaopnlem  19415  itg1climres  19474  itg2l  19489  itg2leub  19494  iblcnlem1  19547  ellimc2  19632  ellimc3  19634  limcmpt  19638  limcres  19641  elaa  20101  aaliou3lem9  20135  taylthlem2  20158  ulmcau  20179  pilem1  20235  sincosq1lem  20273  sineq0  20297  coseq1  20298  ellogrn  20325  logtayl2  20421  cxpcn3lem  20499  cxpcn3  20500  cubic  20557  atandm  20584  atandm2  20585  atandm4  20587  atans2  20639  xrlimcnp  20675  wilthlem2  20720  dvdsflsumcom  20841  dvdsmulf1o  20847  fsumvma  20865  logfac2  20869  dchrelbas2  20889  dchrelbas3  20890  lgsdir2lem4  20978  lgsquadlem1  21006  lgsquadlem2  21007  2sqlem1  21015  pntlem3  21171  ostth  21201  usgra2edg1  21270  usgraedg4  21273  nbgrasym  21316  nb3grapr  21329  nb3grapr2  21330  cusgra2v  21338  cusgra3v  21340  uvtx01vtx  21368  trls  21401  0wlk  21410  0trl  21411  wlkntrllem1  21414  wlkntrllem3  21416  wlkntrllem4  21417  3v3e3cycl1  21480  3v3e3cycl2  21500  vdgrun  21521  vdgrfiun  21522  eupath  21552  avril1  21606  grpoidinvlem3  21643  issubgo  21740  islno  22103  nmoubi  22122  nmobndseqi  22129  siii  22203  minvecolem5  22232  minvecolem6  22233  hvsubaddi  22417  normsub0i  22486  bcsiALT  22530  hcau  22535  hlimadd  22544  hhcmpl  22551  hhcms  22554  issh2  22560  isch2  22575  hlim0  22587  isch3  22593  norm1exi  22601  elch0  22605  hhsssh2  22619  choc0  22677  pjhtheu  22745  pjpreeq  22749  omlsilem  22753  pjoc2i  22789  chsscon1i  22813  spanuni  22895  h1deoi  22900  h1dei  22901  elspansni  22909  cmcm4i  22946  cmbr3i  22951  cmbr4i  22952  osumcor2i  22995  5oalem7  23011  3oalem3  23015  pjss2i  23031  mayete3iOLD  23080  elcnop  23209  ellnop  23210  elhmop  23225  elcnfn  23234  ellnfn  23235  cnvadj  23244  nmopub  23260  nmfnleub  23277  eleigvec  23309  nmop0  23338  nmfn0  23339  nmopun  23366  lncnopbd  23389  riesz2  23418  nmopcoadj0i  23455  rnbra  23459  pjnmopi  23500  pjssdif1i  23527  pjin2i  23545  pjin3i  23546  pjclem1  23547  cvbr2  23635  cvnbtwn3  23640  cvnbtwn4  23641  mdsl2bi  23675  mdsldmd1i  23683  elat2  23692  chrelat2i  23717  atomli  23734  chirredi  23746  mdsymlem6  23760  mdsymlem8  23762  sumdmdii  23767  dmdbr5ati  23774  cdj3i  23793  xfree2  23797  abeq2f  23805  r19.41vv  23815  mo5f  23817  nmo  23818  2reuswap2  23820  reuxfr3d  23821  rexunirn  23823  rmo3f  23827  rmo4fOLD  23828  rmo4f  23829  difeq  23843  disjorf  23866  disjorsf  23867  iundisj2f  23874  dfrel4  23878  suppss2f  23893  abfmpunirn  23907  fmptdF  23912  mptfnf  23916  fmptcof2  23919  funcnvmptOLD  23924  funcnvmpt  23925  funcnv5mpt  23926  gtiso  23930  disjdsct  23932  iundisj2fi  23992  elxrge02  24018  ofldsqr  24067  eldiftp  24190  esumnul  24240  esumpfinvalf  24263  isrnsigaOLD  24292  isrnsiga  24293  measiuns  24366  elunirnmbfm  24398  1stmbfm  24405  2ndmbfm  24406  dya2iocnrect  24426  ballotlemelo  24525  ballotlemodife  24535  ballotlem4  24536  eldmgm  24586  subfacp1lem5  24650  subfacp1lem6  24651  cvmscld  24740  cvmlift2lem12  24781  ghomgrpilem2  24877  axextprim  24930  axrepprim  24931  axunprim  24932  axpowprim  24933  axregprim  24934  axinfprim  24935  axacprim  24936  untangtr  24943  biimpexp  24953  dfid4  24963  divelunit  24965  divcnvshft  24991  divcnvlin  24992  ntrivcvgmul  25010  prodsn  25066  dftr6  25132  coep  25133  coepr  25134  dffr5  25135  dfpo2  25137  cnvco1  25142  cnvco2  25143  eldm3  25144  fundmpss  25147  dfdm5  25157  dfrn5  25158  elpotr  25162  dford5reg  25163  dfon2lem5  25168  dfon2lem6  25169  dfon2lem8  25171  dfon2lem9  25172  dfon2  25173  wfi  25232  eltrpred  25254  frind  25268  poseq  25278  soseq  25279  wfrlem4  25284  wfrlem5  25285  wfrlem9  25289  wfrlem11  25291  wfrlem12  25292  wfrlem13  25293  wfrlem14  25294  wfrlem15  25295  tfrALTlem  25301  tfr3ALT  25304  frrlem5  25310  frrlem5e  25314  frrlem11  25318  nosgnn0  25337  nodenselem5  25364  nobnddown  25380  nofulllem5  25385  elsymdif  25392  brsymdif  25397  brtxp  25445  brpprod  25450  brpprod3b  25452  brsset  25454  idsset  25455  dfon3  25457  brtxpsd  25459  brtxpsd2  25460  brbigcup  25463  elfix  25468  dffix2  25470  ellimits  25475  dffun10  25478  elfuns  25479  snelsingles  25486  dfiota3  25487  brcart  25496  brimg  25501  brapply  25502  brcup  25503  brcap  25504  brsuccf  25505  funpartlem  25506  funpartfun  25507  fullfunfnv  25510  brrestrict  25513  dfrdg4  25514  tfrqfree  25515  altopthsn  25521  altopelaltxp  25536  altxpsspw  25537  mptelee  25549  brbtwn2  25559  colinearalg  25564  ax5seg  25592  axpasch  25595  axlowdimlem6  25601  axlowdimlem13  25608  axeuclidlem  25616  axeuclid  25617  axcontlem3  25620  axcontlem4  25621  axcontlem12  25629  brcolinear2  25707  broutsideof  25770  outsideofcom  25777  fvray  25790  fvline  25793  lineunray  25796  linecom  25799  linerflx2  25800  ellines  25801  bpoly2  25818  bpoly3  25819  rankeq1o  25827  elhf  25830  elhf2  25831  supadd  25949  ovoliunnfl  25954  voliunnfl  25956  itg2addnclem2  25959  itg2addnc  25960  ecase13d  26008  trer  26011  elicc3  26012  finminlem  26013  opnrebl  26015  nn0prpw  26018  clsun  26023  fneval  26059  fnessref  26065  neibastop1  26080  neifg  26092  filnetlem4  26102  f1opr  26118  inixp  26122  sdclem2  26138  sdclem1  26139  fdc  26141  neificl  26151  istotbnd3  26172  sstotbnd3  26177  isbndx  26183  isbnd3b  26186  cntotbnd  26197  heibor1lem  26210  heibor1  26211  isdrngo2  26266  isdrngo3  26267  iscrngo2  26300  smprngopr  26354  isdmn2  26357  isfldidl2  26371  ispridlc  26372  isdmn3  26376  an43OLD  26388  prtlem70  26390  prtlem100  26396  n0el  26400  prter2  26422  funsnfsup  26435  cmpfiiin  26443  isnacs2  26452  elmzpcl  26475  diophrex  26526  2sbcrex  26535  sbcrot3  26539  sbcrot5  26540  3rexfrabdioph  26549  4rexfrabdioph  26550  6rexfrabdioph  26551  7rexfrabdioph  26552  fphpd  26569  fiphp3d  26572  rencldnfilem  26573  jm2.23  26759  expdiophlem1  26784  expdiophlem2  26785  expdioph  26786  dford4  26792  wopprc  26793  ttac  26799  fnwe2lem2  26818  islmodfg  26837  islnm2  26846  lnmlmic  26856  uvcvv0  26909  isnumbasgrplem1  26936  dfacbasgrp  26943  islinds2  26953  lmiclbs  26977  islnr2  26988  islnr3  26989  f1omvdco3  27062  issdrg2  27176  sdrgacs  27179  phisum  27188  isdomn3  27193  pm10.541  27232  pm10.542  27233  19.21vv  27244  19.36vv  27251  19.31vv  27252  19.37vv  27253  19.28vv  27254  pm11.6  27261  pm11.62  27263  pm14.12  27291  elnev  27308  evth2f  27355  elunif  27356  evthf  27367  stoweidlem31  27449  stoweidlem34  27452  stoweidlem51  27469  stoweidlem59  27477  aiffbbtat  27538  aisbbisfaisf  27539  aiffnbandciffatnotciffb  27541  abnotbtaxb  27553  mdandyvr0  27579  mdandyvr1  27580  mdandyvr2  27581  mdandyvr3  27582  mdandyvr4  27583  mdandyvr5  27584  mdandyvr6  27585  mdandyvr7  27586  rexrsb  27616  2rexsb  27617  2rexrsb  27618  cbvral2  27619  cbvrex2  27620  2ralbiim  27621  2reu5a  27624  rmoanim  27626  2rmoswap  27631  2reu1  27633  2reu3  27635  2reu4a  27636  afvpcfv0  27680  ffnaov  27733  ndmaovass  27740  ndmaovdistr  27741  frisusgranb  27751  frgra3v  27756  2pthfrgrarn  27763  2pthfrgra  27765  frgrawopreglem3  27799  frgrawopreglem4  27800  frgrawopreg  27802  frgrawopreg2  27804  gte-lteh  27816  gt-lth  27817  sgnn  27871  onfrALTlem5  27972  onfrALTlem4  27973  onfrALTlem1  27978  2uasbanh  27992  dfvd2  28013  dfvd2an  28016  dfvd3  28025  dfvd3an  28028  eelT00  28150  eelTTT  28151  eelT12  28157  uunT1  28234  uunT1p1  28235  uun132p1  28240  un2122  28244  uunTT1p1  28248  uunTT1p2  28249  uunT11p1  28251  uunT11p2  28252  uunT12  28253  uunT12p1  28254  uunT12p2  28255  uunT12p3  28256  uunT12p4  28257  uunT12p5  28258  uun2221  28267  uun2221p1  28268  uun2221p2  28269  undif3VD  28336  onfrALTlem5VD  28339  onfrALTlem4VD  28340  onfrALTlem1VD  28344  2uasbanhVD  28365  bnj170  28401  bnj248  28403  bnj251  28405  bnj256  28409  bnj258  28411  bnj291  28414  bnj422  28418  bnj432  28419  bnj23  28422  bnj89  28425  bnj132  28430  bnj156  28434  bnj158  28435  bnj538  28447  bnj563  28450  bnj945  28483  bnj946  28484  bnj976  28487  bnj1098  28493  bnj1138  28498  bnj1209  28507  bnj1476  28557  bnj1542  28567  bnj110  28568  bnj91  28571  bnj92  28572  bnj106  28578  bnj118  28579  bnj124  28581  bnj125  28582  bnj153  28590  bnj207  28591  bnj222  28593  bnj518  28596  bnj535  28600  bnj539  28601  bnj543  28603  bnj553  28608  bnj556  28610  bnj558  28612  bnj571  28616  bnj605  28617  bnj591  28621  bnj594  28622  bnj580  28623  bnj609  28627  bnj611  28628  bnj865  28633  bnj849  28635  bnj916  28643  bnj917  28644  bnj934  28645  bnj929  28646  bnj944  28648  bnj953  28649  bnj1000  28651  bnj969  28656  bnj970  28657  bnj978  28659  bnj983  28661  bnj984  28662  bnj985  28663  bnj986  28664  bnj1021  28674  bnj1033  28677  bnj1049  28682  bnj1052  28683  bnj1083  28686  bnj1112  28691  bnj1030  28695  bnj1137  28703  bnj1189  28717  bnj1204  28720  bnj1253  28725  bnj1279  28726  bnj1373  28738  bnj1388  28741  bnj1398  28742  bnj1450  28758  sborNEW7  28903  sbrimNEW7  28904  sblimNEW7  28905  sbanNEW7  28906  sbbiNEW7  28907  sbid2NEW7  28919  sbco2dwAUX7  28922  sb8ewAUX7  28928  exsbOLDNEW7  28934  sbnf2NEW7  28942  2sb5NEW7  28943  2sb6NEW7  28944  sb6aNEW7  28945  sbexNEW7  28951  sbalvNEW7  28952  sblbisNEW7  28975  sbrbisNEW7  28976  sbrbifNEW7  28977  alrot3OLD7  28999  alrot4OLD7  29000  exrot3OLD7  29013  exrot4OLD7  29014  aaanOLD7  29015  eeorOLD7  29016  pm11.53OLD7  29017  eeanOLD7  29019  cbvex4vOLD7  29055  sbco2dOLD7  29070  sb8eOLD7  29074  sbcom2OLD7  29078  2sb5rfOLD7  29079  2sb6rfOLD7  29080  2exsbOLD7  29085  lsateln0  29111  islshpat  29133  lcvbr2  29138  lcvbr3  29139  lcvnbtwn3  29144  islfl  29176  lshpsmreu  29225  lub0N  29305  glb0N  29309  cvrnbtwn3  29392  leat2  29410  isat3  29423  iscvlat2N  29440  ishlat2  29469  ishlat3N  29470  hlrelat5N  29516  hlrelat2  29518  3dim0  29572  2dim  29585  islpln5  29650  islvol5  29694  4atlem3  29711  dalem20  29808  ispsubsp2  29861  snatpsubN  29865  pmapglb  29885  elpadd  29914  paddasslem17  29951  dalawlem13  29998  pclfinN  30015  polval2N  30021  pclfinclN  30065  lhpex2leN  30128  isltrn2N  30235  cdleme0nex  30405  cdleme22b  30456  cdlemftr3  30680  dibopelvalN  31259  dibopelval2  31261  dibelval3  31263  diblsmopel  31287  dicelval3  31296  dihglb2  31458  doch11  31489  islpolN  31599  lcfls1N  31651  mapdval4N  31748  mapdrvallem2  31761
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