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

Theorem bitri 240
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 186 . . 3  |-  ( ph  ->  ps )
3 bitri.2 . . 3  |-  ( ps  <->  ch )
42, 3sylib 188 . 2  |-  ( ph  ->  ch )
53biimpri 197 . . 3  |-  ( ch 
->  ps )
65, 1sylibr 203 . 2  |-  ( ch 
->  ph )
74, 6impbii 180 1  |-  ( ph  <->  ch )
Colors of variables: wff set class
Syntax hints:    <-> wb 176
This theorem is referenced by:  bitr2i  241  bitr3i  242  bitr4i  243  bitrd  244  3bitri  262  3bitr2i  264  3bitr3i  266  3bitr4i  268  xchbinx  301  bibi12i  306  imbi12i  316  mt2bi  328  iman  413  orbi12i  507  or42  515  pm4.71r  612  biadan2  623  anbi2ci  677  anbi12i  678  anbi12ci  679  pm5.3  692  pm5.53  771  an42  798  orddi  839  anddi  840  rbaib  873  rbaibr  874  pm4.43  893  biluk  899  pm5.75  903  dn1  932  3orass  937  3anass  938  3ancomb  943  3anan32  946  3anan12  947  3anor  948  an6  1261  xor2  1301  falbitru  1342  falnantru  1346  truxortru  1348  truxorfal  1349  falxorfal  1351  exp3acom23g  1361  hadass  1376  hadbi  1377  hadrot  1380  cador  1381  cadan  1382  cadnot  1384  cadcomb  1386  cadrot  1387  cad1  1388  had1  1392  alex  1562  alinexa  1568  alexn  1569  exanali  1575  19.26-2  1584  19.26-3an  1585  albiim  1601  2albiim  1602  ax12bOLD  1675  alrot3  1724  alrot4  1725  19.21-2  1804  nf2  1810  19.27  1817  19.28  1818  19.36  1819  19.37  1821  19.44  1825  19.45  1826  exrot3  1830  exrot4  1831  aaan  1837  eeor  1838  19.23vv  1845  pm11.53  1846  19.41vv  1855  19.41vvv  1856  19.41vvvv  1857  19.42vv  1860  19.42vvv  1861  4exdistr  1864  eean  1865  cbvex4v  1965  sbor  2019  sbrim  2020  sblim  2021  sban  2022  sbbi  2024  sblbis  2025  sbrbis  2026  sbrbif  2027  sbid2  2037  sbco2d  2040  sb8e  2046  sbnf2  2060  2sb5  2064  2sb6  2065  sbcom2  2066  sb6a  2068  2sb5rf  2069  2sb6rf  2070  sbex  2080  sbalv  2081  exsbOLD  2083  2exsb  2084  eujust  2158  euf  2162  cbveu  2176  eu2  2181  mo2  2185  sbmo  2186  mo3  2187  mo4f  2188  eu4  2195  moanim  2212  2mo  2234  2mos  2235  2eu1  2236  2eu3  2238  2eu4  2239  2eu6  2241  exists1  2245  abid  2284  eleq12i  2361  abeq2  2401  abeq2i  2403  clabel  2417  abid2f  2457  sbabel  2458  neeq12i  2471  necon1abii  2510  neanior  2544  ralnex  2566  rexnal  2567  ralinexa  2601  rexanali  2602  r3al  2613  r19.26-2  2689  ralbiim  2693  r19.30  2698  ralcomf  2711  rexcomf  2712  rexrot4  2716  reean  2719  3reeanv  2721  rabbi  2731  cbvralf  2771  cbvreu  2775  cbvral2v  2785  cbvrex2v  2786  cbvral3v  2787  cbvralsv  2788  cbvrexsv  2789  sbralie  2790  rabeq2i  2798  issetf  2806  2gencl  2830  3gencl  2831  ceqsex2  2837  ceqsex3v  2839  ceqsex6v  2841  ceqsex8v  2842  gencbvex  2843  spc3gv  2886  eqvincf  2909  ceqsrex2v  2916  elrab2  2938  ralab  2939  ralrab  2940  rexab  2941  rexrab  2942  ralab2  2943  rexab2  2945  eueq3  2953  morex  2962  euxfr2  2963  euxfr  2964  euind  2965  reu2  2966  reu6  2967  rmo4  2971  reu4  2972  reu7  2973  rmoim  2977  2reuswap  2980  reuind  2981  2reu5lem1  2983  2reu5lem2  2984  2reu5  2986  sbcco  3026  sbccomlem  3074  sbccom  3075  ra5  3088  rmo3  3091  csbco  3103  sbnfc2  3154  csbabg  3155  cbvralcsf  3156  cbvreucsf  3158  dfss  3180  dfss2f  3184  ss2ab  3254  dfpss2  3274  dfpss3  3275  psseq12i  3280  sspsstri  3291  difeqri  3309  uneqri  3330  ssequn2  3361  unss  3362  rexun  3368  ralunb  3369  elin2  3372  ineqri  3375  dfss1  3386  dfss5  3387  nsspssun  3415  indifdir  3438  inrab2  3454  rabun2  3460  reuun2  3464  eq0  3482  0el  3484  abn0  3486  0pss  3505  disjr  3509  disj1  3510  disjpss  3518  undif4  3524  difin0ss  3533  inssdif0  3534  uneqdifeq  3555  r19.3rz  3558  r19.3rzv  3560  ralidm  3570  pwss  3652  dfpr2  3669  ralsns  3683  rexsns  3684  eltpg  3689  ralprg  3695  rexprg  3696  raltpg  3697  rextpg  3698  euabsn2  3711  eusn  3716  eldifsn  3762  rexdifsn  3766  difsnpss  3774  pwpw0  3779  ssunsn  3790  eqsn  3791  sstp  3794  tpss  3795  prel12  3805  preqsn  3808  pwsnALT  3838  pwtp  3840  eluniab  3855  elunirab  3856  unipr  3857  dfnfc2  3861  uniun  3862  uniin  3863  unissb  3873  elintab  3889  elintrab  3890  ssintab  3895  ssintrab  3901  intun  3910  intpr  3911  elrint  3919  iuncom4  3928  iuneq2  3937  dfiun2g  3951  ssiinf  3967  elriin  3990  iunxiun  4000  pwssb  4004  iunpwss  4007  dfdisj2  4011  nfdisj  4021  disjor  4023  disjors  4025  invdisj  4028  disjiun  4029  disjxiun  4036  disjxun  4037  cbvopab1  4105  dftr5  4132  trint  4144  inex1  4171  inuni  4189  axpweq  4203  nfnid  4220  zfpair2  4231  moabex  4248  exss  4252  elop  4255  otth  4266  copsex4g  4271  opeqsn  4278  opthwiener  4284  opelopabsbOLD  4289  brabga  4295  opelopabaf  4304  opabn0  4311  iunopab  4312  pwunss  4314  pwundifOLD  4317  dfid3  4326  pocl  4337  sotric  4356  isso2i  4362  somo  4364  frminex  4389  dfepfr  4394  wefrc  4403  ordtri3or  4440  ordtri2  4443  elsuci  4474  elsucg  4475  sucel  4481  on0eqel  4526  uniuni  4543  reusv2lem4  4554  reusv2lem5  4555  reusv2  4556  reusv3  4558  reuxfr2d  4573  elpwun  4583  iunpw  4586  dfwe2  4589  onintrab2  4609  ordpwsuc  4622  ordzsl  4652  dflim4  4655  tfindsg  4667  tfindes  4669  findsg  4699  elxp  4722  opelxp  4735  brxp  4736  rabxp  4741  opthprc  4752  brab2a  4754  opeliunxp  4756  xpundi  4757  xpundir  4758  elvvv  4765  brinxp  4768  brab2ga  4779  xp0r  4784  eqrelrel  4804  reliun  4822  reluni  4824  raliunxp  4841  rexiunxp  4842  ralxpf  4846  rexxpf  4847  iunxpf  4848  relop  4850  elcnv  4874  elcnv2  4875  dmin  4902  dmuni  4904  dmopab  4905  dmi  4909  rnopab  4940  elrnmpt1  4944  rncoeq  4964  resiexg  5013  dfima2  5030  dfima3  5031  elima2  5034  elima3  5035  imai  5043  elimasn  5054  epini  5059  dfse2  5062  cotr  5071  issref  5072  intasym  5074  asymref  5075  asymref2  5076  somin1  5095  cnvopab  5099  cnvi  5101  cnvdif  5103  imainss  5112  dfrel2  5140  dfrel3  5147  rnsnn0  5155  relsn2  5159  dmsnopg  5160  cnvcnvsn  5166  elxp4  5176  elxp5  5177  cnvresima  5178  mptpreima  5182  dfco2  5188  coundi  5190  coundir  5191  imaco  5194  coiun  5198  coi1  5204  relssdmrn  5209  relrelss  5212  ressn  5227  cnviin  5228  cnvpo  5229  cbviota  5240  dffun2  5281  dffun3  5282  dffun4  5283  dffun5  5284  dffun7  5296  dffun8  5297  dffun9  5298  funopab  5303  funun  5312  funcnvsn  5313  funcnv2  5325  funcnv  5326  fun2cnv  5328  fncnv  5330  fun11  5331  fununi  5332  imadif  5343  funimaexg  5345  fnunsn  5367  fnres  5376  fnopabg  5383  mptfng  5385  mptun  5390  fun  5421  fresaunres1  5430  fcnvres  5434  dff12  5452  f1cnvcnv  5461  funforn  5474  dff1o2  5493  dff1o5  5497  f1orn  5498  resdif  5510  ffoss  5521  f11o  5522  f1o00  5524  fo00  5525  brprcneu  5534  elfv  5539  fv3  5557  dffn5f  5593  dffv2  5608  eqfnfv3  5640  fndmdifeq0  5647  fneqeql  5649  unpreima  5667  respreima  5670  dff4  5690  dffo3  5691  dffo5  5693  f1ompt  5698  ffnfvf  5702  fmptco  5707  fsn2  5714  fconst3  5751  fconst4  5752  idref  5775  abrexco  5782  opabex3  5785  abexssex  5797  dff13  5799  dff13f  5800  f1mpt  5801  foeqcnvco  5820  isocnv3  5845  isoini  5851  weniso  5868  oprabid  5898  dfoprab2  5911  eqoprab2b  5922  dmoprab  5944  rnoprab  5946  eloprabga  5950  mpt2mptx  5954  resoprab  5956  ffnov  5964  fnov  5968  elrnmpt2  5973  ralrnmpt2  5974  rexrnmpt2  5975  oprabex3  5978  oprabrexex2  5979  ovid  5980  ov3  6000  ov6g  6001  foov  6010  ndmovdistr  6025  difxp  6169  elopaba  6198  fmpt2  6207  curry1  6226  curry2  6229  fsplit  6239  frxp  6241  xporderlem  6242  soxp  6244  brtpos2  6256  dmtpos  6262  tpostpos  6270  tpossym  6282  tposoprab  6286  sorpsscmpl  6304  opiota  6306  eusvobj2  6353  dfsmo2  6380  tfrlem3  6409  tfrlem7  6415  tfrlem9  6417  tfrlem9a  6418  tz7.48lem  6469  tz7.49c  6474  el1o  6514  dif1o  6515  ondif2  6517  brwitnlem  6522  oarec  6576  omeulem1  6596  omeu  6599  oeordi  6601  oeeui  6616  oeeu  6617  omopthlem1  6669  dfer2  6677  brdifun  6703  swoso  6707  eqerlem  6708  qsid  6741  iiner  6747  erinxp  6749  brecop  6767  eroveu  6769  erovlem  6770  ecopovsym  6776  mapval2  6813  mapsn  6825  elixp  6839  ixpeq2  6846  ixpin  6857  ixpiin  6858  mptelixpg  6869  ixpsnf1o  6872  boxriin  6874  domen  6891  isfi  6901  en1  6944  xpsnen  6962  xpcomco  6968  xpassen  6972  sbthlem9  6995  0sdomg  7006  2pwuninel  7032  ssenen  7051  nneneq  7060  php  7061  modom2  7080  ac6sfi  7117  frfi  7118  fimaxg  7120  elfpw  7173  fissuni  7176  dffi3  7200  marypha1lem  7202  marypha2lem2  7205  dfsup2  7211  dfsup2OLD  7212  wofib  7276  wemapso2lem  7281  wdom2d  7310  unxpwdom2  7318  dford2  7337  inf2  7340  inf3lem2  7346  axinf2  7357  zfinf2  7359  cantnfp1lem2  7397  oemapso  7400  cantnflem1  7407  trcl  7426  epfrs  7429  rankvalb  7485  r1elss  7494  unbndrank  7530  scott0s  7574  cplem1  7575  bnd2  7579  isnum2  7594  iscard2  7625  infxpenlem  7657  fseqenlem1  7667  acnnum  7695  infpwfien  7705  alephnbtwn2  7715  alephord2  7719  alephislim  7726  cardaleph  7732  alephval3  7753  aceq1  7760  aceq2  7762  dfac3  7764  dfac4  7765  dfac5lem1  7766  dfac5lem2  7767  dfac5lem3  7768  dfac5lem4  7769  dfac5lem5  7770  dfac2  7773  dfac0  7775  dfac1  7776  dfac8  7777  dfac9  7778  dfac12  7791  kmlem3  7794  kmlem4  7795  kmlem7  7798  kmlem8  7799  kmlem9  7800  kmlem13  7804  kmlem14  7805  kmlem15  7806  dfackm  7808  pwsdompw  7846  ackbij2lem2  7882  cf0  7893  cfval2  7902  cflim2  7905  cfss  7907  cfslb  7908  isfin3  7938  isfin5  7941  isfin6  7942  sdom2en01  7944  fin23lem25  7966  fin23lem26  7967  fin23lem40  7993  isfin1-2  8027  isfin1-3  8028  fin1a2lem5  8046  fin1a2lem6  8047  fin1a2lem12  8053  fin12  8055  domtriomlem  8084  axdc2lem  8090  axdc3lem2  8093  axdc3lem4  8095  axcclem  8099  ac6num  8122  ac9  8126  ac6n  8128  ac9s  8136  zorn2lem6  8144  zornn0g  8148  ttukeylem6  8157  ttukey2g  8159  brdom7disj  8172  brdom6disj  8173  iunfo  8177  iundom2g  8178  konigthlem  8206  alephsuc3  8218  elgch  8260  fpwwe2lem9  8276  fpwwe2lem12  8279  fpwwe2lem13  8280  fpwwe2  8281  canth4  8285  canthwe  8289  wunex2  8376  uniwun  8378  axgroth5  8462  grothpw  8464  axgroth6  8466  grothprimlem  8471  grothprim  8472  elni  8516  ltexpi  8542  nqerf  8570  nqerid  8573  ordpipq  8582  recmulnq  8604  npomex  8636  genpnnp  8645  genpass  8649  addcompr  8661  mulcompr  8663  reclem2pr  8688  reclem3pr  8689  ltsosr  8732  ltasr  8738  mappsrpr  8746  map2psrpr  8748  opelcn  8767  elreal  8769  elreal2  8770  axaddf  8783  axmulf  8784  axicn  8788  axrrecex  8801  axpre-mulgt0  8806  xrlenlt  8906  ssxr  8908  leloe  8924  msq0i  9431  infm3  9729  supmullem2  9737  inelr  9752  arch  9978  elnnne0  9995  un0addcl  10013  un0mulcl  10014  elnnz  10050  elznn0nn  10053  elznn0  10054  elznn  10055  elz2  10056  raluz2  10284  rexuz2  10286  nnwos  10302  eluz2b2  10306  eluz2b3  10307  ublbneg  10318  zmin  10328  elq  10334  ralrp  10388  rexrp  10389  ltxr  10473  xrnemnf  10476  xrleloe  10494  xrltlen  10496  xrrebnd  10513  xaddf  10567  xmullem  10600  xmullem2  10601  xrsupss  10643  xrinfmss  10644  elfzp1  10852  fzprval  10860  fztpval  10861  fzm1  10878  fzolb  10896  fzolb2  10897  elfzo3  10906  fzouzsplit  10917  fzo0n0  10921  fzind2  10939  uzrdgfni  11037  subsq0i  11232  crreczi  11242  nn0le2msqi  11298  nn0opth2i  11302  hashkf  11355  hashfun  11405  hashbclem  11406  hashbc  11407  hashf1lem2  11410  leiso  11413  iswrd  11431  climeu  12045  lo1resb  12054  rlimresb  12055  o1resb  12056  climmpt2  12063  fsum2dlem  12249  rpnnen2  12520  sqr2irr  12543  divides  12549  odd2np1  12603  divalglem1  12609  divalglem6  12613  divalglem10  12617  divalgb  12619  bitsval2  12632  bitsmod  12643  bitscmp  12645  smueqlem  12697  isprm2  12782  isprm3  12783  isprm4  12784  isprm5  12807  pythagtriplem19  12902  pythagtrip  12903  pceu  12915  prmreclem2  12980  4sqlem2  13012  4sqlem12  13019  vdwpc  13043  vdwnn  13061  dec5dvds2  13096  pwsle  13407  imasleval  13459  xpsfrnel  13481  xpsfrnel2  13483  xpsle  13499  isacs2  13571  mreacs  13576  iscatd2  13599  comfeq  13625  oppcsect  13692  isssc  13713  isfunc  13754  funcoppc  13765  isffth2  13806  fucinv  13863  elhoma  13880  setcinv  13938  ispos  14097  ispos2  14098  tosso  14158  istsr2  14343  spwmo  14351  ismnd  14385  mndcl  14388  issubm  14441  gsumwspan  14484  issubg  14637  isnsg2  14663  eqger  14683  isgim2  14745  giclcl  14752  gicrcl  14753  gicsubgen  14758  gaorber  14778  resscntz  14823  cntzrec  14825  efgval2  15049  efgsfo  15064  efgrelexlemb  15075  isabl2  15113  iscyggen2  15184  iscyg2  15185  iscyg3  15189  lt6abl  15197  gsumval3eu  15206  gsum2d2  15241  dmdprdd  15253  subgdmdprd  15285  iscrng2  15372  dvdsrtr  15450  isunit  15455  isnirred  15498  isirred2  15499  isrhm  15517  isdrng2  15538  drngprop  15539  isabv  15600  issrng  15631  islmod  15647  islss  15708  lss1d  15736  islmim2  15835  lmiclcl  15839  lmicrcl  15840  lsmelval2  15854  lspsolvlem  15911  lspsncv0  15915  islpidl  16014  islpir2  16019  isnzr2  16031  isdomn2  16056  fiidomfld  16065  aspval2  16102  mplcoe1  16225  mplcoe2  16227  evlslem4  16261  xrsdsreclb  16434  unocv  16596  iunocv  16597  ishil2  16635  isobs  16636  obselocv  16644  iinopn  16664  istps4OLD  16677  istps5OLD  16678  istps  16690  istps2  16691  isbasis2g  16702  tgval2  16710  elcls  16826  islpi  16896  isperf2  16899  isperf3  16900  restntr  16928  ordtbaslem  16934  ordtrest2lem  16949  cnrest  17029  ist0-3  17089  ist1-2  17091  ist1-3  17093  nrmsep3  17099  isnrm2  17102  perfcls  17109  ordthaus  17128  cmpcov2  17133  cmpsub  17143  hauscmplem  17149  cmpfi  17151  iscon2  17156  dfcon2  17161  is1stc2  17184  is2ndc  17188  1stcelcls  17203  1stccn  17205  llyi  17216  subislly  17223  iskgen3  17260  txuni2  17276  ptpjpre1  17282  ptbasin  17288  tx1cn  17319  tx2cn  17320  uptx  17335  txdis1cn  17345  ptrescn  17349  txtube  17350  txcmplem1  17351  hausdiag  17355  txkgen  17362  xkohaus  17363  xkococnlem  17369  xkoinjcn  17397  qtopeu  17423  isr0  17444  regr1lem2  17447  hmphsym  17489  elmptrab2  17539  isfbas  17540  isfbas2  17546  trfbas  17555  snfil  17575  fbunfip  17580  elfg  17582  fgcl  17589  fbasrn  17595  filuni  17596  trfil2  17598  cfinfil  17604  csdfil  17605  supfil  17606  ufinffr  17640  rnelfmlem  17663  elflim2  17675  hausflim  17692  hauspwpwf1  17698  txflf  17717  isfcls2  17724  fclsopn  17725  fclsrest  17735  alexsubALTlem2  17758  alexsubALTlem3  17759  alexsubALTlem4  17760  tmdcn2  17788  divstgplem  17819  divstgphaus  17821  tsmssubm  17841  istdrg2  17876  metn0  17940  prdsxmetlem  17948  imasdsf1olem  17953  xpsdsval  17961  blres  17993  xmeterval  17994  xmeter  17995  isxms2  18010  isms2  18012  dscopn  18112  isngp3  18136  isnvc2  18225  isnghm  18248  qtopbaslem  18283  xrtgioo  18328  zcld  18335  elii1  18449  pi1cpbl  18558  tchcph  18683  cmetss  18756  bcth  18767  lssbn  18789  ishl2  18803  minveclem3b  18808  minveclem6  18814  pmltpc  18826  ovolfcl  18842  ovolgelb  18855  ovolunlem1  18872  ovoliunlem1  18877  ismbl  18901  ismbl2  18902  iundisj2  18922  dyadmax  18969  dyadmbllem  18970  vitalilem2  18980  mbfimaopnlem  19026  itg1climres  19085  itg2l  19100  itg2leub  19105  iblcnlem1  19158  ellimc2  19243  ellimc3  19245  limcmpt  19249  limcres  19252  elaa  19712  aaliou3lem9  19746  taylthlem2  19769  ulmcau  19788  pilem1  19843  sincosq1lem  19881  sineq0  19905  coseq1  19906  ellogrn  19933  logtayl2  20025  cxpcn3lem  20103  cxpcn3  20104  cubic  20161  atandm  20188  atandm2  20189  atandm4  20191  atans2  20243  xrlimcnp  20279  wilthlem2  20323  dvdsflsumcom  20444  dvdsmulf1o  20450  fsumvma  20468  logfac2  20472  dchrelbas2  20492  dchrelbas3  20493  lgsdir2lem4  20581  lgsquadlem1  20609  lgsquadlem2  20610  2sqlem1  20618  pntlem3  20774  ostth  20804  avril1  20852  grpoidinvlem3  20889  issubgo  20986  elghom  21046  islno  21347  nmoubi  21366  nmobndseqi  21373  siii  21447  minvecolem5  21476  minvecolem6  21477  hvsubaddi  21661  normsub0i  21730  bcsiALT  21774  hcau  21779  hlimadd  21788  hhcmpl  21795  hhcms  21798  issh2  21804  isch2  21819  hlim0  21831  isch3  21837  norm1exi  21845  elch0  21849  hhsssh2  21863  choc0  21921  pjhtheu  21989  pjpreeq  21993  omlsilem  21997  pjoc2i  22033  chsscon1i  22057  spanuni  22139  h1deoi  22144  h1dei  22145  elspansni  22153  cmcm4i  22190  cmbr3i  22195  cmbr4i  22196  osumcor2i  22239  5oalem7  22255  3oalem3  22259  pjss2i  22275  mayete3iOLD  22324  elcnop  22453  ellnop  22454  elhmop  22469  elcnfn  22478  ellnfn  22479  cnvadj  22488  nmopub  22504  nmfnleub  22521  eleigvec  22553  nmop0  22582  nmfn0  22583  nmopun  22610  lncnopbd  22633  riesz2  22662  nmopcoadj0i  22699  rnbra  22703  pjnmopi  22744  pjssdif1i  22771  pjin2i  22789  pjin3i  22790  pjclem1  22791  cvbr2  22879  cvnbtwn3  22884  cvnbtwn4  22885  mdsl2bi  22919  mdsldmd1i  22927  elat2  22936  chrelat2i  22961  atomli  22978  chirredi  22990  mdsymlem6  23004  mdsymlem8  23006  sumdmdii  23011  dmdbr5ati  23018  cdj3i  23037  xfree2  23041  ballotlemelo  23062  ballotlem2  23063  ballotlemfmpn  23069  ballotlemodife  23072  ballotlem4  23073  ballotth  23112  elxrge02  23132  or3dir  23140  difeq  23144  abeq2f  23145  rabid2f  23151  2reuswap2  23153  reuxfr3d  23154  rexunirn  23156  mo5f  23159  nmo  23160  elim2if  23168  ssiun3  23172  iuninc  23174  r19.41vv  23179  disjex  23192  disjexc  23193  rmo3f  23194  rmo4fOLD  23195  rmo4f  23196  suppss2f  23216  dfrel4  23219  abfmpunirn  23231  fmptdF  23236  mptfnf  23241  fmptcof2  23244  funcnvmptOLD  23249  funcnvmpt  23250  funcnv5mpt  23251  gtiso  23256  disjorf  23371  disjorsf  23372  iundisj2fi  23379  iundisj2f  23381  disjdsct  23384  eldiftp  23410  esumnul  23442  esumpfinvalf  23459  esumpcvgval  23461  esumcvg  23469  isrnsigaOLD  23488  isrnsiga  23489  measiuns  23559  elunirnmbfm  23573  1stmbfm  23580  2ndmbfm  23581  eldmgm  23709  subfacp1lem5  23730  subfacp1lem6  23731  cvmscld  23819  cvmlift2lem12  23860  vdgrun  23908  eupath  23920  ghomgrpilem2  24008  axextprim  24062  axrepprim  24063  axunprim  24064  axpowprim  24065  axregprim  24066  axinfprim  24067  axacprim  24068  untangtr  24075  biimpexp  24085  divelunit  24095  prodmo  24159  dftr6  24178  coep  24179  coepr  24180  dffr5  24181  dfpo2  24183  cnvco1  24188  cnvco2  24189  eldm3  24190  fundmpss  24193  dfdm5  24203  dfrn5  24204  elpotr  24208  dford5reg  24209  dfon2lem5  24214  dfon2lem6  24215  dfon2lem8  24217  dfon2lem9  24218  dfon2  24219  wfi  24278  eltrpred  24300  frind  24314  poseq  24324  soseq  24325  wfrlem4  24330  wfrlem5  24331  wfrlem9  24335  wfrlem11  24337  wfrlem12  24338  wfrlem13  24339  wfrlem14  24340  wfrlem15  24341  tfrALTlem  24347  tfr3ALT  24350  frrlem5  24356  frrlem5e  24360  frrlem11  24364  nosgnn0  24383  nodenselem5  24410  nobnddown  24426  nofulllem5  24431  elsymdif  24438  brsymdif  24443  brtxp  24491  brpprod  24496  brpprod3b  24498  brsset  24500  idsset  24501  dfon3  24503  brtxpsd  24505  brtxpsd2  24506  brbigcup  24509  elfix  24514  dffix2  24516  ellimits  24521  dffun10  24524  elfuns  24525  snelsingles  24532  dfiota3  24533  brcart  24542  brimg  24547  brapply  24548  brcup  24549  brcap  24550  brsuccf  24551  funpartlem  24552  funpartfun  24553  fullfunfnv  24556  brrestrict  24559  dfrdg4  24560  tfrqfree  24561  altopthsn  24567  altopelaltxp  24582  altxpsspw  24583  mptelee  24595  brbtwn2  24605  colinearalg  24610  ax5seg  24638  axpasch  24641  axlowdimlem6  24647  axlowdimlem13  24654  axeuclidlem  24662  axeuclid  24663  axcontlem3  24666  axcontlem4  24667  axcontlem12  24675  brcolinear2  24753  broutsideof  24816  outsideofcom  24823  fvray  24836  fvline  24839  lineunray  24842  linecom  24845  linerflx2  24846  ellines  24847  bpoly2  24864  bpoly3  24865  rankeq1o  24873  elhf  24876  elhf2  24877  supadd  24996  ovoliunnfl  25001  itg2addnclem2  25004  itg2addnc  25005  r19.26-2a  25037  eeeeanv  25047  altdftru  25051  pm11.53g  25067  eqvinopb  25068  copsexgb  25069  ltl4ev  25095  albineal  25102  evevifev  25117  cnvref  25168  restidsing  25179  dffn5a  25233  repcpwti  25264  dfdir2  25394  apnei  25623  ismonc  25917  isepic  25927  isfunb  25938  issubcata  25949  isntr  25976  clscnc  26113  bisig0  26165  isconcl5a  26204  isconcl5ab  26205  isibg2  26213  bosser  26270  hpd  26272  ecase13d  26325  cnvresimaOLD  26329  trer  26330  elicc3  26331  finminlem  26334  opnrebl  26338  nn0prpw  26342  clsun  26349  fneval  26390  fnessref  26396  neibastop1  26411  neifg  26423  filnetlem4  26433  f1opr  26494  inixp  26502  sdclem2  26555  sdclem1  26556  fdc  26558  neificl  26570  istotbnd3  26598  sstotbnd3  26603  isbndx  26609  isbnd3b  26612  cntotbnd  26623  heibor1lem  26636  heibor1  26637  isdrngo2  26692  isdrngo3  26693  iscrngo2  26726  smprngopr  26780  isdmn2  26783  isfldidl2  26797  ispridlc  26798  isdmn3  26802  an43OLD  26816  prtlem70  26818  prtlem100  26824  n0el  26828  prter2  26852  funsnfsup  26865  cmpfiiin  26875  isnacs2  26884  elmzpcl  26907  diophrex  26958  2sbcrex  26967  sbcrot3  26971  sbcrot5  26972  3rexfrabdioph  26981  4rexfrabdioph  26982  6rexfrabdioph  26983  7rexfrabdioph  26984  ftp  26996  fphpd  27002  fiphp3d  27005  rencldnfilem  27006  jm2.23  27192  expdiophlem1  27217  expdiophlem2  27218  expdioph  27219  dford4  27225  wopprc  27226  ttac  27232  fnwe2lem2  27251  islmodfg  27270  islnm2  27279  lnmlmic  27289  uvcvv0  27342  isnumbasgrplem1  27369  dfacbasgrp  27376  islinds2  27386  lmiclbs  27410  islnr2  27421  islnr3  27422  f1omvdco3  27495  matrcl  27569  issdrg2  27609  sdrgacs  27612  phisum  27621  isdomn3  27626  pm10.541  27665  pm10.542  27666  19.21vv  27677  19.36vv  27684  19.31vv  27685  19.37vv  27686  19.28vv  27687  pm11.6  27694  pm11.62  27696  pm14.12  27724  elnev  27741  evth2f  27789  elunif  27790  evthf  27801  stoweidlem14  27866  stoweidlem24  27876  stoweidlem31  27883  stoweidlem34  27886  stoweidlem37  27889  stoweidlem51  27903  stoweidlem54  27906  stoweidlem57  27909  stoweidlem59  27911  aiffnbandciffatnotciffb  27975  mdandyvr0  28013  mdandyvr1  28014  mdandyvr2  28015  mdandyvr3  28016  mdandyvr4  28017  mdandyvr5  28018  mdandyvr6  28019  mdandyvr7  28020  mdandyvr8  28021  mdandyvr9  28022  mdandyvr10  28023  mdandyvr11  28024  mdandyvr12  28025  mdandyvr13  28026  mdandyvr14  28027  mdandyvr15  28028  rexrsb  28050  2rexsb  28051  2rexrsb  28052  cbvral2  28053  cbvrex2  28054  2ralbiim  28055  2reu5a  28058  rmoanim  28060  2rmoswap  28065  2reu1  28067  2reu3  28069  2reu4a  28070  afvpcfv0  28114  ffnaov  28167  ndmaovass  28174  ndmaovdistr  28175  jaoi2  28176  f1oun2prg  28187  opabex3d  28190  0neqopab  28192  mpt2xopovel  28202  hashtpg  28217  hashgt12el  28218  hashgt12el2  28219  4fvwrd4  28220  nbgrasym  28286  nb3grapr  28289  nb3grapr2  28290  cusgra2v  28297  cusgra3v  28299  uvtx01vtx  28305  trls  28335  0wlk  28343  0trl  28344  wlkntrllem1  28345  wlkntrllem3  28347  wlkntrllem4  28348  3v3e3cycl1  28390  3v3e3cycl2  28410  3v3e3cycl  28411  frgra3v  28426  2pthfrgrarn  28433  gte-lteh  28450  gt-lth  28451  sgnn  28505  onfrALTlem5  28606  onfrALTlem4  28607  onfrALTlem1  28612  2uasbanh  28626  dfvd2  28647  dfvd2an  28650  dfvd3  28659  dfvd3an  28662  eelT00  28785  eelTTT  28786  eelT12  28792  uunT1  28869  uunT1p1  28870  uun132p1  28875  un2122  28879  uunTT1p1  28883  uunTT1p2  28884  uunT11p1  28886  uunT11p2  28887  uunT12  28888  uunT12p1  28889  uunT12p2  28890  uunT12p3  28891  uunT12p4  28892  uunT12p5  28893  uun2221  28902  uun2221p1  28903  uun2221p2  28904  undif3VD  28974  onfrALTlem5VD  28977  onfrALTlem4VD  28978  onfrALTlem1VD  28982  2uasbanhVD  29003  bnj170  29039  bnj248  29041  bnj251  29043  bnj256  29047  bnj258  29049  bnj291  29052  bnj422  29056  bnj432  29057  bnj23  29060  bnj89  29063  bnj132  29068  bnj156  29072  bnj158  29073  bnj538  29085  bnj563  29088  bnj945  29121  bnj946  29122  bnj976  29125  bnj1098  29131  bnj1138  29136  bnj1209  29145  bnj1476  29195  bnj1542  29205  bnj110  29206  bnj91  29209  bnj92  29210  bnj106  29216  bnj118  29217  bnj124  29219  bnj125  29220  bnj153  29228  bnj207  29229  bnj222  29231  bnj518  29234  bnj535  29238  bnj539  29239  bnj543  29241  bnj553  29246  bnj556  29248  bnj558  29250  bnj571  29254  bnj605  29255  bnj591  29259  bnj594  29260  bnj580  29261  bnj609  29265  bnj611  29266  bnj865  29271  bnj849  29273  bnj882  29274  bnj916  29281  bnj917  29282  bnj934  29283  bnj929  29284  bnj944  29286  bnj953  29287  bnj1000  29289  bnj969  29294  bnj970  29295  bnj978  29297  bnj983  29299  bnj984  29300  bnj985  29301  bnj986  29302  bnj1021  29312  bnj1033  29315  bnj1049  29320  bnj1052  29321  bnj1083  29324  bnj1112  29329  bnj1030  29333  bnj1137  29341  bnj1189  29355  bnj1204  29358  bnj1253  29363  bnj1279  29364  bnj1373  29376  bnj1388  29379  bnj1398  29380  bnj1450  29396  sborNEW7  29541  sbrimNEW7  29542  sblimNEW7  29543  sbanNEW7  29544  sbbiNEW7  29545  sbid2NEW7  29557  sbco2dwAUX7  29560  sb8ewAUX7  29566  exsbOLDNEW7  29572  sbnf2NEW7  29580  2sb5NEW7  29581  2sb6NEW7  29582  sb6aNEW7  29583  sbexNEW7  29589  sbalvNEW7  29590  sblbisNEW7  29612  sbrbisNEW7  29613  sbrbifNEW7  29614  alrot3OLD7  29636  alrot4OLD7  29637  exrot3OLD7  29650  exrot4OLD7  29651  aaanOLD7  29652  eeorOLD7  29653  pm11.53OLD7  29654  eeanOLD7  29656  cbvex4vOLD7  29692  sbco2dOLD7  29707  sb8eOLD7  29711  sbcom2OLD7  29715  2sb5rfOLD7  29717  2sb6rfOLD7  29718  2exsbOLD7  29723  equvelv  29738  a12study4  29739  a12study8  29741  a12peros  29743  a12lem2  29753  a12study10  29758  a12study10n  29759  lsateln0  29807  islshpat  29829  lcvbr2  29834  lcvbr3  29835  lcvnbtwn3  29840  islfl  29872  lshpsmreu  29921  lub0N  30001  glb0N  30005  cvrnbtwn3  30088  leat2  30106  isat3  30119  iscvlat2N  30136  ishlat2  30165  ishlat3N  30166  hlrelat5N  30212  hlrelat2  30214  3dim0  30268  2dim  30281  islpln5  30346  islvol5  30390  4atlem3  30407  dalem20  30504  ispsubsp2  30557  snatpsubN  30561  pmapglb  30581  elpadd  30610  paddasslem17  30647  dalawlem13  30694  pclfinN  30711  polval2N  30717  pclfinclN  30761  lhpex2leN  30824  isltrn2N  30931  cdleme0nex  31101  cdleme22b  31152  cdlemftr3  31376  tendoset  31570  diarnN  31941  dibopelvalN  31955  dibopelval2  31957  dibelval3  31959  diblsmopel  31983  dicelval3  31992  dihglb2  32154  doch11  32185  islpolN  32295  lcfls1N  32347  mapdval4N  32444  mapdrvallem2  32457
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 177
  Copyright terms: Public domain W3C validator