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  1559  alinexa  1565  alexn  1566  exanali  1572  19.26-2  1581  19.26-3an  1582  albiim  1598  2albiim  1599  ax12bOLD  1656  alrot3  1712  alrot4  1713  19.21-2  1792  nf2  1798  19.27  1805  19.28  1806  19.36  1807  19.37  1809  19.44  1813  19.45  1814  exrot3  1818  exrot4  1819  aaan  1825  eeor  1826  19.23vv  1833  pm11.53  1834  19.41vv  1843  19.41vvv  1844  19.41vvvv  1845  19.42vv  1848  19.42vvv  1849  4exdistr  1852  eean  1853  cbvex4v  1952  sbor  2006  sbrim  2007  sblim  2008  sban  2009  sbbi  2011  sblbis  2012  sbrbis  2013  sbrbif  2014  sbid2  2024  sbco2d  2027  sb8e  2033  sbnf2  2047  2sb5  2051  2sb6  2052  sbcom2  2053  sb6a  2055  2sb5rf  2056  2sb6rf  2057  sbex  2067  sbalv  2068  exsbOLD  2070  2exsb  2071  eujust  2145  euf  2149  cbveu  2163  eu2  2168  mo2  2172  sbmo  2173  mo3  2174  mo4f  2175  eu4  2182  moanim  2199  2mo  2221  2mos  2222  2eu1  2223  2eu3  2225  2eu4  2226  2eu6  2228  exists1  2232  abid  2271  eleq12i  2348  abeq2  2388  abeq2i  2390  clabel  2404  abid2f  2444  sbabel  2445  neeq12i  2458  necon1abii  2497  neanior  2531  ralnex  2553  rexnal  2554  ralinexa  2588  rexanali  2589  r3al  2600  r19.26-2  2676  ralbiim  2680  r19.30  2685  ralcomf  2698  rexcomf  2699  rexrot4  2703  reean  2706  3reeanv  2708  rabbi  2718  cbvralf  2758  cbvreu  2762  cbvral2v  2772  cbvrex2v  2773  cbvral3v  2774  cbvralsv  2775  cbvrexsv  2776  sbralie  2777  rabeq2i  2785  issetf  2793  2gencl  2817  3gencl  2818  ceqsex2  2824  ceqsex3v  2826  ceqsex6v  2828  ceqsex8v  2829  gencbvex  2830  spc3gv  2873  eqvincf  2896  ceqsrex2v  2903  elrab2  2925  ralab  2926  ralrab  2927  rexab  2928  rexrab  2929  ralab2  2930  rexab2  2932  eueq3  2940  morex  2949  euxfr2  2950  euxfr  2951  euind  2952  reu2  2953  reu6  2954  rmo4  2958  reu4  2959  reu7  2960  rmoim  2964  2reuswap  2967  reuind  2968  2reu5lem1  2970  2reu5lem2  2971  2reu5  2973  sbcco  3013  sbccomlem  3061  sbccom  3062  ra5  3075  rmo3  3078  csbco  3090  sbnfc2  3141  csbabg  3142  cbvralcsf  3143  cbvreucsf  3145  dfss  3167  dfss2f  3171  ss2ab  3241  dfpss2  3261  dfpss3  3262  psseq12i  3267  sspsstri  3278  difeqri  3296  uneqri  3317  ssequn2  3348  unss  3349  rexun  3355  ralunb  3356  elin2  3359  ineqri  3362  dfss1  3373  dfss5  3374  nsspssun  3402  indifdir  3425  inrab2  3441  rabun2  3447  reuun2  3451  eq0  3469  0el  3471  abn0  3473  0pss  3492  disjr  3496  disj1  3497  disjpss  3505  undif4  3511  difin0ss  3520  inssdif0  3521  uneqdifeq  3542  r19.3rz  3545  r19.3rzv  3547  ralidm  3557  pwss  3639  dfpr2  3656  ralsns  3670  rexsns  3671  eltpg  3676  ralprg  3682  rexprg  3683  raltpg  3684  rextpg  3685  euabsn2  3698  eusn  3703  eldifsn  3749  rexdifsn  3753  difsnpss  3758  pwpw0  3763  ssunsn  3774  eqsn  3775  sstp  3778  tpss  3779  prel12  3789  preqsn  3792  pwsnALT  3822  pwtp  3824  eluniab  3839  elunirab  3840  unipr  3841  dfnfc2  3845  uniun  3846  uniin  3847  unissb  3857  elintab  3873  elintrab  3874  ssintab  3879  ssintrab  3885  intun  3894  intpr  3895  elrint  3903  iuncom4  3912  iuneq2  3921  dfiun2g  3935  ssiinf  3951  elriin  3974  iunxiun  3984  pwssb  3988  iunpwss  3991  dfdisj2  3995  nfdisj  4005  disjor  4007  disjors  4009  invdisj  4012  disjiun  4013  disjxiun  4020  disjxun  4021  cbvopab1  4089  dftr5  4116  trint  4128  inex1  4155  inuni  4173  axpweq  4187  nfnid  4204  zfpair2  4215  moabex  4232  exss  4236  elop  4239  otth  4250  copsex4g  4255  opeqsn  4262  opthwiener  4268  opelopabsbOLD  4273  brabga  4279  opelopabaf  4288  opabn0  4295  iunopab  4296  pwunss  4298  pwundifOLD  4301  dfid3  4310  pocl  4321  sotric  4340  isso2i  4346  somo  4348  frminex  4373  dfepfr  4378  wefrc  4387  ordtri3or  4424  ordtri2  4427  elsuci  4458  elsucg  4459  sucel  4465  on0eqel  4510  uniuni  4527  reusv2lem4  4538  reusv2lem5  4539  reusv2  4540  reusv3  4542  reuxfr2d  4557  elpwun  4567  iunpw  4570  dfwe2  4573  onintrab2  4593  ordpwsuc  4606  ordzsl  4636  dflim4  4639  tfindsg  4651  tfindes  4653  findsg  4683  elxp  4706  opelxp  4719  brxp  4720  rabxp  4725  opthprc  4736  brab2a  4738  opeliunxp  4740  xpundi  4741  xpundir  4742  elvvv  4749  brinxp  4752  brab2ga  4763  xp0r  4768  eqrelrel  4788  reliun  4806  reluni  4808  raliunxp  4825  rexiunxp  4826  ralxpf  4830  rexxpf  4831  iunxpf  4832  relop  4834  elcnv  4858  elcnv2  4859  dmin  4886  dmuni  4888  dmopab  4889  dmi  4893  rnopab  4924  elrnmpt1  4928  rncoeq  4948  resiexg  4997  dfima2  5014  dfima3  5015  elima2  5018  elima3  5019  imai  5027  elimasn  5038  epini  5043  dfse2  5046  cotr  5055  issref  5056  intasym  5058  asymref  5059  asymref2  5060  somin1  5079  cnvopab  5083  cnvi  5085  cnvdif  5087  imainss  5096  dfrel2  5124  dfrel3  5131  rnsnn0  5139  relsn2  5143  dmsnopg  5144  cnvcnvsn  5150  elxp4  5160  elxp5  5161  cnvresima  5162  mptpreima  5166  dfco2  5172  coundi  5174  coundir  5175  imaco  5178  coiun  5182  coi1  5188  relssdmrn  5193  relrelss  5196  ressn  5211  cnviin  5212  cnvpo  5213  cbviota  5224  dffun2  5265  dffun3  5266  dffun4  5267  dffun5  5268  dffun7  5280  dffun8  5281  dffun9  5282  funopab  5287  funun  5296  funcnvsn  5297  funcnv2  5309  funcnv  5310  fun2cnv  5312  fncnv  5314  fun11  5315  fununi  5316  imadif  5327  funimaexg  5329  fnunsn  5351  fnres  5360  fnopabg  5367  mptfng  5369  mptun  5374  fun  5405  fresaunres1  5414  fcnvres  5418  dff12  5436  f1cnvcnv  5445  funforn  5458  dff1o2  5477  dff1o5  5481  f1orn  5482  resdif  5494  ffoss  5505  f11o  5506  f1o00  5508  fo00  5509  brprcneu  5518  elfv  5523  fv3  5541  dffn5f  5577  dffv2  5592  eqfnfv3  5624  fndmdifeq0  5631  fneqeql  5633  unpreima  5651  respreima  5654  dff4  5674  dffo3  5675  dffo5  5677  f1ompt  5682  ffnfvf  5686  fmptco  5691  fsn2  5698  fconst3  5735  fconst4  5736  idref  5759  abrexco  5766  opabex3  5769  abexssex  5781  dff13  5783  dff13f  5784  f1mpt  5785  foeqcnvco  5804  isocnv3  5829  isoini  5835  weniso  5852  oprabid  5882  dfoprab2  5895  eqoprab2b  5906  dmoprab  5928  rnoprab  5930  eloprabga  5934  mpt2mptx  5938  resoprab  5940  ffnov  5948  fnov  5952  elrnmpt2  5957  ralrnmpt2  5958  rexrnmpt2  5959  oprabex3  5962  oprabrexex2  5963  ovid  5964  ov3  5984  ov6g  5985  foov  5994  ndmovdistr  6009  difxp  6153  elopaba  6182  fmpt2  6191  curry1  6210  curry2  6213  fsplit  6223  frxp  6225  xporderlem  6226  soxp  6228  brtpos2  6240  dmtpos  6246  tpostpos  6254  tpossym  6266  tposoprab  6270  sorpsscmpl  6288  opiota  6290  eusvobj2  6337  dfsmo2  6364  tfrlem3  6393  tfrlem7  6399  tfrlem9  6401  tfrlem9a  6402  tz7.48lem  6453  tz7.49c  6458  el1o  6498  dif1o  6499  ondif2  6501  brwitnlem  6506  oarec  6560  omeulem1  6580  omeu  6583  oeordi  6585  oeeui  6600  oeeu  6601  omopthlem1  6653  dfer2  6661  brdifun  6687  swoso  6691  eqerlem  6692  qsid  6725  iiner  6731  erinxp  6733  brecop  6751  eroveu  6753  erovlem  6754  ecopovsym  6760  mapval2  6797  mapsn  6809  elixp  6823  ixpeq2  6830  ixpin  6841  ixpiin  6842  mptelixpg  6853  ixpsnf1o  6856  boxriin  6858  domen  6875  isfi  6885  en1  6928  xpsnen  6946  xpcomco  6952  xpassen  6956  sbthlem9  6979  0sdomg  6990  2pwuninel  7016  ssenen  7035  nneneq  7044  php  7045  modom2  7064  ac6sfi  7101  frfi  7102  fimaxg  7104  elfpw  7157  fissuni  7160  dffi3  7184  marypha1lem  7186  marypha2lem2  7189  dfsup2  7195  dfsup2OLD  7196  wofib  7260  wemapso2lem  7265  wdom2d  7294  unxpwdom2  7302  dford2  7321  inf2  7324  inf3lem2  7330  axinf2  7341  zfinf2  7343  cantnfp1lem2  7381  oemapso  7384  cantnflem1  7391  trcl  7410  epfrs  7413  rankvalb  7469  r1elss  7478  unbndrank  7514  scott0s  7558  cplem1  7559  bnd2  7563  isnum2  7578  iscard2  7609  infxpenlem  7641  fseqenlem1  7651  acnnum  7679  infpwfien  7689  alephnbtwn2  7699  alephord2  7703  alephislim  7710  cardaleph  7716  alephval3  7737  aceq1  7744  aceq2  7746  dfac3  7748  dfac4  7749  dfac5lem1  7750  dfac5lem2  7751  dfac5lem3  7752  dfac5lem4  7753  dfac5lem5  7754  dfac2  7757  dfac0  7759  dfac1  7760  dfac8  7761  dfac9  7762  dfac12  7775  kmlem3  7778  kmlem4  7779  kmlem7  7782  kmlem8  7783  kmlem9  7784  kmlem13  7788  kmlem14  7789  kmlem15  7790  dfackm  7792  pwsdompw  7830  ackbij2lem2  7866  cf0  7877  cfval2  7886  cflim2  7889  cfss  7891  cfslb  7892  isfin3  7922  isfin5  7925  isfin6  7926  sdom2en01  7928  fin23lem25  7950  fin23lem26  7951  fin23lem40  7977  isfin1-2  8011  isfin1-3  8012  fin1a2lem5  8030  fin1a2lem6  8031  fin1a2lem12  8037  fin12  8039  domtriomlem  8068  axdc2lem  8074  axdc3lem2  8077  axdc3lem4  8079  axcclem  8083  ac6num  8106  ac9  8110  ac6n  8112  ac9s  8120  zorn2lem6  8128  zornn0g  8132  ttukeylem6  8141  ttukey2g  8143  brdom7disj  8156  brdom6disj  8157  iunfo  8161  iundom2g  8162  konigthlem  8190  alephsuc3  8202  elgch  8244  fpwwe2lem9  8260  fpwwe2lem12  8263  fpwwe2lem13  8264  fpwwe2  8265  canth4  8269  canthwe  8273  wunex2  8360  uniwun  8362  axgroth5  8446  grothpw  8448  axgroth6  8450  grothprimlem  8455  grothprim  8456  elni  8500  ltexpi  8526  nqerf  8554  nqerid  8557  ordpipq  8566  recmulnq  8588  npomex  8620  genpnnp  8629  genpass  8633  addcompr  8645  mulcompr  8647  reclem2pr  8672  reclem3pr  8673  ltsosr  8716  ltasr  8722  mappsrpr  8730  map2psrpr  8732  opelcn  8751  elreal  8753  elreal2  8754  axaddf  8767  axmulf  8768  axicn  8772  axrrecex  8785  axpre-mulgt0  8790  xrlenlt  8890  ssxr  8892  leloe  8908  msq0i  9415  infm3  9713  supmullem2  9721  inelr  9736  arch  9962  elnnne0  9979  un0addcl  9997  un0mulcl  9998  elnnz  10034  elznn0nn  10037  elznn0  10038  elznn  10039  elz2  10040  raluz2  10268  rexuz2  10270  nnwos  10286  eluz2b2  10290  eluz2b3  10291  ublbneg  10302  zmin  10312  elq  10318  ralrp  10372  rexrp  10373  ltxr  10457  xrnemnf  10460  xrleloe  10478  xrltlen  10480  xrrebnd  10497  xaddf  10551  xmullem  10584  xmullem2  10585  xrsupss  10627  xrinfmss  10628  elfzp1  10836  fzprval  10844  fztpval  10845  fzm1  10862  fzolb  10880  fzolb2  10881  elfzo3  10890  fzouzsplit  10901  fzo0n0  10905  fzind2  10923  uzrdgfni  11021  subsq0i  11216  crreczi  11226  nn0le2msqi  11282  nn0opth2i  11286  hashkf  11339  hashfun  11389  hashbclem  11390  hashbc  11391  hashf1lem2  11394  leiso  11397  iswrd  11415  climeu  12029  lo1resb  12038  rlimresb  12039  o1resb  12040  climmpt2  12047  fsum2dlem  12233  rpnnen2  12504  sqr2irr  12527  divides  12533  odd2np1  12587  divalglem1  12593  divalglem6  12597  divalglem10  12601  divalgb  12603  bitsval2  12616  bitsmod  12627  bitscmp  12629  smueqlem  12681  isprm2  12766  isprm3  12767  isprm4  12768  isprm5  12791  pythagtriplem19  12886  pythagtrip  12887  pceu  12899  prmreclem2  12964  4sqlem2  12996  4sqlem12  13003  vdwpc  13027  vdwnn  13045  dec5dvds2  13080  pwsle  13391  imasleval  13443  xpsfrnel  13465  xpsfrnel2  13467  xpsle  13483  isacs2  13555  mreacs  13560  iscatd2  13583  comfeq  13609  oppcsect  13676  isssc  13697  isfunc  13738  funcoppc  13749  isffth2  13790  fucinv  13847  elhoma  13864  setcinv  13922  ispos  14081  ispos2  14082  tosso  14142  istsr2  14327  spwmo  14335  ismnd  14369  mndcl  14372  issubm  14425  gsumwspan  14468  issubg  14621  isnsg2  14647  eqger  14667  isgim2  14729  giclcl  14736  gicrcl  14737  gicsubgen  14742  gaorber  14762  resscntz  14807  cntzrec  14809  efgval2  15033  efgsfo  15048  efgrelexlemb  15059  isabl2  15097  iscyggen2  15168  iscyg2  15169  iscyg3  15173  lt6abl  15181  gsumval3eu  15190  gsum2d2  15225  dmdprdd  15237  subgdmdprd  15269  iscrng2  15356  dvdsrtr  15434  isunit  15439  isnirred  15482  isirred2  15483  isrhm  15501  isdrng2  15522  drngprop  15523  isabv  15584  issrng  15615  islmod  15631  islss  15692  lss1d  15720  islmim2  15819  lmiclcl  15823  lmicrcl  15824  lsmelval2  15838  lspsolvlem  15895  lspsncv0  15899  islpidl  15998  islpir2  16003  isnzr2  16015  isdomn2  16040  fiidomfld  16049  aspval2  16086  mplcoe1  16209  mplcoe2  16211  evlslem4  16245  xrsdsreclb  16418  unocv  16580  iunocv  16581  ishil2  16619  isobs  16620  obselocv  16628  iinopn  16648  istps4OLD  16661  istps5OLD  16662  istps  16674  istps2  16675  isbasis2g  16686  tgval2  16694  elcls  16810  islpi  16880  isperf2  16883  isperf3  16884  restntr  16912  ordtbaslem  16918  ordtrest2lem  16933  cnrest  17013  ist0-3  17073  ist1-2  17075  ist1-3  17077  nrmsep3  17083  isnrm2  17086  perfcls  17093  ordthaus  17112  cmpcov2  17117  cmpsub  17127  hauscmplem  17133  cmpfi  17135  iscon2  17140  dfcon2  17145  is1stc2  17168  is2ndc  17172  1stcelcls  17187  1stccn  17189  llyi  17200  subislly  17207  iskgen3  17244  txuni2  17260  ptpjpre1  17266  ptbasin  17272  tx1cn  17303  tx2cn  17304  uptx  17319  txdis1cn  17329  ptrescn  17333  txtube  17334  txcmplem1  17335  hausdiag  17339  txkgen  17346  xkohaus  17347  xkococnlem  17353  xkoinjcn  17381  qtopeu  17407  isr0  17428  regr1lem2  17431  hmphsym  17473  elmptrab2  17523  isfbas  17524  isfbas2  17530  trfbas  17539  snfil  17559  fbunfip  17564  elfg  17566  fgcl  17573  fbasrn  17579  filuni  17580  trfil2  17582  cfinfil  17588  csdfil  17589  supfil  17590  ufinffr  17624  rnelfmlem  17647  elflim2  17659  hausflim  17676  hauspwpwf1  17682  txflf  17701  isfcls2  17708  fclsopn  17709  fclsrest  17719  alexsubALTlem2  17742  alexsubALTlem3  17743  alexsubALTlem4  17744  tmdcn2  17772  divstgplem  17803  divstgphaus  17805  tsmssubm  17825  istdrg2  17860  metn0  17924  prdsxmetlem  17932  imasdsf1olem  17937  xpsdsval  17945  blres  17977  xmeterval  17978  xmeter  17979  isxms2  17994  isms2  17996  dscopn  18096  isngp3  18120  isnvc2  18209  isnghm  18232  qtopbaslem  18267  xrtgioo  18312  zcld  18319  elii1  18433  pi1cpbl  18542  tchcph  18667  cmetss  18740  bcth  18751  lssbn  18773  ishl2  18787  minveclem3b  18792  minveclem6  18798  pmltpc  18810  ovolfcl  18826  ovolgelb  18839  ovolunlem1  18856  ovoliunlem1  18861  ismbl  18885  ismbl2  18886  iundisj2  18906  dyadmax  18953  dyadmbllem  18954  vitalilem2  18964  mbfimaopnlem  19010  itg1climres  19069  itg2l  19084  itg2leub  19089  iblcnlem1  19142  ellimc2  19227  ellimc3  19229  limcmpt  19233  limcres  19236  elaa  19696  aaliou3lem9  19730  taylthlem2  19753  ulmcau  19772  pilem1  19827  sincosq1lem  19865  sineq0  19889  coseq1  19890  ellogrn  19917  logtayl2  20009  cxpcn3lem  20087  cxpcn3  20088  cubic  20145  atandm  20172  atandm2  20173  atandm4  20175  atans2  20227  xrlimcnp  20263  wilthlem2  20307  dvdsflsumcom  20428  dvdsmulf1o  20434  fsumvma  20452  logfac2  20456  dchrelbas2  20476  dchrelbas3  20477  lgsdir2lem4  20565  lgsquadlem1  20593  lgsquadlem2  20594  2sqlem1  20602  pntlem3  20758  ostth  20788  avril1  20836  grpoidinvlem3  20873  issubgo  20970  elghom  21030  islno  21331  nmoubi  21350  nmobndseqi  21357  siii  21431  minvecolem5  21460  minvecolem6  21461  hvsubaddi  21645  normsub0i  21714  bcsiALT  21758  hcau  21763  hlimadd  21772  hhcmpl  21779  hhcms  21782  issh2  21788  isch2  21803  hlim0  21815  isch3  21821  norm1exi  21829  elch0  21833  hhsssh2  21847  choc0  21905  pjhtheu  21973  pjpreeq  21977  omlsilem  21981  pjoc2i  22017  chsscon1i  22041  spanuni  22123  h1deoi  22128  h1dei  22129  elspansni  22137  cmcm4i  22174  cmbr3i  22179  cmbr4i  22180  osumcor2i  22223  5oalem7  22239  3oalem3  22243  pjss2i  22259  mayete3iOLD  22308  elcnop  22437  ellnop  22438  elhmop  22453  elcnfn  22462  ellnfn  22463  cnvadj  22472  nmopub  22488  nmfnleub  22505  eleigvec  22537  nmop0  22566  nmfn0  22567  nmopun  22594  lncnopbd  22617  riesz2  22646  nmopcoadj0i  22683  rnbra  22687  pjnmopi  22728  pjssdif1i  22755  pjin2i  22773  pjin3i  22774  pjclem1  22775  cvbr2  22863  cvnbtwn3  22868  cvnbtwn4  22869  mdsl2bi  22903  mdsldmd1i  22911  elat2  22920  chrelat2i  22945  atomli  22962  chirredi  22974  mdsymlem6  22988  mdsymlem8  22990  sumdmdii  22995  dmdbr5ati  23002  cdj3i  23021  xfree2  23025  ballotlemelo  23046  ballotlem2  23047  ballotlemfmpn  23053  ballotlemodife  23056  ballotlem4  23057  ballotth  23096  elxrge02  23116  or3dir  23124  difeq  23128  abeq2f  23129  rabid2f  23135  2reuswap2  23137  reuxfr3d  23138  rexunirn  23140  mo5f  23143  nmo  23144  elim2if  23152  ssiun3  23156  iuninc  23158  r19.41vv  23163  disjex  23176  disjexc  23177  rmo3f  23178  rmo4fOLD  23179  rmo4f  23180  suppss2f  23201  dfrel4  23204  abfmpunirn  23216  fmptdF  23221  mptfnf  23226  fmptcof2  23229  funcnvmptOLD  23234  funcnvmpt  23235  funcnv5mpt  23236  gtiso  23241  disjorf  23356  disjorsf  23357  iundisj2fi  23364  iundisj2f  23366  disjdsct  23369  eldiftp  23395  esumnul  23427  esumpfinvalf  23444  esumpcvgval  23446  esumcvg  23454  isrnsigaOLD  23473  isrnsiga  23474  measiuns  23544  elunirnmbfm  23558  1stmbfm  23565  2ndmbfm  23566  eldmgm  23694  subfacp1lem5  23715  subfacp1lem6  23716  cvmscld  23804  cvmlift2lem12  23845  vdgrun  23893  eupath  23905  ghomgrpilem2  23993  axextprim  24047  axrepprim  24048  axunprim  24049  axpowprim  24050  axregprim  24051  axinfprim  24052  axacprim  24053  untangtr  24060  biimpexp  24070  divelunit  24080  dftr6  24107  coep  24108  coepr  24109  dffr5  24110  dfpo2  24112  cnvco1  24117  cnvco2  24118  eldm3  24119  fundmpss  24122  dfdm5  24132  dfrn5  24133  elpotr  24137  dford5reg  24138  dfon2lem5  24143  dfon2lem6  24144  dfon2lem8  24146  dfon2lem9  24147  dfon2  24148  wfi  24207  eltrpred  24229  frind  24243  poseq  24253  soseq  24254  wfrlem4  24259  wfrlem5  24260  wfrlem9  24264  wfrlem11  24266  wfrlem12  24267  wfrlem13  24268  wfrlem14  24269  wfrlem15  24270  tfrALTlem  24276  tfr3ALT  24279  frrlem5  24285  frrlem5e  24289  frrlem11  24293  nosgnn0  24312  nodenselem5  24339  nobnddown  24355  nofulllem5  24360  elsymdif  24367  brsymdif  24372  brtxp  24420  brpprod  24425  brpprod3b  24427  brsset  24429  idsset  24430  dfon3  24432  brtxpsd  24434  brtxpsd2  24435  brbigcup  24438  elfix  24443  dffix2  24445  ellimits  24450  dffun10  24453  elfuns  24454  snelsingles  24461  dfiota3  24462  brcart  24471  brimg  24476  brapply  24477  brcup  24478  brcap  24479  brsuccf  24480  funpartfun  24481  fullfunfnv  24484  brrestrict  24487  dfrdg4  24488  tfrqfree  24489  altopthsn  24495  altopelaltxp  24510  altxpsspw  24511  mptelee  24523  brbtwn2  24533  colinearalg  24538  ax5seg  24566  axpasch  24569  axlowdimlem6  24575  axlowdimlem13  24582  axeuclidlem  24590  axeuclid  24591  axcontlem3  24594  axcontlem4  24595  axcontlem12  24603  brcolinear2  24681  broutsideof  24744  outsideofcom  24751  fvray  24764  fvline  24767  lineunray  24770  linecom  24773  linerflx2  24774  ellines  24775  bpoly2  24792  bpoly3  24793  rankeq1o  24801  elhf  24804  elhf2  24805  r19.26-2a  24934  eeeeanv  24944  altdftru  24948  pm11.53g  24964  eqvinopb  24965  copsexgb  24966  ltl4ev  24992  albineal  24999  evevifev  25014  cnvref  25065  restidsing  25076  dffn5a  25130  repcpwti  25161  dfdir2  25291  apnei  25520  ismonc  25814  isepic  25824  isfunb  25835  issubcata  25846  isntr  25873  clscnc  26010  bisig0  26062  isconcl5a  26101  isconcl5ab  26102  isibg2  26110  bosser  26167  hpd  26169  ecase13d  26222  cnvresimaOLD  26226  trer  26227  elicc3  26228  finminlem  26231  opnrebl  26235  nn0prpw  26239  clsun  26246  fneval  26287  fnessref  26293  neibastop1  26308  neifg  26320  filnetlem4  26330  f1opr  26391  inixp  26399  sdclem2  26452  sdclem1  26453  fdc  26455  neificl  26467  istotbnd3  26495  sstotbnd3  26500  isbndx  26506  isbnd3b  26509  cntotbnd  26520  heibor1lem  26533  heibor1  26534  isdrngo2  26589  isdrngo3  26590  iscrngo2  26623  smprngopr  26677  isdmn2  26680  isfldidl2  26694  ispridlc  26695  isdmn3  26699  an43OLD  26713  prtlem70  26715  prtlem100  26721  n0el  26725  prter2  26749  funsnfsup  26762  cmpfiiin  26772  isnacs2  26781  elmzpcl  26804  diophrex  26855  2sbcrex  26864  sbcrot3  26868  sbcrot5  26869  3rexfrabdioph  26878  4rexfrabdioph  26879  6rexfrabdioph  26880  7rexfrabdioph  26881  ftp  26893  fphpd  26899  fiphp3d  26902  rencldnfilem  26903  jm2.23  27089  expdiophlem1  27114  expdiophlem2  27115  expdioph  27116  dford4  27122  wopprc  27123  ttac  27129  fnwe2lem2  27148  islmodfg  27167  islnm2  27176  lnmlmic  27186  uvcvv0  27239  isnumbasgrplem1  27266  dfacbasgrp  27273  islinds2  27283  lmiclbs  27307  islnr2  27318  islnr3  27319  f1omvdco3  27392  matrcl  27466  issdrg2  27506  sdrgacs  27509  phisum  27518  isdomn3  27523  pm10.541  27562  pm10.542  27563  19.21vv  27574  19.36vv  27581  19.31vv  27582  19.37vv  27583  19.28vv  27584  pm11.6  27591  pm11.62  27593  pm14.12  27621  elnev  27638  evth2f  27686  elunif  27687  evthf  27698  stoweidlem14  27763  stoweidlem24  27773  stoweidlem31  27780  stoweidlem34  27783  stoweidlem37  27786  stoweidlem51  27800  stoweidlem54  27803  stoweidlem57  27806  stoweidlem59  27808  aiffnbandciffatnotciffb  27872  mdandyvr0  27910  mdandyvr1  27911  mdandyvr2  27912  mdandyvr3  27913  mdandyvr4  27914  mdandyvr5  27915  mdandyvr6  27916  mdandyvr7  27917  mdandyvr8  27918  mdandyvr9  27919  mdandyvr10  27920  mdandyvr11  27921  mdandyvr12  27922  mdandyvr13  27923  mdandyvr14  27924  mdandyvr15  27925  rexrsb  27947  2rexsb  27948  2rexrsb  27949  cbvral2  27950  cbvrex2  27951  2ralbiim  27952  2reu5a  27955  rmoanim  27957  2rmoswap  27962  2reu1  27964  2reu3  27966  2reu4a  27967  afvpcfv0  28009  ffnaov  28059  ndmaovass  28066  ndmaovdistr  28067  f1oun2prg  28076  mpt2xopovel  28086  nbgrasym  28152  cusgra2v  28158  uvtx01vtx  28164  frgra3v  28180  gte-lteh  28196  gt-lth  28197  sgnn  28251  onfrALTlem5  28307  onfrALTlem4  28308  onfrALTlem1  28313  2uasbanh  28327  dfvd2  28348  dfvd2an  28351  dfvd3  28360  dfvd3an  28363  eelT00  28480  eelTTT  28481  eelT12  28486  uunT1  28555  uunT1p1  28556  uun132p1  28561  un2122  28565  uunTT1p1  28569  uunTT1p2  28570  uunT11p1  28572  uunT11p2  28573  uunT12  28574  uunT12p1  28575  uunT12p2  28576  uunT12p3  28577  uunT12p4  28578  uunT12p5  28579  uun2221  28588  uun2221p1  28589  uun2221p2  28590  undif3VD  28658  onfrALTlem5VD  28661  onfrALTlem4VD  28662  onfrALTlem1VD  28666  2uasbanhVD  28687  bnj170  28723  bnj248  28725  bnj251  28727  bnj256  28731  bnj258  28733  bnj291  28736  bnj422  28740  bnj432  28741  bnj23  28744  bnj89  28747  bnj132  28752  bnj156  28756  bnj158  28757  bnj538  28769  bnj563  28772  bnj945  28805  bnj946  28806  bnj976  28809  bnj1098  28815  bnj1138  28820  bnj1209  28829  bnj1476  28879  bnj1542  28889  bnj110  28890  bnj91  28893  bnj92  28894  bnj106  28900  bnj118  28901  bnj124  28903  bnj125  28904  bnj153  28912  bnj207  28913  bnj222  28915  bnj518  28918  bnj535  28922  bnj539  28923  bnj543  28925  bnj553  28930  bnj556  28932  bnj558  28934  bnj571  28938  bnj605  28939  bnj591  28943  bnj594  28944  bnj580  28945  bnj609  28949  bnj611  28950  bnj865  28955  bnj849  28957  bnj882  28958  bnj916  28965  bnj917  28966  bnj934  28967  bnj929  28968  bnj944  28970  bnj953  28971  bnj1000  28973  bnj969  28978  bnj970  28979  bnj978  28981  bnj983  28983  bnj984  28984  bnj985  28985  bnj986  28986  bnj1021  28996  bnj1033  28999  bnj1049  29004  bnj1052  29005  bnj1083  29008  bnj1112  29013  bnj1030  29017  bnj1137  29025  bnj1189  29039  bnj1204  29042  bnj1253  29047  bnj1279  29048  bnj1373  29060  bnj1388  29063  bnj1398  29064  bnj1450  29080  equvelv  29116  a12study4  29117  a12study8  29119  a12peros  29121  a12lem2  29131  a12study10  29136  a12study10n  29137  lsateln0  29185  islshpat  29207  lcvbr2  29212  lcvbr3  29213  lcvnbtwn3  29218  islfl  29250  lshpsmreu  29299  lub0N  29379  glb0N  29383  cvrnbtwn3  29466  leat2  29484  isat3  29497  iscvlat2N  29514  ishlat2  29543  ishlat3N  29544  hlrelat5N  29590  hlrelat2  29592  3dim0  29646  2dim  29659  islpln5  29724  islvol5  29768  4atlem3  29785  dalem20  29882  ispsubsp2  29935  snatpsubN  29939  pmapglb  29959  elpadd  29988  paddasslem17  30025  dalawlem13  30072  pclfinN  30089  polval2N  30095  pclfinclN  30139  lhpex2leN  30202  isltrn2N  30309  cdleme0nex  30479  cdleme22b  30530  cdlemftr3  30754  tendoset  30948  diarnN  31319  dibopelvalN  31333  dibopelval2  31335  dibelval3  31337  diblsmopel  31361  dicelval3  31370  dihglb2  31532  doch11  31563  islpolN  31673  lcfls1N  31725  mapdval4N  31822  mapdrvallem2  31835
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