MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  bitri Structured version   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  1319  falbitru  1361  falnantru  1365  truxortru  1367  truxorfal  1368  falxorfal  1370  exp3acom23g  1380  hadass  1395  hadbi  1396  hadrot  1399  cador  1400  cadan  1401  cadnot  1403  cadcomb  1405  cadrot  1406  cad1  1407  had1  1411  alex  1581  alinexa  1588  alexn  1589  exanali  1595  19.26-2  1604  19.26-3an  1605  albiim  1621  2albiim  1622  ax12bOLD  1702  alrot3  1753  alrot4  1754  exrot3  1759  exrot4  1760  19.27  1841  19.28  1842  19.21-2  1887  nf2  1889  19.36  1892  19.37  1894  19.44  1898  19.45  1899  aaan  1906  eeor  1907  19.23vv  1915  pm11.53  1916  19.41vv  1925  19.41vvv  1926  19.41vvvv  1927  19.42vv  1930  19.42vvv  1931  4exdistr  1934  4exdistrOLD  1935  eean  1936  eeeanv  1938  cbvex4v  1996  sbrim  2136  sblim  2137  sbor  2138  sban  2139  sbbi  2141  sblbis  2144  sbrbis  2145  sbrbif  2146  sbie  2149  sbid2  2159  sbco2d  2162  sbcom  2164  sbnf2  2184  2sb5  2188  2sb6  2189  sbcom2  2190  pm11.07  2191  sb6a  2193  2sb5rf  2194  2sb6rf  2195  sbex  2205  sbalv  2206  exsbOLD  2208  2exsb  2209  eujust  2283  euf  2287  cbveu  2301  eu2  2306  mo2  2310  sbmo  2311  mo3  2312  mo4f  2313  eu4  2320  moanim  2337  2mo  2359  2mos  2360  2eu1  2361  2eu3  2363  2eu4  2364  2eu6  2366  exists1  2370  abid  2424  eleq12i  2501  abeq2  2541  abeq2i  2543  clabel  2557  abid2f  2597  sbabel  2598  neeq12i  2613  necon1abii  2655  neanior  2689  ralnex  2715  rexnal  2716  ralinexa  2750  rexanali  2751  r3al  2763  r19.26-2  2839  ralbiim  2843  r19.30  2853  ralcomf  2866  rexcomf  2867  rexrot4  2871  reean  2874  3reeanv  2876  rabbi  2886  cbvralf  2926  cbvreu  2930  cbvral2v  2940  cbvrex2v  2941  cbvral3v  2942  cbvralsv  2943  cbvrexsv  2944  sbralie  2945  rabeq2i  2953  issetf  2961  2gencl  2985  3gencl  2986  ceqsex2  2992  ceqsex3v  2994  ceqsex6v  2996  ceqsex8v  2997  gencbvex  2998  spc3gv  3041  eqvincf  3064  ceqsrex2v  3071  elrab2  3094  ralab  3095  ralrab  3096  rexab  3097  rexrab  3098  ralab2  3099  rexab2  3101  eueq3  3109  morex  3118  euxfr2  3119  euxfr  3120  euind  3121  reu2  3122  reu6  3123  rmo4  3127  reu4  3128  reu7  3129  rmoim  3133  2reuswap  3136  reuind  3137  2reu5lem1  3139  2reu5lem2  3140  2reu5  3142  sbcco  3183  sbccomlem  3231  sbccom  3232  ra5  3245  rmo3  3248  csbco  3260  sbnfc2  3309  csbabg  3310  cbvralcsf  3311  cbvreucsf  3313  dfss  3335  dfss2f  3339  ss2ab  3411  dfpss2  3432  dfpss3  3433  psseq12i  3438  sspsstri  3449  difeqri  3467  raldifb  3487  uneqri  3489  ssequn2  3520  unss  3521  rexun  3527  ralunb  3528  elin2  3531  ineqri  3534  dfss1  3545  dfss5  3546  nsspssun  3574  indifdir  3597  inrab2  3614  rabun2  3620  reuun2  3624  eq0  3642  0el  3644  abn0  3646  0pss  3665  disjr  3669  disj1  3670  disjpss  3678  undif4  3684  difin0ss  3694  inssdif0  3695  uneqdifeq  3716  r19.3rz  3719  r19.3rzv  3721  ralidm  3731  pwss  3813  dfpr2  3830  ralsns  3844  rexsns  3845  eltpg  3851  ralprg  3857  rexprg  3858  raltpg  3859  rextpg  3860  rabrsn  3874  euabsn2  3875  eusn  3880  eldifsn  3927  rexdifsn  3931  tppreqb  3939  difsnpss  3941  pwpw0  3946  ssunsn  3959  eqsn  3960  sstp  3963  tpss  3964  prel12  3975  prnebg  3979  preqsn  3980  pwsnALT  4010  pwtp  4012  eluniab  4027  elunirab  4028  unipr  4029  dfnfc2  4033  uniun  4034  uniin  4035  unissb  4045  elintab  4061  elintrab  4062  ssintab  4067  ssintrab  4073  intun  4082  intpr  4083  elrint  4091  iuncom4  4100  iuneq2  4109  dfiun2g  4123  ssiinf  4140  elriin  4163  iunxiun  4173  pwssb  4177  iunpwss  4180  dfdisj2  4184  disjor  4196  disjors  4198  disjiun  4202  disjxiun  4209  disjxun  4210  cbvopab1  4278  dftr5  4305  trint  4317  inex1  4344  inuni  4362  axpweq  4376  nfnid  4393  zfpair2  4404  moabex  4422  exss  4426  elop  4429  otth  4440  copsex4g  4445  opeqsn  4452  opthwiener  4458  opelopabsbOLD  4463  brabga  4469  opelopabaf  4478  opabn0  4485  iunopab  4486  pwunss  4488  dfid3  4499  pocl  4510  sotric  4529  isso2i  4535  somo  4537  frminex  4562  dfepfr  4567  wefrc  4576  ordtri3or  4613  ordtri2  4616  elsuci  4647  elsucg  4648  sucel  4654  on0eqel  4699  uniuni  4716  reusv2lem4  4727  reusv2lem5  4728  reusv2  4729  reusv3  4731  reuxfr2d  4746  elpwun  4756  iunpw  4759  dfwe2  4762  onintrab2  4782  ordpwsuc  4795  ordzsl  4825  dflim4  4828  tfindsg  4840  tfindes  4842  findsg  4872  elxp  4895  opelxp  4908  brxp  4909  rabxp  4914  opthprc  4925  brab2a  4927  opeliunxp  4929  xpundi  4930  xpundir  4931  elvvv  4937  brinxp  4940  brab2ga  4951  xp0r  4956  ssrel2  4966  eqrelrel  4977  reliun  4995  reluni  4997  raliunxp  5014  rexiunxp  5015  ralxpf  5019  rexxpf  5020  iunxpf  5021  relop  5023  elcnv  5049  elcnv2  5050  dmin  5077  dmuni  5079  dmopab  5080  dmi  5084  rnopab  5115  elrnmpt1  5119  rncoeq  5139  resiexg  5188  dfima2  5205  dfima3  5206  elima2  5209  elima3  5210  imai  5218  elimasn  5229  epini  5234  dfse2  5237  cotr  5246  issref  5247  intasym  5249  asymref  5250  asymref2  5251  somin1  5270  cnvopab  5274  cnvi  5276  cnvdif  5278  imainss  5287  dfrel2  5321  dfrel3  5328  rnsnn0  5336  relsn2  5340  dmsnopg  5341  cnvcnvsn  5347  elxp4  5357  elxp5  5358  cnvresima  5359  mptpreima  5363  dfco2  5369  coundi  5371  coundir  5372  imaco  5375  coiun  5379  coi1  5385  relssdmrn  5390  relrelss  5393  ressn  5408  cnviin  5409  cnvpo  5410  cbviota  5423  dffun2  5464  dffun3  5465  dffun4  5466  dffun5  5467  dffun7  5479  dffun8  5480  dffun9  5481  funopab  5486  funun  5495  funcnvsn  5496  fntpg  5506  funcnv2  5510  funcnv  5511  fun2cnv  5513  fncnv  5515  fun11  5516  fununi  5517  imadif  5528  funimaexg  5530  fnunsn  5552  fnres  5561  fnopabg  5568  mptfng  5570  mptun  5575  fun  5607  fresaunres1  5616  fcnvres  5620  dff12  5638  f1cnvcnv  5647  funforn  5660  dff1o2  5679  dff1o5  5683  f1orn  5684  resdif  5696  ffoss  5707  f11o  5708  f1o00  5710  fo00  5711  elfv  5726  fv3  5744  dffn5f  5781  dffv2  5796  eqfnfv3  5829  fndmdifeq0  5836  fneqeql  5838  unpreima  5856  respreima  5859  dff4  5883  dffo3  5884  dffo5  5886  f1ompt  5891  ffnfvf  5895  fmptco  5901  fsn2  5908  ftpg  5916  fconst3  5955  fconst4  5956  idref  5979  abrexco  5986  opabex3d  5989  opabex3  5990  abexssex  6002  dff13  6004  dff13f  6006  foeqcnvco  6027  isocnv3  6052  isoini  6058  weniso  6075  oprabid  6105  dfoprab2  6121  eqoprab2b  6132  dmoprab  6154  rnoprab  6156  eloprabga  6160  mpt2mptx  6164  resoprab  6166  ffnov  6174  fnov  6178  elrnmpt2  6183  ralrnmpt2  6184  rexrnmpt2  6185  oprabex3  6188  oprabrexex2  6189  ovid  6190  ov3  6210  ov6g  6211  foov  6220  ndmovdistr  6236  difxp  6380  elopaba  6409  fmpt2  6418  curry1  6438  curry2  6441  fsplit  6451  frxp  6456  xporderlem  6457  soxp  6459  mpt2xopovel  6471  brtpos2  6485  dmtpos  6491  tpostpos  6499  tpossym  6511  tposoprab  6515  sorpsscmpl  6533  opiota  6535  eusvobj2  6582  dfsmo2  6609  tfrlem3  6638  tfrlem7  6644  tfrlem9  6646  tfrlem9a  6647  tz7.48lem  6698  tz7.49c  6703  el1o  6743  dif1o  6744  ondif2  6746  brwitnlem  6751  oarec  6805  omeulem1  6825  omeu  6828  oeordi  6830  oeeui  6845  oeeu  6846  omopthlem1  6898  dfer2  6906  brdifun  6932  swoso  6936  eqerlem  6937  qsid  6970  iiner  6976  erinxp  6978  brecop  6997  eroveu  6999  erovlem  7000  ecopovsym  7006  mapval2  7043  mapsn  7055  elixp  7069  ixpeq2  7076  ixpin  7087  ixpiin  7088  mptelixpg  7099  ixpsnf1o  7102  boxriin  7104  domen  7121  isfi  7131  en1  7174  xpsnen  7192  xpcomco  7198  xpassen  7202  sbthlem9  7225  0sdomg  7236  2pwuninel  7262  ssenen  7281  nneneq  7290  php  7291  modom2  7310  ac6sfi  7351  frfi  7352  fimaxg  7354  elfpw  7408  fissuni  7411  dffi3  7436  marypha1lem  7438  marypha2lem2  7441  dfsup2  7447  dfsup2OLD  7448  wofib  7514  wemapso2lem  7519  wdom2d  7548  unxpwdom2  7556  dford2  7575  inf2  7578  inf3lem2  7584  axinf2  7595  zfinf2  7597  cantnfp1lem2  7635  oemapso  7638  cantnflem1  7645  trcl  7664  epfrs  7667  rankvalb  7723  r1elss  7732  unbndrank  7768  scott0s  7812  cplem1  7813  bnd2  7817  isnum2  7832  iscard2  7863  infxpenlem  7895  fseqenlem1  7905  acnnum  7933  infpwfien  7943  alephnbtwn2  7953  alephord2  7957  alephislim  7964  cardaleph  7970  alephval3  7991  aceq1  7998  aceq2  8000  dfac3  8002  dfac4  8003  dfac5lem1  8004  dfac5lem2  8005  dfac5lem3  8006  dfac5lem4  8007  dfac5lem5  8008  dfac2  8011  dfac0  8013  dfac1  8014  dfac8  8015  dfac9  8016  dfac12  8029  kmlem3  8032  kmlem4  8033  kmlem7  8036  kmlem8  8037  kmlem9  8038  kmlem13  8042  kmlem14  8043  kmlem15  8044  dfackm  8046  pwsdompw  8084  ackbij2lem2  8120  cf0  8131  cfval2  8140  cflim2  8143  cfss  8145  cfslb  8146  isfin3  8176  isfin5  8179  isfin6  8180  sdom2en01  8182  fin23lem25  8204  fin23lem26  8205  fin23lem40  8231  isfin1-2  8265  isfin1-3  8266  fin1a2lem5  8284  fin1a2lem6  8285  fin1a2lem12  8291  fin12  8293  domtriomlem  8322  axdc2lem  8328  axdc3lem2  8331  axdc3lem4  8333  axcclem  8337  ac6num  8359  ac6n  8365  zorn2lem6  8381  zornn0g  8385  ttukeylem6  8394  ttukey2g  8396  brdom7disj  8409  brdom6disj  8410  iunfo  8414  iundom2g  8415  konigthlem  8443  alephsuc3  8455  elgch  8497  fpwwe2lem9  8513  fpwwe2lem12  8516  fpwwe2lem13  8517  fpwwe2  8518  canth4  8522  canthwe  8526  wunex2  8613  uniwun  8615  axgroth5  8699  grothpw  8701  axgroth6  8703  grothprimlem  8708  grothprim  8709  elni  8753  ltexpi  8779  nqerf  8807  nqerid  8810  ordpipq  8819  recmulnq  8841  npomex  8873  genpnnp  8882  genpass  8886  addcompr  8898  mulcompr  8900  reclem2pr  8925  reclem3pr  8926  ltsosr  8969  ltasr  8975  mappsrpr  8983  map2psrpr  8985  opelcn  9004  elreal  9006  elreal2  9007  axaddf  9020  axmulf  9021  axicn  9025  axrrecex  9038  axpre-mulgt0  9043  xrlenlt  9143  ssxr  9145  leloe  9161  msq0i  9669  infm3  9967  supmullem2  9975  inelr  9990  arch  10218  elnnne0  10235  un0addcl  10253  un0mulcl  10254  nn0n0n1ge2b  10281  elnnz  10292  elznn0nn  10295  elznn0  10296  elznn  10297  elz2  10298  raluz2  10526  rexuz2  10528  nnwos  10544  eluz2b2  10548  eluz2b3  10549  ublbneg  10560  zmin  10570  elq  10576  ralrp  10630  rexrp  10631  ltxr  10715  xrnemnf  10718  xrleloe  10737  xrltlen  10739  xrrebnd  10756  xaddf  10810  xmullem  10843  xmullem2  10844  xrsupss  10887  xrinfmss  10888  elfzp1  11097  fzprval  11106  fztpval  11107  4fvwrd4  11121  fzm1  11127  fzolb  11145  fzolb2  11146  elfzo3  11155  fzouzsplit  11168  fzo0n0  11174  fzind2  11198  uzrdgfni  11298  subsq0i  11494  crreczi  11504  nn0le2msqi  11560  nn0opth2i  11564  hashkf  11620  hashinfxadd  11659  hashgt12el  11682  hashgt12el2  11683  hashtpg  11691  hashfun  11700  hashbclem  11701  hashbc  11702  hashf1lem2  11705  leiso  11708  iswrd  11729  f1oun2prg  11864  climeu  12349  lo1resb  12358  rlimresb  12359  o1resb  12360  climmpt2  12367  fsum2dlem  12554  rpnnen2  12825  sqr2irr  12848  divides  12854  odd2np1  12908  divalglem1  12914  divalglem6  12918  divalglem10  12922  divalgb  12924  bitsval2  12937  bitsmod  12948  bitscmp  12950  smueqlem  13002  isprm2  13087  isprm3  13088  isprm4  13089  isprm5  13112  pythagtriplem19  13207  pythagtrip  13208  pceu  13220  prmreclem2  13285  4sqlem2  13317  4sqlem12  13324  vdwpc  13348  vdwnn  13366  dec5dvds2  13401  pwsle  13714  imasleval  13766  xpsfrnel  13788  xpsfrnel2  13790  xpsle  13806  isacs2  13878  mreacs  13883  iscatd2  13906  comfeq  13932  oppcsect  13999  isfunc  14061  funcoppc  14072  isffth2  14113  fucinv  14170  elhoma  14187  setcinv  14245  ispos  14404  ispos2  14405  tosso  14465  istsr2  14650  spwmo  14658  ismnd  14692  mndcl  14695  issubm  14748  gsumwspan  14791  issubg  14944  isnsg2  14970  eqger  14990  isgim2  15052  giclcl  15059  gicrcl  15060  gicsubgen  15065  gaorber  15085  resscntz  15130  cntzrec  15132  efgval2  15356  efgsfo  15371  efgrelexlemb  15382  isabl2  15420  iscyggen2  15491  iscyg2  15492  iscyg3  15496  lt6abl  15504  gsumval3eu  15513  gsum2d2  15548  dmdprdd  15560  subgdmdprd  15592  iscrng2  15679  dvdsrtr  15757  isunit  15762  isnirred  15805  isirred2  15806  isrhm  15824  isdrng2  15845  drngprop  15846  isabv  15907  issrng  15938  islmod  15954  islss  16011  lss1d  16039  islmim2  16138  lmiclcl  16142  lmicrcl  16143  lsmelval2  16157  lspsolvlem  16214  islpidl  16317  islpir2  16322  isnzr2  16334  isdomn2  16359  fiidomfld  16368  aspval2  16405  mplcoe1  16528  mplcoe2  16530  evlslem4  16564  xrsdsreclb  16745  unocv  16907  iunocv  16908  ishil2  16946  isobs  16947  obselocv  16955  iinopn  16975  istps4OLD  16988  istps5OLD  16989  istps  17001  istps2  17002  isbasis2g  17013  tgval2  17021  elcls  17137  neipeltop  17193  neiptopuni  17194  islpi  17213  isperf2  17216  isperf3  17217  neitr  17244  restntr  17246  ordtrest2lem  17267  cnrest  17349  ist0-3  17409  ist1-2  17411  ist1-3  17413  nrmsep3  17419  isnrm2  17422  perfcls  17429  ordthaus  17448  cmpcov2  17453  cmpsub  17463  hauscmplem  17469  cmpfi  17471  iscon2  17477  dfcon2  17482  is1stc2  17505  is2ndc  17509  1stcelcls  17524  1stccn  17526  llyi  17537  subislly  17544  iskgen3  17581  txuni2  17597  ptpjpre1  17603  ptbasin  17609  tx1cn  17641  tx2cn  17642  uptx  17657  txdis1cn  17667  ptrescn  17671  txtube  17672  txcmplem1  17673  hausdiag  17677  txkgen  17684  xkohaus  17685  xkococnlem  17691  xkoinjcn  17719  qtopeu  17748  isr0  17769  regr1lem2  17772  hmphsym  17814  elmptrab2  17860  isfbas  17861  isfbas2  17867  trfbas  17876  snfil  17896  fbunfip  17901  elfg  17903  fgcl  17910  fbasrn  17916  filuni  17917  cfinfil  17925  csdfil  17926  supfil  17927  ufinffr  17961  rnelfmlem  17984  elflim2  17996  hausflim  18013  hauspwpwf1  18019  txflf  18038  isfcls2  18045  fclsopn  18046  fclsrest  18056  alexsubALTlem2  18079  alexsubALTlem3  18080  alexsubALTlem4  18081  tmdcn2  18119  divstgplem  18150  divstgphaus  18152  tsmssubm  18172  istdrg2  18207  ustfilxp  18242  ust0  18249  fmucndlem  18321  metn0  18390  prdsxmetlem  18398  imasdsf1olem  18403  xpsdsval  18411  blres  18461  xmeterval  18462  xmeter  18463  isxms2  18478  isms2  18480  metustsymOLD  18591  metustsym  18592  dscopn  18621  isngp3  18645  isnvc2  18734  isnghm  18757  qtopbaslem  18792  xrtgioo  18837  zcld  18844  elii1  18960  pi1cpbl  19069  tchcph  19194  cmetss  19267  bcth  19282  lssbn  19304  ishl2  19324  minveclem3b  19329  minveclem6  19335  pmltpc  19347  ovolfcl  19363  ovolgelb  19376  ovolunlem1  19393  ovoliunlem1  19398  ismbl  19422  ismbl2  19423  dyadmax  19490  dyadmbllem  19491  vitalilem2  19501  mbfimaopnlem  19547  itg1climres  19606  itg2l  19621  itg2leub  19626  iblcnlem1  19679  ellimc2  19764  ellimc3  19766  limcmpt  19770  limcres  19773  elaa  20233  aaliou3lem9  20267  taylthlem2  20290  ulmcau  20311  pilem1  20367  sincosq1lem  20405  sineq0  20429  coseq1  20430  ellogrn  20457  logtayl2  20553  cxpcn3lem  20631  cxpcn3  20632  cubic  20689  atandm  20716  atandm2  20717  atandm4  20719  atans2  20771  xrlimcnp  20807  wilthlem2  20852  dvdsflsumcom  20973  dvdsmulf1o  20979  fsumvma  20997  logfac2  21001  dchrelbas2  21021  dchrelbas3  21022  lgsdir2lem4  21110  lgsquadlem1  21138  lgsquadlem2  21139  2sqlem1  21147  pntlem3  21303  ostth  21333  usgra2edg1  21403  usgraedg4  21406  nbgrasym  21449  nb3grapr  21462  nb3grapr2  21463  cusgra2v  21471  cusgra3v  21473  uvtx01vtx  21501  trls  21536  0wlk  21545  0trl  21546  wlkntrllem1  21559  wlkntrllem2  21560  is2wlk  21565  3v3e3cycl1  21631  3v3e3cycl2  21651  vdgrun  21672  vdgrfiun  21673  eupath  21703  avril1  21757  grpoidinvlem3  21794  issubgo  21891  islno  22254  nmoubi  22273  nmobndseqi  22280  siii  22354  minvecolem5  22383  minvecolem6  22384  hvsubaddi  22568  normsub0i  22637  bcsiALT  22681  hcau  22686  hlimadd  22695  hhcmpl  22702  hhcms  22705  issh2  22711  isch2  22726  hlim0  22738  isch3  22744  norm1exi  22752  elch0  22756  hhsssh2  22770  choc0  22828  pjhtheu  22896  pjpreeq  22900  omlsilem  22904  pjoc2i  22940  chsscon1i  22964  spanuni  23046  h1deoi  23051  h1dei  23052  elspansni  23060  cmcm4i  23097  cmbr3i  23102  cmbr4i  23103  osumcor2i  23146  5oalem7  23162  3oalem3  23166  pjss2i  23182  mayete3iOLD  23231  elcnop  23360  ellnop  23361  elhmop  23376  elcnfn  23385  ellnfn  23386  cnvadj  23395  nmopub  23411  nmfnleub  23428  eleigvec  23460  nmop0  23489  nmfn0  23490  nmopun  23517  lncnopbd  23540  riesz2  23569  nmopcoadj0i  23606  rnbra  23610  pjnmopi  23651  pjssdif1i  23678  pjin2i  23696  pjin3i  23697  pjclem1  23698  cvbr2  23786  cvnbtwn3  23791  cvnbtwn4  23792  mdsl2bi  23826  mdsldmd1i  23834  elat2  23843  chrelat2i  23868  atomli  23885  chirredi  23897  mdsymlem6  23911  mdsymlem8  23913  sumdmdii  23918  dmdbr5ati  23925  cdj3i  23944  xfree2  23948  abeq2f  23960  r19.41vv  23970  mo5f  23972  nmo  23973  2reuswap2  23975  reuxfr3d  23976  rexunirn  23978  rmo3f  23982  rmo4fOLD  23983  rmo4f  23984  difeq  23998  disjorf  24021  disjorsf  24022  iundisj2f  24030  dfrel4  24034  suppss2f  24049  abfmpunirn  24064  fmptdF  24069  mptfnf  24073  fmptcof2  24076  ofpreima  24081  funcnvmptOLD  24082  funcnvmpt  24083  funcnv5mpt  24084  gtiso  24088  disjdsct  24090  iundisj2fi  24153  elxrge02  24178  toslub  24191  tosglb  24192  ofldsqr  24240  isarchi  24252  eldiftp  24393  esumnul  24443  esumpfinvalf  24466  isrnsigaOLD  24495  isrnsiga  24496  measiuns  24571  elunirnmbfm  24603  1stmbfm  24610  2ndmbfm  24611  dya2iocnrect  24631  sibfof  24654  ballotlemelo  24745  ballotlemodife  24755  ballotlem4  24756  eldmgm  24806  subfacp1lem5  24870  subfacp1lem6  24871  cvmscld  24960  cvmlift2lem12  25001  ghomgrpilem2  25097  axextprim  25150  axrepprim  25151  axunprim  25152  axpowprim  25153  axregprim  25154  axinfprim  25155  axacprim  25156  untangtr  25163  biimpexp  25173  dfid4  25183  divelunit  25185  divcnvshft  25211  divcnvlin  25212  ntrivcvgmul  25230  prodsn  25286  fprod2dlem  25304  dftr6  25373  coep  25374  coepr  25375  dffr5  25376  dfpo2  25378  cnvco1  25383  cnvco2  25384  eldm3  25385  pocnv  25387  socnv  25388  fundmpss  25390  dfdm5  25400  dfrn5  25401  snnzb  25402  elpotr  25408  dford5reg  25409  dfon2lem5  25414  dfon2lem6  25415  dfon2lem8  25417  dfon2lem9  25418  dfon2  25419  wfi  25482  eltrpred  25504  frind  25518  poseq  25528  soseq  25529  wfrlem4  25541  wfrlem5  25542  wfrlem9  25546  wfrlem11  25548  wfrlem12  25549  wfrlem13  25550  wfrlem14  25551  wfrlem15  25552  frrlem5  25586  frrlem5e  25590  frrlem11  25594  nosgnn0  25613  nodenselem5  25640  nobnddown  25656  nofulllem5  25661  elsymdif  25668  brsymdif  25673  brtxp  25725  brpprod  25730  brpprod3b  25732  brsset  25734  idsset  25735  dfon3  25737  brtxpsd  25739  brtxpsd2  25740  brbigcup  25743  elfix  25748  ellimits  25755  sscoid  25758  dffun10  25759  elfuns  25760  snelsingles  25767  dfiota3  25768  brcart  25777  brimg  25782  brapply  25783  brcup  25784  brcap  25785  brsuccf  25786  funpartlem  25787  funpartfun  25788  fullfunfnv  25791  brrestrict  25794  dfrdg4  25795  tfrqfree  25796  imagesset  25798  brub  25799  altopthsn  25806  altopelaltxp  25821  altxpsspw  25822  mptelee  25834  brbtwn2  25844  colinearalg  25849  ax5seg  25877  axpasch  25880  axlowdimlem6  25886  axlowdimlem13  25893  axeuclidlem  25901  axeuclid  25902  axcontlem3  25905  axcontlem4  25906  axcontlem12  25914  brcolinear2  25992  broutsideof  26055  outsideofcom  26062  fvray  26075  fvline  26078  lineunray  26081  linecom  26084  linerflx2  26085  ellines  26086  bpoly2  26103  bpoly3  26104  rankeq1o  26112  elhf  26115  elhf2  26116  wl-exeq  26234  supadd  26238  mblfinlem1  26243  mblfinlem2  26244  ovoliunnfl  26248  voliunnfl  26250  mbfposadd  26254  cnambfre  26255  itg2addnclem2  26257  itg2addnclem3  26258  itg2addnc  26259  ftc1anclem1  26280  ftc1anclem3  26282  ftc1anc  26288  ecase13d  26316  trer  26319  elicc3  26320  finminlem  26321  opnrebl  26323  nn0prpw  26326  clsun  26331  fneval  26367  fnessref  26373  neibastop1  26388  neifg  26400  filnetlem4  26410  f1opr  26426  inixp  26430  sdclem2  26446  sdclem1  26447  fdc  26449  neificl  26459  istotbnd3  26480  sstotbnd3  26485  isbndx  26491  isbnd3b  26494  cntotbnd  26505  heibor1lem  26518  heibor1  26519  isdrngo2  26574  isdrngo3  26575  iscrngo2  26608  smprngopr  26662  isdmn2  26665  isfldidl2  26679  ispridlc  26680  isdmn3  26684  an43OLD  26696  prtlem70  26698  prtlem100  26704  n0el  26708  prter2  26730  funsnfsup  26743  cmpfiiin  26751  isnacs2  26760  elmzpcl  26783  diophrex  26834  2sbcrex  26843  sbcrot3  26847  sbcrot5  26848  3rexfrabdioph  26857  4rexfrabdioph  26858  6rexfrabdioph  26859  7rexfrabdioph  26860  fphpd  26877  fiphp3d  26880  rencldnfilem  26881  jm2.23  27067  expdiophlem1  27092  expdiophlem2  27093  expdioph  27094  dford4  27100  wopprc  27101  ttac  27107  fnwe2lem2  27126  islmodfg  27144  islnm2  27153  lnmlmic  27163  uvcvv0  27216  isnumbasgrplem1  27243  dfacbasgrp  27250  islinds2  27260  lmiclbs  27284  islnr2  27295  islnr3  27296  f1omvdco3  27369  issdrg2  27483  sdrgacs  27486  phisum  27495  isdomn3  27500  pm10.541  27539  pm10.542  27540  19.21vv  27551  19.36vv  27558  19.31vv  27559  19.37vv  27560  19.28vv  27561  pm11.6  27568  pm11.62  27570  pm14.12  27598  elnev  27615  evth2f  27662  elunif  27663  evthf  27674  stoweidlem31  27756  stoweidlem34  27759  stoweidlem51  27776  stoweidlem59  27784  aiffbbtat  27845  aisbbisfaisf  27846  aiffnbandciffatnotciffb  27848  abnotbtaxb  27860  mdandyvr0  27886  mdandyvr1  27887  mdandyvr2  27888  mdandyvr3  27889  mdandyvr4  27890  mdandyvr5  27891  mdandyvr6  27892  mdandyvr7  27893  rexrsb  27923  2rexsb  27924  2rexrsb  27925  cbvral2  27926  cbvrex2  27927  2ralbiim  27928  2reu5a  27931  rmoanim  27933  2rmoswap  27938  2reu1  27940  2reu3  27942  2reu4a  27943  afvpcfv0  27986  ffnaov  28039  ndmaovass  28046  ndmaovdistr  28047  3an4anass  28049  raldifsnb  28058  rexdifpr  28059  dff14a  28078  dff14b  28079  f13dfv  28081  oprabv  28085  elfz2z  28105  2ffzoeq  28140  swrdnd  28182  swrdvalodmlem1  28187  cshwssizelem2  28281  cshwssizelem3  28282  usgra2pthspth  28305  usgra2pthlem1  28310  el2wlkonotot0  28339  usg2spthonot0  28356  isrusgra  28370  frisusgranb  28387  frgra3v  28392  2pthfrgrarn  28399  2pthfrgra  28401  frgrawopreglem3  28435  frgrawopreglem4  28436  frgrawopreg  28438  frgrawopreg2  28440  usg2spot2nb  28454  usgreg2spot  28456  gte-lteh  28469  gt-lth  28470  sgnn  28524  onfrALTlem5  28628  onfrALTlem4  28629  onfrALTlem1  28634  2uasbanh  28648  dfvd2  28671  dfvd2an  28674  dfvd3  28683  dfvd3an  28686  eelT00  28808  eelTTT  28809  eelT12  28815  uunT1  28892  uunT1p1  28893  uun132p1  28898  un2122  28902  uunTT1p1  28906  uunTT1p2  28907  uunT11p1  28909  uunT11p2  28910  uunT12  28911  uunT12p1  28912  uunT12p2  28913  uunT12p3  28914  uunT12p4  28915  uunT12p5  28916  uun2221  28925  uun2221p1  28926  uun2221p2  28927  undif3VD  28994  onfrALTlem5VD  28997  onfrALTlem4VD  28998  onfrALTlem1VD  29002  2uasbanhVD  29023  bnj170  29062  bnj248  29064  bnj251  29066  bnj256  29070  bnj258  29072  bnj291  29075  bnj422  29079  bnj432  29080  bnj23  29083  bnj89  29086  bnj132  29091  bnj156  29095  bnj158  29096  bnj538  29108  bnj563  29111  bnj945  29144  bnj946  29145  bnj976  29148  bnj1098  29154  bnj1138  29159  bnj1209  29168  bnj1476  29218  bnj1542  29228  bnj110  29229  bnj91  29232  bnj92  29233  bnj106  29239  bnj118  29240  bnj124  29242  bnj125  29243  bnj153  29251  bnj207  29252  bnj222  29254  bnj518  29257  bnj535  29261  bnj539  29262  bnj543  29264  bnj553  29269  bnj556  29271  bnj558  29273  bnj571  29277  bnj605  29278  bnj591  29282  bnj594  29283  bnj580  29284  bnj609  29288  bnj611  29289  bnj865  29294  bnj849  29296  bnj916  29304  bnj917  29305  bnj934  29306  bnj929  29307  bnj944  29309  bnj953  29310  bnj1000  29312  bnj969  29317  bnj970  29318  bnj978  29320  bnj983  29322  bnj984  29323  bnj985  29324  bnj986  29325  bnj1021  29335  bnj1033  29338  bnj1049  29343  bnj1052  29344  bnj1083  29347  bnj1112  29352  bnj1030  29356  bnj1137  29364  bnj1189  29378  bnj1204  29381  bnj1253  29386  bnj1279  29387  bnj1373  29399  bnj1388  29402  bnj1398  29403  bnj1450  29419  sborNEW7  29566  sbrimNEW7  29567  sblimNEW7  29568  sbanNEW7  29569  sbbiNEW7  29570  sbid2NEW7  29583  sbco2dwAUX7  29586  sb8ewAUX7  29594  exsbOLDNEW7  29600  sbnf2NEW7  29608  2sb5NEW7  29609  2sb6NEW7  29610  sb6aNEW7  29611  sbexNEW7  29617  sbalvNEW7  29618  sblbisNEW7  29641  sbrbisNEW7  29642  sbrbifNEW7  29643  sbcom2NEW7  29644  ax7w15lemxAUX7  29666  ax7w15AUX7  29668  ax7w14lemAUX7  29669  ax7w14AUX7  29670  elsb34AUX7  29672  ax7w17lem1AUX7  29675  alrot3OLD7  29682  alrot4OLD7  29683  exrot3OLD7  29696  exrot4OLD7  29697  aaanOLD7  29698  eeorOLD7  29699  pm11.53OLD7  29700  eeanOLD7  29702  cbvex4vOLD7  29738  sbco2dOLD7  29753  sb8eOLD7  29757  2sb5rfOLD7  29761  2sb6rfOLD7  29762  2exsbOLD7  29767  lsateln0  29793  islshpat  29815  lcvbr2  29820  lcvbr3  29821  lcvnbtwn3  29826  islfl  29858  lshpsmreu  29907  lub0N  29987  glb0N  29991  cvrnbtwn3  30074  leat2  30092  isat3  30105  iscvlat2N  30122  ishlat2  30151  ishlat3N  30152  hlrelat5N  30198  hlrelat2  30200  3dim0  30254  2dim  30267  islpln5  30332  islvol5  30376  4atlem3  30393  dalem20  30490  ispsubsp2  30543  snatpsubN  30547  pmapglb  30567  elpadd  30596  paddasslem17  30633  dalawlem13  30680  pclfinN  30697  polval2N  30703  pclfinclN  30747  lhpex2leN  30810  isltrn2N  30917  cdleme0nex  31087  cdleme22b  31138  cdlemftr3  31362  dibopelvalN  31941  dibopelval2  31943  dibelval3  31945  diblsmopel  31969  dicelval3  31978  dihglb2  32140  doch11  32171  islpolN  32281  lcfls1N  32333  mapdval4N  32430  mapdrvallem2  32443
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