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  2038  sbor  2092  sbrim  2093  sblim  2094  sban  2095  sbbi  2097  sblbis  2098  sbrbis  2099  sbrbif  2100  sbid2  2110  sbco2d  2113  sbnf2  2134  2sb5  2138  2sb6  2139  sbcom2  2140  pm11.07  2141  sb6a  2143  2sb5rf  2144  2sb6rf  2145  sbex  2155  sbalv  2156  exsbOLD  2158  2exsb  2159  eujust  2233  euf  2237  cbveu  2251  eu2  2256  mo2  2260  sbmo  2261  mo3  2262  mo4f  2263  eu4  2270  moanim  2287  2mo  2309  2mos  2310  2eu1  2311  2eu3  2313  2eu4  2314  2eu6  2316  exists1  2320  abid  2368  eleq12i  2445  abeq2  2485  abeq2i  2487  clabel  2501  abid2f  2541  sbabel  2542  neeq12i  2555  necon1abii  2594  neanior  2628  ralnex  2652  rexnal  2653  ralinexa  2687  rexanali  2688  r3al  2699  r19.26-2  2775  ralbiim  2779  r19.30  2789  ralcomf  2802  rexcomf  2803  rexrot4  2807  reean  2810  3reeanv  2812  rabbi  2822  cbvralf  2862  cbvreu  2866  cbvral2v  2876  cbvrex2v  2877  cbvral3v  2878  cbvralsv  2879  cbvrexsv  2880  sbralie  2881  rabeq2i  2889  issetf  2897  2gencl  2921  3gencl  2922  ceqsex2  2928  ceqsex3v  2930  ceqsex6v  2932  ceqsex8v  2933  gencbvex  2934  spc3gv  2977  eqvincf  3000  ceqsrex2v  3007  elrab2  3030  ralab  3031  ralrab  3032  rexab  3033  rexrab  3034  ralab2  3035  rexab2  3037  eueq3  3045  morex  3054  euxfr2  3055  euxfr  3056  euind  3057  reu2  3058  reu6  3059  rmo4  3063  reu4  3064  reu7  3065  rmoim  3069  2reuswap  3072  reuind  3073  2reu5lem1  3075  2reu5lem2  3076  2reu5  3078  sbcco  3119  sbccomlem  3167  sbccom  3168  ra5  3181  rmo3  3184  csbco  3196  sbnfc2  3245  csbabg  3246  cbvralcsf  3247  cbvreucsf  3249  dfss  3271  dfss2f  3275  ss2ab  3347  dfpss2  3368  dfpss3  3369  psseq12i  3374  sspsstri  3385  difeqri  3403  raldifb  3423  uneqri  3425  ssequn2  3456  unss  3457  rexun  3463  ralunb  3464  elin2  3467  ineqri  3470  dfss1  3481  dfss5  3482  nsspssun  3510  indifdir  3533  inrab2  3550  rabun2  3556  reuun2  3560  eq0  3578  0el  3580  abn0  3582  0pss  3601  disjr  3605  disj1  3606  disjpss  3614  undif4  3620  difin0ss  3630  inssdif0  3631  uneqdifeq  3652  r19.3rz  3655  r19.3rzv  3657  ralidm  3667  pwss  3749  dfpr2  3766  ralsns  3780  rexsns  3781  eltpg  3787  ralprg  3793  rexprg  3794  raltpg  3795  rextpg  3796  rabrsn  3810  euabsn2  3811  eusn  3816  eldifsn  3863  rexdifsn  3867  tppreqb  3875  difsnpss  3877  pwpw0  3882  ssunsn  3895  eqsn  3896  sstp  3899  tpss  3900  prel12  3910  prnebg  3914  preqsn  3915  pwsnALT  3945  pwtp  3947  eluniab  3962  elunirab  3963  unipr  3964  dfnfc2  3968  uniun  3969  uniin  3970  unissb  3980  elintab  3996  elintrab  3997  ssintab  4002  ssintrab  4008  intun  4017  intpr  4018  elrint  4026  iuncom4  4035  iuneq2  4044  dfiun2g  4058  ssiinf  4074  elriin  4097  iunxiun  4107  pwssb  4111  iunpwss  4114  dfdisj2  4118  disjor  4130  disjors  4132  disjiun  4136  disjxiun  4143  disjxun  4144  cbvopab1  4212  dftr5  4239  trint  4251  inex1  4278  inuni  4296  axpweq  4310  nfnid  4327  zfpair2  4338  moabex  4356  exss  4360  elop  4363  otth  4374  copsex4g  4379  opeqsn  4386  opthwiener  4392  opelopabsbOLD  4397  brabga  4403  opelopabaf  4412  opabn0  4419  iunopab  4420  pwunss  4422  dfid3  4433  pocl  4444  sotric  4463  isso2i  4469  somo  4471  frminex  4496  dfepfr  4501  wefrc  4510  ordtri3or  4547  ordtri2  4550  elsuci  4581  elsucg  4582  sucel  4588  on0eqel  4632  uniuni  4649  reusv2lem4  4660  reusv2lem5  4661  reusv2  4662  reusv3  4664  reuxfr2d  4679  elpwun  4689  iunpw  4692  dfwe2  4695  onintrab2  4715  ordpwsuc  4728  ordzsl  4758  dflim4  4761  tfindsg  4773  tfindes  4775  findsg  4805  elxp  4828  opelxp  4841  brxp  4842  rabxp  4847  opthprc  4858  brab2a  4860  opeliunxp  4862  xpundi  4863  xpundir  4864  elvvv  4870  brinxp  4873  brab2ga  4884  xp0r  4889  ssrel2  4899  eqrelrel  4910  reliun  4928  reluni  4930  raliunxp  4947  rexiunxp  4948  ralxpf  4952  rexxpf  4953  iunxpf  4954  relop  4956  elcnv  4982  elcnv2  4983  dmin  5010  dmuni  5012  dmopab  5013  dmi  5017  rnopab  5048  elrnmpt1  5052  rncoeq  5072  resiexg  5121  dfima2  5138  dfima3  5139  elima2  5142  elima3  5143  imai  5151  elimasn  5162  epini  5167  dfse2  5170  cotr  5179  issref  5180  intasym  5182  asymref  5183  asymref2  5184  somin1  5203  cnvopab  5207  cnvi  5209  cnvdif  5211  imainss  5220  dfrel2  5254  dfrel3  5261  rnsnn0  5269  relsn2  5273  dmsnopg  5274  cnvcnvsn  5280  elxp4  5290  elxp5  5291  cnvresima  5292  mptpreima  5296  dfco2  5302  coundi  5304  coundir  5305  imaco  5308  coiun  5312  coi1  5318  relssdmrn  5323  relrelss  5326  ressn  5341  cnviin  5342  cnvpo  5343  cbviota  5356  dffun2  5397  dffun3  5398  dffun4  5399  dffun5  5400  dffun7  5412  dffun8  5413  dffun9  5414  funopab  5419  funun  5428  funcnvsn  5429  fntpg  5439  funcnv2  5443  funcnv  5444  fun2cnv  5446  fncnv  5448  fun11  5449  fununi  5450  imadif  5461  funimaexg  5463  fnunsn  5485  fnres  5494  fnopabg  5501  mptfng  5503  mptun  5508  fun  5540  fresaunres1  5549  fcnvres  5553  dff12  5571  f1cnvcnv  5580  funforn  5593  dff1o2  5612  dff1o5  5616  f1orn  5617  resdif  5629  ffoss  5640  f11o  5641  f1o00  5643  fo00  5644  elfv  5659  fv3  5677  dffn5f  5713  dffv2  5728  eqfnfv3  5761  fndmdifeq0  5768  fneqeql  5770  unpreima  5788  respreima  5791  dff4  5815  dffo3  5816  dffo5  5818  f1ompt  5823  ffnfvf  5827  fmptco  5833  fsn2  5840  ftpg  5848  fconst3  5887  fconst4  5888  idref  5911  abrexco  5918  opabex3d  5921  opabex3  5922  abexssex  5934  dff13  5936  dff13f  5938  foeqcnvco  5959  isocnv3  5984  isoini  5990  weniso  6007  oprabid  6037  0neqopab  6051  dfoprab2  6053  eqoprab2b  6064  dmoprab  6086  rnoprab  6088  eloprabga  6092  mpt2mptx  6096  resoprab  6098  ffnov  6106  fnov  6110  elrnmpt2  6115  ralrnmpt2  6116  rexrnmpt2  6117  oprabex3  6120  oprabrexex2  6121  ovid  6122  ov3  6142  ov6g  6143  foov  6152  ndmovdistr  6168  difxp  6312  elopaba  6341  fmpt2  6350  curry1  6370  curry2  6373  fsplit  6383  frxp  6385  xporderlem  6386  soxp  6388  mpt2xopovel  6400  brtpos2  6414  dmtpos  6420  tpostpos  6428  tpossym  6440  tposoprab  6444  sorpsscmpl  6462  opiota  6464  eusvobj2  6511  dfsmo2  6538  tfrlem3  6567  tfrlem7  6573  tfrlem9  6575  tfrlem9a  6576  tz7.48lem  6627  tz7.49c  6632  el1o  6672  dif1o  6673  ondif2  6675  brwitnlem  6680  oarec  6734  omeulem1  6754  omeu  6757  oeordi  6759  oeeui  6774  oeeu  6775  omopthlem1  6827  dfer2  6835  brdifun  6861  swoso  6865  eqerlem  6866  qsid  6899  iiner  6905  erinxp  6907  brecop  6926  eroveu  6928  erovlem  6929  ecopovsym  6935  mapval2  6972  mapsn  6984  elixp  6998  ixpeq2  7005  ixpin  7016  ixpiin  7017  mptelixpg  7028  ixpsnf1o  7031  boxriin  7033  domen  7050  isfi  7060  en1  7103  xpsnen  7121  xpcomco  7127  xpassen  7131  sbthlem9  7154  0sdomg  7165  2pwuninel  7191  ssenen  7210  nneneq  7219  php  7220  modom2  7239  ac6sfi  7280  frfi  7281  fimaxg  7283  elfpw  7336  fissuni  7339  dffi3  7364  marypha1lem  7366  marypha2lem2  7369  dfsup2  7375  dfsup2OLD  7376  wofib  7440  wemapso2lem  7445  wdom2d  7474  unxpwdom2  7482  dford2  7501  inf2  7504  inf3lem2  7510  axinf2  7521  zfinf2  7523  cantnfp1lem2  7561  oemapso  7564  cantnflem1  7571  trcl  7590  epfrs  7593  rankvalb  7649  r1elss  7658  unbndrank  7694  scott0s  7738  cplem1  7739  bnd2  7743  isnum2  7758  iscard2  7789  infxpenlem  7821  fseqenlem1  7831  acnnum  7859  infpwfien  7869  alephnbtwn2  7879  alephord2  7883  alephislim  7890  cardaleph  7896  alephval3  7917  aceq1  7924  aceq2  7926  dfac3  7928  dfac4  7929  dfac5lem1  7930  dfac5lem2  7931  dfac5lem3  7932  dfac5lem4  7933  dfac5lem5  7934  dfac2  7937  dfac0  7939  dfac1  7940  dfac8  7941  dfac9  7942  dfac12  7955  kmlem3  7958  kmlem4  7959  kmlem7  7962  kmlem8  7963  kmlem9  7964  kmlem13  7968  kmlem14  7969  kmlem15  7970  dfackm  7972  pwsdompw  8010  ackbij2lem2  8046  cf0  8057  cfval2  8066  cflim2  8069  cfss  8071  cfslb  8072  isfin3  8102  isfin5  8105  isfin6  8106  sdom2en01  8108  fin23lem25  8130  fin23lem26  8131  fin23lem40  8157  isfin1-2  8191  isfin1-3  8192  fin1a2lem5  8210  fin1a2lem6  8211  fin1a2lem12  8217  fin12  8219  domtriomlem  8248  axdc2lem  8254  axdc3lem2  8257  axdc3lem4  8259  axcclem  8263  ac6num  8285  ac6n  8291  zorn2lem6  8307  zornn0g  8311  ttukeylem6  8320  ttukey2g  8322  brdom7disj  8335  brdom6disj  8336  iunfo  8340  iundom2g  8341  konigthlem  8369  alephsuc3  8381  elgch  8423  fpwwe2lem9  8439  fpwwe2lem12  8442  fpwwe2lem13  8443  fpwwe2  8444  canth4  8448  canthwe  8452  wunex2  8539  uniwun  8541  axgroth5  8625  grothpw  8627  axgroth6  8629  grothprimlem  8634  grothprim  8635  elni  8679  ltexpi  8705  nqerf  8733  nqerid  8736  ordpipq  8745  recmulnq  8767  npomex  8799  genpnnp  8808  genpass  8812  addcompr  8824  mulcompr  8826  reclem2pr  8851  reclem3pr  8852  ltsosr  8895  ltasr  8901  mappsrpr  8909  map2psrpr  8911  opelcn  8930  elreal  8932  elreal2  8933  axaddf  8946  axmulf  8947  axicn  8951  axrrecex  8964  axpre-mulgt0  8969  xrlenlt  9069  ssxr  9071  leloe  9087  msq0i  9594  infm3  9892  supmullem2  9900  inelr  9915  arch  10143  elnnne0  10160  un0addcl  10178  un0mulcl  10179  nn0n0n1ge2b  10206  elnnz  10217  elznn0nn  10220  elznn0  10221  elznn  10222  elz2  10223  raluz2  10451  rexuz2  10453  nnwos  10469  eluz2b2  10473  eluz2b3  10474  ublbneg  10485  zmin  10495  elq  10501  ralrp  10555  rexrp  10556  ltxr  10640  xrnemnf  10643  xrleloe  10662  xrltlen  10664  xrrebnd  10681  xaddf  10735  xmullem  10768  xmullem2  10769  xrsupss  10812  xrinfmss  10813  elfzp1  11022  fzprval  11030  fztpval  11031  4fvwrd4  11044  fzm1  11050  fzolb  11068  fzolb2  11069  elfzo3  11078  fzouzsplit  11091  fzo0n0  11095  fzind2  11118  uzrdgfni  11218  subsq0i  11414  crreczi  11424  nn0le2msqi  11480  nn0opth2i  11484  hashkf  11540  hashinfxadd  11579  hashgt12el  11602  hashgt12el2  11603  hashtpg  11611  hashfun  11620  hashbclem  11621  hashbc  11622  hashf1lem2  11625  leiso  11628  iswrd  11649  f1oun2prg  11784  climeu  12269  lo1resb  12278  rlimresb  12279  o1resb  12280  climmpt2  12287  fsum2dlem  12474  rpnnen2  12745  sqr2irr  12768  divides  12774  odd2np1  12828  divalglem1  12834  divalglem6  12838  divalglem10  12842  divalgb  12844  bitsval2  12857  bitsmod  12868  bitscmp  12870  smueqlem  12922  isprm2  13007  isprm3  13008  isprm4  13009  isprm5  13032  pythagtriplem19  13127  pythagtrip  13128  pceu  13140  prmreclem2  13205  4sqlem2  13237  4sqlem12  13244  vdwpc  13268  vdwnn  13286  dec5dvds2  13321  pwsle  13634  imasleval  13686  xpsfrnel  13708  xpsfrnel2  13710  xpsle  13726  isacs2  13798  mreacs  13803  iscatd2  13826  comfeq  13852  oppcsect  13919  isfunc  13981  funcoppc  13992  isffth2  14033  fucinv  14090  elhoma  14107  setcinv  14165  ispos  14324  ispos2  14325  tosso  14385  istsr2  14570  spwmo  14578  ismnd  14612  mndcl  14615  issubm  14668  gsumwspan  14711  issubg  14864  isnsg2  14890  eqger  14910  isgim2  14972  giclcl  14979  gicrcl  14980  gicsubgen  14985  gaorber  15005  resscntz  15050  cntzrec  15052  efgval2  15276  efgsfo  15291  efgrelexlemb  15302  isabl2  15340  iscyggen2  15411  iscyg2  15412  iscyg3  15416  lt6abl  15424  gsumval3eu  15433  gsum2d2  15468  dmdprdd  15480  subgdmdprd  15512  iscrng2  15599  dvdsrtr  15677  isunit  15682  isnirred  15725  isirred2  15726  isrhm  15744  isdrng2  15765  drngprop  15766  isabv  15827  issrng  15858  islmod  15874  islss  15931  lss1d  15959  islmim2  16058  lmiclcl  16062  lmicrcl  16063  lsmelval2  16077  lspsolvlem  16134  lspsncv0  16138  islpidl  16237  islpir2  16242  isnzr2  16254  isdomn2  16279  fiidomfld  16288  aspval2  16325  mplcoe1  16448  mplcoe2  16450  evlslem4  16484  xrsdsreclb  16661  unocv  16823  iunocv  16824  ishil2  16862  isobs  16863  obselocv  16871  iinopn  16891  istps4OLD  16904  istps5OLD  16905  istps  16917  istps2  16918  isbasis2g  16929  tgval2  16937  elcls  17053  neipeltop  17109  neiptopuni  17110  islpi  17128  isperf2  17131  isperf3  17132  neitr  17159  restntr  17161  ordtrest2lem  17182  cnrest  17264  ist0-3  17324  ist1-2  17326  ist1-3  17328  nrmsep3  17334  isnrm2  17337  perfcls  17344  ordthaus  17363  cmpcov2  17368  cmpsub  17378  hauscmplem  17384  cmpfi  17386  iscon2  17391  dfcon2  17396  is1stc2  17419  is2ndc  17423  1stcelcls  17438  1stccn  17440  llyi  17451  subislly  17458  iskgen3  17495  txuni2  17511  ptpjpre1  17517  ptbasin  17523  tx1cn  17555  tx2cn  17556  uptx  17571  txdis1cn  17581  ptrescn  17585  txtube  17586  txcmplem1  17587  hausdiag  17591  txkgen  17598  xkohaus  17599  xkococnlem  17605  xkoinjcn  17633  qtopeu  17662  isr0  17683  regr1lem2  17686  hmphsym  17728  elmptrab2  17774  isfbas  17775  isfbas2  17781  trfbas  17790  snfil  17810  fbunfip  17815  elfg  17817  fgcl  17824  fbasrn  17830  filuni  17831  trfil2  17833  cfinfil  17839  csdfil  17840  supfil  17841  ufinffr  17875  rnelfmlem  17898  elflim2  17910  hausflim  17927  hauspwpwf1  17933  txflf  17952  isfcls2  17959  fclsopn  17960  fclsrest  17970  alexsubALTlem2  17993  alexsubALTlem3  17994  alexsubALTlem4  17995  tmdcn2  18033  divstgplem  18064  divstgphaus  18066  tsmssubm  18086  istdrg2  18121  ustfilxp  18156  ust0  18163  fmucndlem  18235  metn0  18291  prdsxmetlem  18299  imasdsf1olem  18304  xpsdsval  18312  blres  18344  xmeterval  18345  xmeter  18346  isxms2  18361  isms2  18363  metustsym  18468  dscopn  18485  isngp3  18509  isnvc2  18598  isnghm  18621  qtopbaslem  18656  xrtgioo  18701  zcld  18708  elii1  18824  pi1cpbl  18933  tchcph  19058  cmetss  19131  bcth  19144  lssbn  19166  ishl2  19184  minveclem3b  19189  minveclem6  19195  pmltpc  19207  ovolfcl  19223  ovolgelb  19236  ovolunlem1  19253  ovoliunlem1  19258  ismbl  19282  ismbl2  19283  iundisj2  19303  dyadmax  19350  dyadmbllem  19351  vitalilem2  19361  mbfimaopnlem  19407  itg1climres  19466  itg2l  19481  itg2leub  19486  iblcnlem1  19539  ellimc2  19624  ellimc3  19626  limcmpt  19630  limcres  19633  elaa  20093  aaliou3lem9  20127  taylthlem2  20150  ulmcau  20171  pilem1  20227  sincosq1lem  20265  sineq0  20289  coseq1  20290  ellogrn  20317  logtayl2  20413  cxpcn3lem  20491  cxpcn3  20492  cubic  20549  atandm  20576  atandm2  20577  atandm4  20579  atans2  20631  xrlimcnp  20667  wilthlem2  20712  dvdsflsumcom  20833  dvdsmulf1o  20839  fsumvma  20857  logfac2  20861  dchrelbas2  20881  dchrelbas3  20882  lgsdir2lem4  20970  lgsquadlem1  20998  lgsquadlem2  20999  2sqlem1  21007  pntlem3  21163  ostth  21193  usgra2edg1  21262  usgraedg4  21265  nbgrasym  21308  nb3grapr  21321  nb3grapr2  21322  cusgra2v  21330  cusgra3v  21332  uvtx01vtx  21360  trls  21393  0wlk  21402  0trl  21403  wlkntrllem1  21406  wlkntrllem3  21408  wlkntrllem4  21409  3v3e3cycl1  21472  3v3e3cycl2  21492  vdgrun  21513  vdgrfiun  21514  eupath  21544  avril1  21598  grpoidinvlem3  21635  issubgo  21732  islno  22095  nmoubi  22114  nmobndseqi  22121  siii  22195  minvecolem5  22224  minvecolem6  22225  hvsubaddi  22409  normsub0i  22478  bcsiALT  22522  hcau  22527  hlimadd  22536  hhcmpl  22543  hhcms  22546  issh2  22552  isch2  22567  hlim0  22579  isch3  22585  norm1exi  22593  elch0  22597  hhsssh2  22611  choc0  22669  pjhtheu  22737  pjpreeq  22741  omlsilem  22745  pjoc2i  22781  chsscon1i  22805  spanuni  22887  h1deoi  22892  h1dei  22893  elspansni  22901  cmcm4i  22938  cmbr3i  22943  cmbr4i  22944  osumcor2i  22987  5oalem7  23003  3oalem3  23007  pjss2i  23023  mayete3iOLD  23072  elcnop  23201  ellnop  23202  elhmop  23217  elcnfn  23226  ellnfn  23227  cnvadj  23236  nmopub  23252  nmfnleub  23269  eleigvec  23301  nmop0  23330  nmfn0  23331  nmopun  23358  lncnopbd  23381  riesz2  23410  nmopcoadj0i  23447  rnbra  23451  pjnmopi  23492  pjssdif1i  23519  pjin2i  23537  pjin3i  23538  pjclem1  23539  cvbr2  23627  cvnbtwn3  23632  cvnbtwn4  23633  mdsl2bi  23667  mdsldmd1i  23675  elat2  23684  chrelat2i  23709  atomli  23726  chirredi  23738  mdsymlem6  23752  mdsymlem8  23754  sumdmdii  23759  dmdbr5ati  23766  cdj3i  23785  xfree2  23789  abeq2f  23797  r19.41vv  23807  mo5f  23809  nmo  23810  2reuswap2  23812  reuxfr3d  23813  rexunirn  23815  rmo3f  23819  rmo4fOLD  23820  rmo4f  23821  difeq  23835  disjorf  23858  disjorsf  23859  iundisj2f  23866  dfrel4  23870  suppss2f  23885  abfmpunirn  23899  fmptdF  23904  mptfnf  23908  fmptcof2  23911  funcnvmptOLD  23916  funcnvmpt  23917  funcnv5mpt  23918  gtiso  23922  disjdsct  23924  iundisj2fi  23984  elxrge02  24010  ofldsqr  24059  eldiftp  24182  esumnul  24232  esumpfinvalf  24255  isrnsigaOLD  24284  isrnsiga  24285  measiuns  24358  elunirnmbfm  24390  1stmbfm  24397  2ndmbfm  24398  dya2iocnrect  24418  ballotlemelo  24517  ballotlemodife  24527  ballotlem4  24528  eldmgm  24578  subfacp1lem5  24642  subfacp1lem6  24643  cvmscld  24732  cvmlift2lem12  24773  ghomgrpilem2  24869  axextprim  24922  axrepprim  24923  axunprim  24924  axpowprim  24925  axregprim  24926  axinfprim  24927  axacprim  24928  untangtr  24935  biimpexp  24945  dfid4  24955  divelunit  24957  divcnvshft  24983  divcnvlin  24984  ntrivcvgmul  25002  prodsn  25058  dftr6  25124  coep  25125  coepr  25126  dffr5  25127  dfpo2  25129  cnvco1  25134  cnvco2  25135  eldm3  25136  fundmpss  25139  dfdm5  25149  dfrn5  25150  elpotr  25154  dford5reg  25155  dfon2lem5  25160  dfon2lem6  25161  dfon2lem8  25163  dfon2lem9  25164  dfon2  25165  wfi  25224  eltrpred  25246  frind  25260  poseq  25270  soseq  25271  wfrlem4  25276  wfrlem5  25277  wfrlem9  25281  wfrlem11  25283  wfrlem12  25284  wfrlem13  25285  wfrlem14  25286  wfrlem15  25287  tfrALTlem  25293  tfr3ALT  25296  frrlem5  25302  frrlem5e  25306  frrlem11  25310  nosgnn0  25329  nodenselem5  25356  nobnddown  25372  nofulllem5  25377  elsymdif  25384  brsymdif  25389  brtxp  25437  brpprod  25442  brpprod3b  25444  brsset  25446  idsset  25447  dfon3  25449  brtxpsd  25451  brtxpsd2  25452  brbigcup  25455  elfix  25460  dffix2  25462  ellimits  25467  dffun10  25470  elfuns  25471  snelsingles  25478  dfiota3  25479  brcart  25488  brimg  25493  brapply  25494  brcup  25495  brcap  25496  brsuccf  25497  funpartlem  25498  funpartfun  25499  fullfunfnv  25502  brrestrict  25505  dfrdg4  25506  tfrqfree  25507  altopthsn  25513  altopelaltxp  25528  altxpsspw  25529  mptelee  25541  brbtwn2  25551  colinearalg  25556  ax5seg  25584  axpasch  25587  axlowdimlem6  25593  axlowdimlem13  25600  axeuclidlem  25608  axeuclid  25609  axcontlem3  25612  axcontlem4  25613  axcontlem12  25621  brcolinear2  25699  broutsideof  25762  outsideofcom  25769  fvray  25782  fvline  25785  lineunray  25788  linecom  25791  linerflx2  25792  ellines  25793  bpoly2  25810  bpoly3  25811  rankeq1o  25819  elhf  25822  elhf2  25823  supadd  25941  ovoliunnfl  25946  voliunnfl  25948  itg2addnclem2  25951  itg2addnc  25952  ecase13d  26000  trer  26003  elicc3  26004  finminlem  26005  opnrebl  26007  nn0prpw  26010  clsun  26015  fneval  26051  fnessref  26057  neibastop1  26072  neifg  26084  filnetlem4  26094  f1opr  26110  inixp  26114  sdclem2  26130  sdclem1  26131  fdc  26133  neificl  26143  istotbnd3  26164  sstotbnd3  26169  isbndx  26175  isbnd3b  26178  cntotbnd  26189  heibor1lem  26202  heibor1  26203  isdrngo2  26258  isdrngo3  26259  iscrngo2  26292  smprngopr  26346  isdmn2  26349  isfldidl2  26363  ispridlc  26364  isdmn3  26368  an43OLD  26380  prtlem70  26382  prtlem100  26388  n0el  26392  prter2  26414  funsnfsup  26427  cmpfiiin  26435  isnacs2  26444  elmzpcl  26467  diophrex  26518  2sbcrex  26527  sbcrot3  26531  sbcrot5  26532  3rexfrabdioph  26541  4rexfrabdioph  26542  6rexfrabdioph  26543  7rexfrabdioph  26544  fphpd  26561  fiphp3d  26564  rencldnfilem  26565  jm2.23  26751  expdiophlem1  26776  expdiophlem2  26777  expdioph  26778  dford4  26784  wopprc  26785  ttac  26791  fnwe2lem2  26810  islmodfg  26829  islnm2  26838  lnmlmic  26848  uvcvv0  26901  isnumbasgrplem1  26928  dfacbasgrp  26935  islinds2  26945  lmiclbs  26969  islnr2  26980  islnr3  26981  f1omvdco3  27054  issdrg2  27168  sdrgacs  27171  phisum  27180  isdomn3  27185  pm10.541  27224  pm10.542  27225  19.21vv  27236  19.36vv  27243  19.31vv  27244  19.37vv  27245  19.28vv  27246  pm11.6  27253  pm11.62  27255  pm14.12  27283  elnev  27300  evth2f  27347  elunif  27348  evthf  27359  stoweidlem31  27441  stoweidlem34  27444  stoweidlem51  27461  stoweidlem59  27469  aiffbbtat  27530  aisbbisfaisf  27531  aiffnbandciffatnotciffb  27533  abnotbtaxb  27545  mdandyvr0  27571  mdandyvr1  27572  mdandyvr2  27573  mdandyvr3  27574  mdandyvr4  27575  mdandyvr5  27576  mdandyvr6  27577  mdandyvr7  27578  rexrsb  27608  2rexsb  27609  2rexrsb  27610  cbvral2  27611  cbvrex2  27612  2ralbiim  27613  2reu5a  27616  rmoanim  27618  2rmoswap  27623  2reu1  27625  2reu3  27627  2reu4a  27628  afvpcfv0  27672  ffnaov  27725  ndmaovass  27732  ndmaovdistr  27733  frisusgranb  27743  frgra3v  27748  2pthfrgrarn  27755  2pthfrgra  27757  frgrawopreglem3  27791  frgrawopreglem4  27792  frgrawopreg  27794  frgrawopreg2  27796  gte-lteh  27808  gt-lth  27809  sgnn  27863  onfrALTlem5  27964  onfrALTlem4  27965  onfrALTlem1  27970  2uasbanh  27984  dfvd2  28005  dfvd2an  28008  dfvd3  28017  dfvd3an  28020  eelT00  28142  eelTTT  28143  eelT12  28149  uunT1  28226  uunT1p1  28227  uun132p1  28232  un2122  28236  uunTT1p1  28240  uunTT1p2  28241  uunT11p1  28243  uunT11p2  28244  uunT12  28245  uunT12p1  28246  uunT12p2  28247  uunT12p3  28248  uunT12p4  28249  uunT12p5  28250  uun2221  28259  uun2221p1  28260  uun2221p2  28261  undif3VD  28328  onfrALTlem5VD  28331  onfrALTlem4VD  28332  onfrALTlem1VD  28336  2uasbanhVD  28357  bnj170  28393  bnj248  28395  bnj251  28397  bnj256  28401  bnj258  28403  bnj291  28406  bnj422  28410  bnj432  28411  bnj23  28414  bnj89  28417  bnj132  28422  bnj156  28426  bnj158  28427  bnj538  28439  bnj563  28442  bnj945  28475  bnj946  28476  bnj976  28479  bnj1098  28485  bnj1138  28490  bnj1209  28499  bnj1476  28549  bnj1542  28559  bnj110  28560  bnj91  28563  bnj92  28564  bnj106  28570  bnj118  28571  bnj124  28573  bnj125  28574  bnj153  28582  bnj207  28583  bnj222  28585  bnj518  28588  bnj535  28592  bnj539  28593  bnj543  28595  bnj553  28600  bnj556  28602  bnj558  28604  bnj571  28608  bnj605  28609  bnj591  28613  bnj594  28614  bnj580  28615  bnj609  28619  bnj611  28620  bnj865  28625  bnj849  28627  bnj916  28635  bnj917  28636  bnj934  28637  bnj929  28638  bnj944  28640  bnj953  28641  bnj1000  28643  bnj969  28648  bnj970  28649  bnj978  28651  bnj983  28653  bnj984  28654  bnj985  28655  bnj986  28656  bnj1021  28666  bnj1033  28669  bnj1049  28674  bnj1052  28675  bnj1083  28678  bnj1112  28683  bnj1030  28687  bnj1137  28695  bnj1189  28709  bnj1204  28712  bnj1253  28717  bnj1279  28718  bnj1373  28730  bnj1388  28733  bnj1398  28734  bnj1450  28750  sborNEW7  28895  sbrimNEW7  28896  sblimNEW7  28897  sbanNEW7  28898  sbbiNEW7  28899  sbid2NEW7  28911  sbco2dwAUX7  28914  sb8ewAUX7  28920  exsbOLDNEW7  28926  sbnf2NEW7  28934  2sb5NEW7  28935  2sb6NEW7  28936  sb6aNEW7  28937  sbexNEW7  28943  sbalvNEW7  28944  sblbisNEW7  28967  sbrbisNEW7  28968  sbrbifNEW7  28969  alrot3OLD7  28991  alrot4OLD7  28992  exrot3OLD7  29005  exrot4OLD7  29006  aaanOLD7  29007  eeorOLD7  29008  pm11.53OLD7  29009  eeanOLD7  29011  cbvex4vOLD7  29047  sbco2dOLD7  29062  sb8eOLD7  29066  sbcom2OLD7  29070  2sb5rfOLD7  29071  2sb6rfOLD7  29072  2exsbOLD7  29077  equvelv  29092  a12study4  29093  a12study8  29095  a12peros  29097  a12lem2  29107  a12study10  29112  a12study10n  29113  lsateln0  29161  islshpat  29183  lcvbr2  29188  lcvbr3  29189  lcvnbtwn3  29194  islfl  29226  lshpsmreu  29275  lub0N  29355  glb0N  29359  cvrnbtwn3  29442  leat2  29460  isat3  29473  iscvlat2N  29490  ishlat2  29519  ishlat3N  29520  hlrelat5N  29566  hlrelat2  29568  3dim0  29622  2dim  29635  islpln5  29700  islvol5  29744  4atlem3  29761  dalem20  29858  ispsubsp2  29911  snatpsubN  29915  pmapglb  29935  elpadd  29964  paddasslem17  30001  dalawlem13  30048  pclfinN  30065  polval2N  30071  pclfinclN  30115  lhpex2leN  30178  isltrn2N  30285  cdleme0nex  30455  cdleme22b  30506  cdlemftr3  30730  dibopelvalN  31309  dibopelval2  31311  dibelval3  31313  diblsmopel  31337  dicelval3  31346  dihglb2  31508  doch11  31539  islpolN  31649  lcfls1N  31701  mapdval4N  31798  mapdrvallem2  31811
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