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  2066  sbor  2119  sbrim  2120  sblim  2121  sban  2122  sbbi  2124  sblbis  2125  sbrbis  2126  sbrbif  2127  sbid2  2137  sbco2d  2140  sbnf2  2161  2sb5  2165  2sb6  2166  sbcom2  2167  pm11.07  2168  sb6a  2170  2sb5rf  2171  2sb6rf  2172  sbex  2182  sbalv  2183  exsbOLD  2185  2exsb  2186  eujust  2260  euf  2264  cbveu  2278  eu2  2283  mo2  2287  sbmo  2288  mo3  2289  mo4f  2290  eu4  2297  moanim  2314  2mo  2336  2mos  2337  2eu1  2338  2eu3  2340  2eu4  2341  2eu6  2343  exists1  2347  abid  2396  eleq12i  2473  abeq2  2513  abeq2i  2515  clabel  2529  abid2f  2569  sbabel  2570  neeq12i  2583  necon1abii  2622  neanior  2656  ralnex  2680  rexnal  2681  ralinexa  2715  rexanali  2716  r3al  2727  r19.26-2  2803  ralbiim  2807  r19.30  2817  ralcomf  2830  rexcomf  2831  rexrot4  2835  reean  2838  3reeanv  2840  rabbi  2850  cbvralf  2890  cbvreu  2894  cbvral2v  2904  cbvrex2v  2905  cbvral3v  2906  cbvralsv  2907  cbvrexsv  2908  sbralie  2909  rabeq2i  2917  issetf  2925  2gencl  2949  3gencl  2950  ceqsex2  2956  ceqsex3v  2958  ceqsex6v  2960  ceqsex8v  2961  gencbvex  2962  spc3gv  3005  eqvincf  3028  ceqsrex2v  3035  elrab2  3058  ralab  3059  ralrab  3060  rexab  3061  rexrab  3062  ralab2  3063  rexab2  3065  eueq3  3073  morex  3082  euxfr2  3083  euxfr  3084  euind  3085  reu2  3086  reu6  3087  rmo4  3091  reu4  3092  reu7  3093  rmoim  3097  2reuswap  3100  reuind  3101  2reu5lem1  3103  2reu5lem2  3104  2reu5  3106  sbcco  3147  sbccomlem  3195  sbccom  3196  ra5  3209  rmo3  3212  csbco  3224  sbnfc2  3273  csbabg  3274  cbvralcsf  3275  cbvreucsf  3277  dfss  3299  dfss2f  3303  ss2ab  3375  dfpss2  3396  dfpss3  3397  psseq12i  3402  sspsstri  3413  difeqri  3431  raldifb  3451  uneqri  3453  ssequn2  3484  unss  3485  rexun  3491  ralunb  3492  elin2  3495  ineqri  3498  dfss1  3509  dfss5  3510  nsspssun  3538  indifdir  3561  inrab2  3578  rabun2  3584  reuun2  3588  eq0  3606  0el  3608  abn0  3610  0pss  3629  disjr  3633  disj1  3634  disjpss  3642  undif4  3648  difin0ss  3658  inssdif0  3659  uneqdifeq  3680  r19.3rz  3683  r19.3rzv  3685  ralidm  3695  pwss  3777  dfpr2  3794  ralsns  3808  rexsns  3809  eltpg  3815  ralprg  3821  rexprg  3822  raltpg  3823  rextpg  3824  rabrsn  3838  euabsn2  3839  eusn  3844  eldifsn  3891  rexdifsn  3895  tppreqb  3903  difsnpss  3905  pwpw0  3910  ssunsn  3923  eqsn  3924  sstp  3927  tpss  3928  prel12  3939  prnebg  3943  preqsn  3944  pwsnALT  3974  pwtp  3976  eluniab  3991  elunirab  3992  unipr  3993  dfnfc2  3997  uniun  3998  uniin  3999  unissb  4009  elintab  4025  elintrab  4026  ssintab  4031  ssintrab  4037  intun  4046  intpr  4047  elrint  4055  iuncom4  4064  iuneq2  4073  dfiun2g  4087  ssiinf  4104  elriin  4127  iunxiun  4137  pwssb  4141  iunpwss  4144  dfdisj2  4148  disjor  4160  disjors  4162  disjiun  4166  disjxiun  4173  disjxun  4174  cbvopab1  4242  dftr5  4269  trint  4281  inex1  4308  inuni  4326  axpweq  4340  nfnid  4357  zfpair2  4368  moabex  4386  exss  4390  elop  4393  otth  4404  copsex4g  4409  opeqsn  4416  opthwiener  4422  opelopabsbOLD  4427  brabga  4433  opelopabaf  4442  opabn0  4449  iunopab  4450  pwunss  4452  dfid3  4463  pocl  4474  sotric  4493  isso2i  4499  somo  4501  frminex  4526  dfepfr  4531  wefrc  4540  ordtri3or  4577  ordtri2  4580  elsuci  4611  elsucg  4612  sucel  4618  on0eqel  4662  uniuni  4679  reusv2lem4  4690  reusv2lem5  4691  reusv2  4692  reusv3  4694  reuxfr2d  4709  elpwun  4719  iunpw  4722  dfwe2  4725  onintrab2  4745  ordpwsuc  4758  ordzsl  4788  dflim4  4791  tfindsg  4803  tfindes  4805  findsg  4835  elxp  4858  opelxp  4871  brxp  4872  rabxp  4877  opthprc  4888  brab2a  4890  opeliunxp  4892  xpundi  4893  xpundir  4894  elvvv  4900  brinxp  4903  brab2ga  4914  xp0r  4919  ssrel2  4929  eqrelrel  4940  reliun  4958  reluni  4960  raliunxp  4977  rexiunxp  4978  ralxpf  4982  rexxpf  4983  iunxpf  4984  relop  4986  elcnv  5012  elcnv2  5013  dmin  5040  dmuni  5042  dmopab  5043  dmi  5047  rnopab  5078  elrnmpt1  5082  rncoeq  5102  resiexg  5151  dfima2  5168  dfima3  5169  elima2  5172  elima3  5173  imai  5181  elimasn  5192  epini  5197  dfse2  5200  cotr  5209  issref  5210  intasym  5212  asymref  5213  asymref2  5214  somin1  5233  cnvopab  5237  cnvi  5239  cnvdif  5241  imainss  5250  dfrel2  5284  dfrel3  5291  rnsnn0  5299  relsn2  5303  dmsnopg  5304  cnvcnvsn  5310  elxp4  5320  elxp5  5321  cnvresima  5322  mptpreima  5326  dfco2  5332  coundi  5334  coundir  5335  imaco  5338  coiun  5342  coi1  5348  relssdmrn  5353  relrelss  5356  ressn  5371  cnviin  5372  cnvpo  5373  cbviota  5386  dffun2  5427  dffun3  5428  dffun4  5429  dffun5  5430  dffun7  5442  dffun8  5443  dffun9  5444  funopab  5449  funun  5458  funcnvsn  5459  fntpg  5469  funcnv2  5473  funcnv  5474  fun2cnv  5476  fncnv  5478  fun11  5479  fununi  5480  imadif  5491  funimaexg  5493  fnunsn  5515  fnres  5524  fnopabg  5531  mptfng  5533  mptun  5538  fun  5570  fresaunres1  5579  fcnvres  5583  dff12  5601  f1cnvcnv  5610  funforn  5623  dff1o2  5642  dff1o5  5646  f1orn  5647  resdif  5659  ffoss  5670  f11o  5671  f1o00  5673  fo00  5674  elfv  5689  fv3  5707  dffn5f  5744  dffv2  5759  eqfnfv3  5792  fndmdifeq0  5799  fneqeql  5801  unpreima  5819  respreima  5822  dff4  5846  dffo3  5847  dffo5  5849  f1ompt  5854  ffnfvf  5858  fmptco  5864  fsn2  5871  ftpg  5879  fconst3  5918  fconst4  5919  idref  5942  abrexco  5949  opabex3d  5952  opabex3  5953  abexssex  5965  dff13  5967  dff13f  5969  foeqcnvco  5990  isocnv3  6015  isoini  6021  weniso  6038  oprabid  6068  0neqopab  6082  dfoprab2  6084  eqoprab2b  6095  dmoprab  6117  rnoprab  6119  eloprabga  6123  mpt2mptx  6127  resoprab  6129  ffnov  6137  fnov  6141  elrnmpt2  6146  ralrnmpt2  6147  rexrnmpt2  6148  oprabex3  6151  oprabrexex2  6152  ovid  6153  ov3  6173  ov6g  6174  foov  6183  ndmovdistr  6199  difxp  6343  elopaba  6372  fmpt2  6381  curry1  6401  curry2  6404  fsplit  6414  frxp  6419  xporderlem  6420  soxp  6422  mpt2xopovel  6434  brtpos2  6448  dmtpos  6454  tpostpos  6462  tpossym  6474  tposoprab  6478  sorpsscmpl  6496  opiota  6498  eusvobj2  6545  dfsmo2  6572  tfrlem3  6601  tfrlem7  6607  tfrlem9  6609  tfrlem9a  6610  tz7.48lem  6661  tz7.49c  6666  el1o  6706  dif1o  6707  ondif2  6709  brwitnlem  6714  oarec  6768  omeulem1  6788  omeu  6791  oeordi  6793  oeeui  6808  oeeu  6809  omopthlem1  6861  dfer2  6869  brdifun  6895  swoso  6899  eqerlem  6900  qsid  6933  iiner  6939  erinxp  6941  brecop  6960  eroveu  6962  erovlem  6963  ecopovsym  6969  mapval2  7006  mapsn  7018  elixp  7032  ixpeq2  7039  ixpin  7050  ixpiin  7051  mptelixpg  7062  ixpsnf1o  7065  boxriin  7067  domen  7084  isfi  7094  en1  7137  xpsnen  7155  xpcomco  7161  xpassen  7165  sbthlem9  7188  0sdomg  7199  2pwuninel  7225  ssenen  7244  nneneq  7253  php  7254  modom2  7273  ac6sfi  7314  frfi  7315  fimaxg  7317  elfpw  7370  fissuni  7373  dffi3  7398  marypha1lem  7400  marypha2lem2  7403  dfsup2  7409  dfsup2OLD  7410  wofib  7474  wemapso2lem  7479  wdom2d  7508  unxpwdom2  7516  dford2  7535  inf2  7538  inf3lem2  7544  axinf2  7555  zfinf2  7557  cantnfp1lem2  7595  oemapso  7598  cantnflem1  7605  trcl  7624  epfrs  7627  rankvalb  7683  r1elss  7692  unbndrank  7728  scott0s  7772  cplem1  7773  bnd2  7777  isnum2  7792  iscard2  7823  infxpenlem  7855  fseqenlem1  7865  acnnum  7893  infpwfien  7903  alephnbtwn2  7913  alephord2  7917  alephislim  7924  cardaleph  7930  alephval3  7951  aceq1  7958  aceq2  7960  dfac3  7962  dfac4  7963  dfac5lem1  7964  dfac5lem2  7965  dfac5lem3  7966  dfac5lem4  7967  dfac5lem5  7968  dfac2  7971  dfac0  7973  dfac1  7974  dfac8  7975  dfac9  7976  dfac12  7989  kmlem3  7992  kmlem4  7993  kmlem7  7996  kmlem8  7997  kmlem9  7998  kmlem13  8002  kmlem14  8003  kmlem15  8004  dfackm  8006  pwsdompw  8044  ackbij2lem2  8080  cf0  8091  cfval2  8100  cflim2  8103  cfss  8105  cfslb  8106  isfin3  8136  isfin5  8139  isfin6  8140  sdom2en01  8142  fin23lem25  8164  fin23lem26  8165  fin23lem40  8191  isfin1-2  8225  isfin1-3  8226  fin1a2lem5  8244  fin1a2lem6  8245  fin1a2lem12  8251  fin12  8253  domtriomlem  8282  axdc2lem  8288  axdc3lem2  8291  axdc3lem4  8293  axcclem  8297  ac6num  8319  ac6n  8325  zorn2lem6  8341  zornn0g  8345  ttukeylem6  8354  ttukey2g  8356  brdom7disj  8369  brdom6disj  8370  iunfo  8374  iundom2g  8375  konigthlem  8403  alephsuc3  8415  elgch  8457  fpwwe2lem9  8473  fpwwe2lem12  8476  fpwwe2lem13  8477  fpwwe2  8478  canth4  8482  canthwe  8486  wunex2  8573  uniwun  8575  axgroth5  8659  grothpw  8661  axgroth6  8663  grothprimlem  8668  grothprim  8669  elni  8713  ltexpi  8739  nqerf  8767  nqerid  8770  ordpipq  8779  recmulnq  8801  npomex  8833  genpnnp  8842  genpass  8846  addcompr  8858  mulcompr  8860  reclem2pr  8885  reclem3pr  8886  ltsosr  8929  ltasr  8935  mappsrpr  8943  map2psrpr  8945  opelcn  8964  elreal  8966  elreal2  8967  axaddf  8980  axmulf  8981  axicn  8985  axrrecex  8998  axpre-mulgt0  9003  xrlenlt  9103  ssxr  9105  leloe  9121  msq0i  9629  infm3  9927  supmullem2  9935  inelr  9950  arch  10178  elnnne0  10195  un0addcl  10213  un0mulcl  10214  nn0n0n1ge2b  10241  elnnz  10252  elznn0nn  10255  elznn0  10256  elznn  10257  elz2  10258  raluz2  10486  rexuz2  10488  nnwos  10504  eluz2b2  10508  eluz2b3  10509  ublbneg  10520  zmin  10530  elq  10536  ralrp  10590  rexrp  10591  ltxr  10675  xrnemnf  10678  xrleloe  10697  xrltlen  10699  xrrebnd  10716  xaddf  10770  xmullem  10803  xmullem2  10804  xrsupss  10847  xrinfmss  10848  elfzp1  11057  fzprval  11066  fztpval  11067  4fvwrd4  11080  fzm1  11086  fzolb  11104  fzolb2  11105  elfzo3  11114  fzouzsplit  11127  fzo0n0  11133  fzind2  11157  uzrdgfni  11257  subsq0i  11453  crreczi  11463  nn0le2msqi  11519  nn0opth2i  11523  hashkf  11579  hashinfxadd  11618  hashgt12el  11641  hashgt12el2  11642  hashtpg  11650  hashfun  11659  hashbclem  11660  hashbc  11661  hashf1lem2  11664  leiso  11667  iswrd  11688  f1oun2prg  11823  climeu  12308  lo1resb  12317  rlimresb  12318  o1resb  12319  climmpt2  12326  fsum2dlem  12513  rpnnen2  12784  sqr2irr  12807  divides  12813  odd2np1  12867  divalglem1  12873  divalglem6  12877  divalglem10  12881  divalgb  12883  bitsval2  12896  bitsmod  12907  bitscmp  12909  smueqlem  12961  isprm2  13046  isprm3  13047  isprm4  13048  isprm5  13071  pythagtriplem19  13166  pythagtrip  13167  pceu  13179  prmreclem2  13244  4sqlem2  13276  4sqlem12  13283  vdwpc  13307  vdwnn  13325  dec5dvds2  13360  pwsle  13673  imasleval  13725  xpsfrnel  13747  xpsfrnel2  13749  xpsle  13765  isacs2  13837  mreacs  13842  iscatd2  13865  comfeq  13891  oppcsect  13958  isfunc  14020  funcoppc  14031  isffth2  14072  fucinv  14129  elhoma  14146  setcinv  14204  ispos  14363  ispos2  14364  tosso  14424  istsr2  14609  spwmo  14617  ismnd  14651  mndcl  14654  issubm  14707  gsumwspan  14750  issubg  14903  isnsg2  14929  eqger  14949  isgim2  15011  giclcl  15018  gicrcl  15019  gicsubgen  15024  gaorber  15044  resscntz  15089  cntzrec  15091  efgval2  15315  efgsfo  15330  efgrelexlemb  15341  isabl2  15379  iscyggen2  15450  iscyg2  15451  iscyg3  15455  lt6abl  15463  gsumval3eu  15472  gsum2d2  15507  dmdprdd  15519  subgdmdprd  15551  iscrng2  15638  dvdsrtr  15716  isunit  15721  isnirred  15764  isirred2  15765  isrhm  15783  isdrng2  15804  drngprop  15805  isabv  15866  issrng  15897  islmod  15913  islss  15970  lss1d  15998  islmim2  16097  lmiclcl  16101  lmicrcl  16102  lsmelval2  16116  lspsolvlem  16173  lspsncv0  16177  islpidl  16276  islpir2  16281  isnzr2  16293  isdomn2  16318  fiidomfld  16327  aspval2  16364  mplcoe1  16487  mplcoe2  16489  evlslem4  16523  xrsdsreclb  16704  unocv  16866  iunocv  16867  ishil2  16905  isobs  16906  obselocv  16914  iinopn  16934  istps4OLD  16947  istps5OLD  16948  istps  16960  istps2  16961  isbasis2g  16972  tgval2  16980  elcls  17096  neipeltop  17152  neiptopuni  17153  islpi  17171  isperf2  17174  isperf3  17175  neitr  17202  restntr  17204  ordtrest2lem  17225  cnrest  17307  ist0-3  17367  ist1-2  17369  ist1-3  17371  nrmsep3  17377  isnrm2  17380  perfcls  17387  ordthaus  17406  cmpcov2  17411  cmpsub  17421  hauscmplem  17427  cmpfi  17429  iscon2  17434  dfcon2  17439  is1stc2  17462  is2ndc  17466  1stcelcls  17481  1stccn  17483  llyi  17494  subislly  17501  iskgen3  17538  txuni2  17554  ptpjpre1  17560  ptbasin  17566  tx1cn  17598  tx2cn  17599  uptx  17614  txdis1cn  17624  ptrescn  17628  txtube  17629  txcmplem1  17630  hausdiag  17634  txkgen  17641  xkohaus  17642  xkococnlem  17648  xkoinjcn  17676  qtopeu  17705  isr0  17726  regr1lem2  17729  hmphsym  17771  elmptrab2  17817  isfbas  17818  isfbas2  17824  trfbas  17833  snfil  17853  fbunfip  17858  elfg  17860  fgcl  17867  fbasrn  17873  filuni  17874  trfil2  17876  cfinfil  17882  csdfil  17883  supfil  17884  ufinffr  17918  rnelfmlem  17941  elflim2  17953  hausflim  17970  hauspwpwf1  17976  txflf  17995  isfcls2  18002  fclsopn  18003  fclsrest  18013  alexsubALTlem2  18036  alexsubALTlem3  18037  alexsubALTlem4  18038  tmdcn2  18076  divstgplem  18107  divstgphaus  18109  tsmssubm  18129  istdrg2  18164  ustfilxp  18199  ust0  18206  fmucndlem  18278  metn0  18347  prdsxmetlem  18355  imasdsf1olem  18360  xpsdsval  18368  blres  18418  xmeterval  18419  xmeter  18420  isxms2  18435  isms2  18437  metustsymOLD  18548  metustsym  18549  dscopn  18578  isngp3  18602  isnvc2  18691  isnghm  18714  qtopbaslem  18749  xrtgioo  18794  zcld  18801  elii1  18917  pi1cpbl  19026  tchcph  19151  cmetss  19224  bcth  19239  lssbn  19261  ishl2  19281  minveclem3b  19286  minveclem6  19292  pmltpc  19304  ovolfcl  19320  ovolgelb  19333  ovolunlem1  19350  ovoliunlem1  19355  ismbl  19379  ismbl2  19380  iundisj2  19400  dyadmax  19447  dyadmbllem  19448  vitalilem2  19458  mbfimaopnlem  19504  itg1climres  19563  itg2l  19578  itg2leub  19583  iblcnlem1  19636  ellimc2  19721  ellimc3  19723  limcmpt  19727  limcres  19730  elaa  20190  aaliou3lem9  20224  taylthlem2  20247  ulmcau  20268  pilem1  20324  sincosq1lem  20362  sineq0  20386  coseq1  20387  ellogrn  20414  logtayl2  20510  cxpcn3lem  20588  cxpcn3  20589  cubic  20646  atandm  20673  atandm2  20674  atandm4  20676  atans2  20728  xrlimcnp  20764  wilthlem2  20809  dvdsflsumcom  20930  dvdsmulf1o  20936  fsumvma  20954  logfac2  20958  dchrelbas2  20978  dchrelbas3  20979  lgsdir2lem4  21067  lgsquadlem1  21095  lgsquadlem2  21096  2sqlem1  21104  pntlem3  21260  ostth  21290  usgra2edg1  21360  usgraedg4  21363  nbgrasym  21406  nb3grapr  21419  nb3grapr2  21420  cusgra2v  21428  cusgra3v  21430  uvtx01vtx  21458  trls  21493  0wlk  21502  0trl  21503  wlkntrllem1  21516  wlkntrllem2  21517  is2wlk  21522  3v3e3cycl1  21588  3v3e3cycl2  21608  vdgrun  21629  vdgrfiun  21630  eupath  21660  avril1  21714  grpoidinvlem3  21751  issubgo  21848  islno  22211  nmoubi  22230  nmobndseqi  22237  siii  22311  minvecolem5  22340  minvecolem6  22341  hvsubaddi  22525  normsub0i  22594  bcsiALT  22638  hcau  22643  hlimadd  22652  hhcmpl  22659  hhcms  22662  issh2  22668  isch2  22683  hlim0  22695  isch3  22701  norm1exi  22709  elch0  22713  hhsssh2  22727  choc0  22785  pjhtheu  22853  pjpreeq  22857  omlsilem  22861  pjoc2i  22897  chsscon1i  22921  spanuni  23003  h1deoi  23008  h1dei  23009  elspansni  23017  cmcm4i  23054  cmbr3i  23059  cmbr4i  23060  osumcor2i  23103  5oalem7  23119  3oalem3  23123  pjss2i  23139  mayete3iOLD  23188  elcnop  23317  ellnop  23318  elhmop  23333  elcnfn  23342  ellnfn  23343  cnvadj  23352  nmopub  23368  nmfnleub  23385  eleigvec  23417  nmop0  23446  nmfn0  23447  nmopun  23474  lncnopbd  23497  riesz2  23526  nmopcoadj0i  23563  rnbra  23567  pjnmopi  23608  pjssdif1i  23635  pjin2i  23653  pjin3i  23654  pjclem1  23655  cvbr2  23743  cvnbtwn3  23748  cvnbtwn4  23749  mdsl2bi  23783  mdsldmd1i  23791  elat2  23800  chrelat2i  23825  atomli  23842  chirredi  23854  mdsymlem6  23868  mdsymlem8  23870  sumdmdii  23875  dmdbr5ati  23882  cdj3i  23901  xfree2  23905  abeq2f  23917  r19.41vv  23927  mo5f  23929  nmo  23930  2reuswap2  23932  reuxfr3d  23933  rexunirn  23935  rmo3f  23939  rmo4fOLD  23940  rmo4f  23941  difeq  23955  disjorf  23978  disjorsf  23979  iundisj2f  23987  dfrel4  23991  suppss2f  24006  abfmpunirn  24021  fmptdF  24026  mptfnf  24030  fmptcof2  24033  ofpreima  24038  funcnvmptOLD  24039  funcnvmpt  24040  funcnv5mpt  24041  gtiso  24045  disjdsct  24047  iundisj2fi  24110  elxrge02  24135  toslub  24148  tosglb  24149  ofldsqr  24197  isarchi  24209  eldiftp  24350  esumnul  24400  esumpfinvalf  24423  isrnsigaOLD  24452  isrnsiga  24453  measiuns  24528  elunirnmbfm  24560  1stmbfm  24567  2ndmbfm  24568  dya2iocnrect  24588  sibfof  24611  ballotlemelo  24702  ballotlemodife  24712  ballotlem4  24713  eldmgm  24763  subfacp1lem5  24827  subfacp1lem6  24828  cvmscld  24917  cvmlift2lem12  24958  ghomgrpilem2  25054  axextprim  25107  axrepprim  25108  axunprim  25109  axpowprim  25110  axregprim  25111  axinfprim  25112  axacprim  25113  untangtr  25120  biimpexp  25130  dfid4  25140  divelunit  25142  divcnvshft  25168  divcnvlin  25169  ntrivcvgmul  25187  prodsn  25243  fprod2dlem  25261  dftr6  25325  coep  25326  coepr  25327  dffr5  25328  dfpo2  25330  cnvco1  25335  cnvco2  25336  eldm3  25337  fundmpss  25340  dfdm5  25350  dfrn5  25351  elpotr  25355  dford5reg  25356  dfon2lem5  25361  dfon2lem6  25362  dfon2lem8  25364  dfon2lem9  25365  dfon2  25366  wfi  25425  eltrpred  25447  frind  25461  poseq  25471  soseq  25472  wfrlem4  25477  wfrlem5  25478  wfrlem9  25482  wfrlem11  25484  wfrlem12  25485  wfrlem13  25486  wfrlem14  25487  wfrlem15  25488  tfrALTlem  25494  tfr3ALT  25497  frrlem5  25503  frrlem5e  25507  frrlem11  25511  nosgnn0  25530  nodenselem5  25557  nobnddown  25573  nofulllem5  25578  elsymdif  25585  brsymdif  25590  brtxp  25638  brpprod  25643  brpprod3b  25645  brsset  25647  idsset  25648  dfon3  25650  brtxpsd  25652  brtxpsd2  25653  brbigcup  25656  elfix  25661  dffix2  25663  ellimits  25668  dffun10  25671  elfuns  25672  snelsingles  25679  dfiota3  25680  brcart  25689  brimg  25694  brapply  25695  brcup  25696  brcap  25697  brsuccf  25698  funpartlem  25699  funpartfun  25700  fullfunfnv  25703  brrestrict  25706  dfrdg4  25707  tfrqfree  25708  altopthsn  25714  altopelaltxp  25729  altxpsspw  25730  mptelee  25742  brbtwn2  25752  colinearalg  25757  ax5seg  25785  axpasch  25788  axlowdimlem6  25794  axlowdimlem13  25801  axeuclidlem  25809  axeuclid  25810  axcontlem3  25813  axcontlem4  25814  axcontlem12  25822  brcolinear2  25900  broutsideof  25963  outsideofcom  25970  fvray  25983  fvline  25986  lineunray  25989  linecom  25992  linerflx2  25993  ellines  25994  bpoly2  26011  bpoly3  26012  rankeq1o  26020  elhf  26023  elhf2  26024  supadd  26142  mblfinlem  26147  ovoliunnfl  26151  voliunnfl  26153  mbfposadd  26157  cnambfre  26158  itg2addnclem2  26160  itg2addnclem3  26161  itg2addnc  26162  ecase13d  26210  trer  26213  elicc3  26214  finminlem  26215  opnrebl  26217  nn0prpw  26220  clsun  26225  fneval  26261  fnessref  26267  neibastop1  26282  neifg  26294  filnetlem4  26304  f1opr  26320  inixp  26324  sdclem2  26340  sdclem1  26341  fdc  26343  neificl  26353  istotbnd3  26374  sstotbnd3  26379  isbndx  26385  isbnd3b  26388  cntotbnd  26399  heibor1lem  26412  heibor1  26413  isdrngo2  26468  isdrngo3  26469  iscrngo2  26502  smprngopr  26556  isdmn2  26559  isfldidl2  26573  ispridlc  26574  isdmn3  26578  an43OLD  26590  prtlem70  26592  prtlem100  26598  n0el  26602  prter2  26624  funsnfsup  26637  cmpfiiin  26645  isnacs2  26654  elmzpcl  26677  diophrex  26728  2sbcrex  26737  sbcrot3  26741  sbcrot5  26742  3rexfrabdioph  26751  4rexfrabdioph  26752  6rexfrabdioph  26753  7rexfrabdioph  26754  fphpd  26771  fiphp3d  26774  rencldnfilem  26775  jm2.23  26961  expdiophlem1  26986  expdiophlem2  26987  expdioph  26988  dford4  26994  wopprc  26995  ttac  27001  fnwe2lem2  27020  islmodfg  27039  islnm2  27048  lnmlmic  27058  uvcvv0  27111  isnumbasgrplem1  27138  dfacbasgrp  27145  islinds2  27155  lmiclbs  27179  islnr2  27190  islnr3  27191  f1omvdco3  27264  issdrg2  27378  sdrgacs  27381  phisum  27390  isdomn3  27395  pm10.541  27434  pm10.542  27435  19.21vv  27446  19.36vv  27453  19.31vv  27454  19.37vv  27455  19.28vv  27456  pm11.6  27463  pm11.62  27465  pm14.12  27493  elnev  27510  evth2f  27557  elunif  27558  evthf  27569  stoweidlem31  27651  stoweidlem34  27654  stoweidlem51  27671  stoweidlem59  27679  aiffbbtat  27740  aisbbisfaisf  27741  aiffnbandciffatnotciffb  27743  abnotbtaxb  27755  mdandyvr0  27781  mdandyvr1  27782  mdandyvr2  27783  mdandyvr3  27784  mdandyvr4  27785  mdandyvr5  27786  mdandyvr6  27787  mdandyvr7  27788  rexrsb  27818  2rexsb  27819  2rexrsb  27820  cbvral2  27821  cbvrex2  27822  2ralbiim  27823  2reu5a  27826  rmoanim  27828  2rmoswap  27833  2reu1  27835  2reu3  27837  2reu4a  27838  afvpcfv0  27881  ffnaov  27934  ndmaovass  27941  ndmaovdistr  27942  raldifsnb  27950  rexdifpr  27951  dff14a  27963  dff14b  27964  f13dfv  27966  nn0fz0  27983  swrdnd  28005  usgra2pthspth  28039  usgra2pthlem1  28044  el2wlkonotot0  28073  usg2spthonot0  28090  frisusgranb  28105  frgra3v  28110  2pthfrgrarn  28117  2pthfrgra  28119  frgrawopreglem3  28153  frgrawopreglem4  28154  frgrawopreg  28156  frgrawopreg2  28158  usg2spot2nb  28172  usgreg2spot  28174  gte-lteh  28187  gt-lth  28188  sgnn  28242  onfrALTlem5  28343  onfrALTlem4  28344  onfrALTlem1  28349  2uasbanh  28363  dfvd2  28384  dfvd2an  28387  dfvd3  28396  dfvd3an  28399  eelT00  28521  eelTTT  28522  eelT12  28528  uunT1  28605  uunT1p1  28606  uun132p1  28611  un2122  28615  uunTT1p1  28619  uunTT1p2  28620  uunT11p1  28622  uunT11p2  28623  uunT12  28624  uunT12p1  28625  uunT12p2  28626  uunT12p3  28627  uunT12p4  28628  uunT12p5  28629  uun2221  28638  uun2221p1  28639  uun2221p2  28640  undif3VD  28707  onfrALTlem5VD  28710  onfrALTlem4VD  28711  onfrALTlem1VD  28715  2uasbanhVD  28736  bnj170  28772  bnj248  28774  bnj251  28776  bnj256  28780  bnj258  28782  bnj291  28785  bnj422  28789  bnj432  28790  bnj23  28793  bnj89  28796  bnj132  28801  bnj156  28805  bnj158  28806  bnj538  28818  bnj563  28821  bnj945  28854  bnj946  28855  bnj976  28858  bnj1098  28864  bnj1138  28869  bnj1209  28878  bnj1476  28928  bnj1542  28938  bnj110  28939  bnj91  28942  bnj92  28943  bnj106  28949  bnj118  28950  bnj124  28952  bnj125  28953  bnj153  28961  bnj207  28962  bnj222  28964  bnj518  28967  bnj535  28971  bnj539  28972  bnj543  28974  bnj553  28979  bnj556  28981  bnj558  28983  bnj571  28987  bnj605  28988  bnj591  28992  bnj594  28993  bnj580  28994  bnj609  28998  bnj611  28999  bnj865  29004  bnj849  29006  bnj916  29014  bnj917  29015  bnj934  29016  bnj929  29017  bnj944  29019  bnj953  29020  bnj1000  29022  bnj969  29027  bnj970  29028  bnj978  29030  bnj983  29032  bnj984  29033  bnj985  29034  bnj986  29035  bnj1021  29045  bnj1033  29048  bnj1049  29053  bnj1052  29054  bnj1083  29057  bnj1112  29062  bnj1030  29066  bnj1137  29074  bnj1189  29088  bnj1204  29091  bnj1253  29096  bnj1279  29097  bnj1373  29109  bnj1388  29112  bnj1398  29113  bnj1450  29129  sborNEW7  29274  sbrimNEW7  29275  sblimNEW7  29276  sbanNEW7  29277  sbbiNEW7  29278  sbid2NEW7  29290  sbco2dwAUX7  29293  sb8ewAUX7  29299  exsbOLDNEW7  29305  sbnf2NEW7  29313  2sb5NEW7  29314  2sb6NEW7  29315  sb6aNEW7  29316  sbexNEW7  29322  sbalvNEW7  29323  sblbisNEW7  29346  sbrbisNEW7  29347  sbrbifNEW7  29348  alrot3OLD7  29370  alrot4OLD7  29371  exrot3OLD7  29384  exrot4OLD7  29385  aaanOLD7  29386  eeorOLD7  29387  pm11.53OLD7  29388  eeanOLD7  29390  cbvex4vOLD7  29426  sbco2dOLD7  29441  sb8eOLD7  29445  sbcom2OLD7  29449  2sb5rfOLD7  29450  2sb6rfOLD7  29451  2exsbOLD7  29456  lsateln0  29482  islshpat  29504  lcvbr2  29509  lcvbr3  29510  lcvnbtwn3  29515  islfl  29547  lshpsmreu  29596  lub0N  29676  glb0N  29680  cvrnbtwn3  29763  leat2  29781  isat3  29794  iscvlat2N  29811  ishlat2  29840  ishlat3N  29841  hlrelat5N  29887  hlrelat2  29889  3dim0  29943  2dim  29956  islpln5  30021  islvol5  30065  4atlem3  30082  dalem20  30179  ispsubsp2  30232  snatpsubN  30236  pmapglb  30256  elpadd  30285  paddasslem17  30322  dalawlem13  30369  pclfinN  30386  polval2N  30392  pclfinclN  30436  lhpex2leN  30499  isltrn2N  30606  cdleme0nex  30776  cdleme22b  30827  cdlemftr3  31051  dibopelvalN  31630  dibopelval2  31632  dibelval3  31634  diblsmopel  31658  dicelval3  31667  dihglb2  31829  doch11  31860  islpolN  31970  lcfls1N  32022  mapdval4N  32119  mapdrvallem2  32132
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