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  1561  alinexa  1567  alexn  1568  exanali  1574  19.26-2  1583  19.26-3an  1584  albiim  1600  2albiim  1601  ax12bOLD  1658  alrot3  1714  alrot4  1715  19.21-2  1794  nf2  1800  19.27  1807  19.28  1808  19.36  1809  19.37  1811  19.44  1815  19.45  1816  exrot3  1820  exrot4  1821  aaan  1827  eeor  1828  19.23vv  1835  pm11.53  1836  19.41vv  1845  19.41vvv  1846  19.41vvvv  1847  19.42vv  1850  19.42vvv  1851  4exdistr  1854  eean  1855  cbvex4v  1954  sbor  2008  sbrim  2009  sblim  2010  sban  2011  sbbi  2013  sblbis  2014  sbrbis  2015  sbrbif  2016  sbid2  2026  sbco2d  2029  sb8e  2035  sbnf2  2049  2sb5  2053  2sb6  2054  sbcom2  2055  sb6a  2057  2sb5rf  2058  2sb6rf  2059  sbex  2069  sbalv  2070  exsbOLD  2072  2exsb  2073  eujust  2147  euf  2151  cbveu  2165  eu2  2170  mo2  2174  sbmo  2175  mo3  2176  mo4f  2177  eu4  2184  moanim  2201  2mo  2223  2mos  2224  2eu1  2225  2eu3  2227  2eu4  2228  2eu6  2230  exists1  2234  abid  2273  eleq12i  2350  abeq2  2390  abeq2i  2392  clabel  2406  abid2f  2446  sbabel  2447  neeq12i  2460  necon1abii  2499  neanior  2533  ralnex  2555  rexnal  2556  ralinexa  2590  rexanali  2591  r3al  2602  r19.26-2  2678  ralbiim  2682  r19.30  2687  ralcomf  2700  rexcomf  2701  rexrot4  2705  reean  2708  3reeanv  2710  rabbi  2720  cbvralf  2760  cbvreu  2764  cbvral2v  2774  cbvrex2v  2775  cbvral3v  2776  cbvralsv  2777  cbvrexsv  2778  sbralie  2779  rabeq2i  2787  issetf  2795  2gencl  2819  3gencl  2820  ceqsex2  2826  ceqsex3v  2828  ceqsex6v  2830  ceqsex8v  2831  gencbvex  2832  spc3gv  2875  eqvincf  2898  ceqsrex2v  2905  elrab2  2927  ralab  2928  ralrab  2929  rexab  2930  rexrab  2931  ralab2  2932  rexab2  2934  eueq3  2942  morex  2951  euxfr2  2952  euxfr  2953  euind  2954  reu2  2955  reu6  2956  rmo4  2960  reu4  2961  reu7  2962  rmoim  2966  2reuswap  2969  reuind  2970  2reu5lem1  2972  2reu5lem2  2973  2reu5  2975  sbcco  3015  sbccomlem  3063  sbccom  3064  ra5  3077  rmo3  3080  csbco  3092  sbnfc2  3143  csbabg  3144  cbvralcsf  3145  cbvreucsf  3147  dfss  3169  dfss2f  3173  ss2ab  3243  dfpss2  3263  dfpss3  3264  psseq12i  3269  sspsstri  3280  difeqri  3298  uneqri  3319  ssequn2  3350  unss  3351  rexun  3357  ralunb  3358  elin2  3361  ineqri  3364  dfss1  3375  dfss5  3376  nsspssun  3404  indifdir  3427  inrab2  3443  rabun2  3449  reuun2  3453  eq0  3471  0el  3473  abn0  3475  0pss  3494  disjr  3498  disj1  3499  disjpss  3507  undif4  3513  difin0ss  3522  inssdif0  3523  uneqdifeq  3544  r19.3rz  3547  r19.3rzv  3549  ralidm  3559  pwss  3641  dfpr2  3658  ralsns  3672  rexsns  3673  eltpg  3678  ralprg  3684  rexprg  3685  raltpg  3686  rextpg  3687  euabsn2  3700  eusn  3705  eldifsn  3751  rexdifsn  3755  difsnpss  3760  pwpw0  3765  ssunsn  3776  eqsn  3777  sstp  3780  tpss  3781  prel12  3791  preqsn  3794  pwsnALT  3824  pwtp  3826  eluniab  3841  elunirab  3842  unipr  3843  dfnfc2  3847  uniun  3848  uniin  3849  unissb  3859  elintab  3875  elintrab  3876  ssintab  3881  ssintrab  3887  intun  3896  intpr  3897  elrint  3905  iuncom4  3914  iuneq2  3923  dfiun2g  3937  ssiinf  3953  elriin  3976  iunxiun  3986  pwssb  3990  iunpwss  3993  dfdisj2  3997  nfdisj  4007  disjor  4009  disjors  4011  invdisj  4014  disjiun  4015  disjxiun  4022  disjxun  4023  cbvopab1  4091  dftr5  4118  trint  4130  inex1  4157  inuni  4175  axpweq  4189  nfnid  4206  zfpair2  4217  moabex  4234  exss  4238  elop  4241  otth  4252  copsex4g  4257  opeqsn  4264  opthwiener  4270  opelopabsbOLD  4275  brabga  4281  opelopabaf  4290  opabn0  4297  iunopab  4298  pwunss  4300  pwundifOLD  4303  dfid3  4312  pocl  4323  sotric  4342  isso2i  4348  somo  4350  frminex  4375  dfepfr  4380  wefrc  4389  ordtri3or  4426  ordtri2  4429  elsuci  4460  elsucg  4461  sucel  4467  on0eqel  4512  uniuni  4529  reusv2lem4  4540  reusv2lem5  4541  reusv2  4542  reusv3  4544  reuxfr2d  4559  elpwun  4569  iunpw  4572  dfwe2  4575  onintrab2  4595  ordpwsuc  4608  ordzsl  4638  dflim4  4641  tfindsg  4653  tfindes  4655  findsg  4685  elxp  4708  opelxp  4721  brxp  4722  rabxp  4727  opthprc  4738  brab2a  4740  opeliunxp  4742  xpundi  4743  xpundir  4744  elvvv  4751  brinxp  4754  brab2ga  4765  xp0r  4770  eqrelrel  4790  reliun  4808  reluni  4810  raliunxp  4827  rexiunxp  4828  ralxpf  4832  rexxpf  4833  iunxpf  4834  relop  4836  elcnv  4860  elcnv2  4861  dmin  4888  dmuni  4890  dmopab  4891  dmi  4895  rnopab  4926  elrnmpt1  4930  rncoeq  4950  resiexg  4999  dfima2  5016  dfima3  5017  elima2  5020  elima3  5021  imai  5029  elimasn  5040  epini  5045  dfse2  5048  cotr  5057  issref  5058  intasym  5060  asymref  5061  asymref2  5062  somin1  5081  cnvopab  5085  cnvi  5087  cnvdif  5089  imainss  5098  dfrel2  5126  dfrel3  5133  rnsnn0  5141  relsn2  5145  dmsnopg  5146  cnvcnvsn  5152  elxp4  5162  elxp5  5163  cnvresima  5164  mptpreima  5168  dfco2  5174  coundi  5176  coundir  5177  imaco  5180  coiun  5184  coi1  5190  relssdmrn  5195  relrelss  5198  ressn  5213  cnviin  5214  cnvpo  5215  cbviota  5226  dffun2  5267  dffun3  5268  dffun4  5269  dffun5  5270  dffun7  5282  dffun8  5283  dffun9  5284  funopab  5289  funun  5298  funcnvsn  5299  funcnv2  5311  funcnv  5312  fun2cnv  5314  fncnv  5316  fun11  5317  fununi  5318  imadif  5329  funimaexg  5331  fnunsn  5353  fnres  5362  fnopabg  5369  mptfng  5371  mptun  5376  fun  5407  fresaunres1  5416  fcnvres  5420  dff12  5438  f1cnvcnv  5447  funforn  5460  dff1o2  5479  dff1o5  5483  f1orn  5484  resdif  5496  ffoss  5507  f11o  5508  f1o00  5510  fo00  5511  brprcneu  5520  elfv  5525  fv3  5543  dffn5f  5579  dffv2  5594  eqfnfv3  5626  fndmdifeq0  5633  fneqeql  5635  unpreima  5653  respreima  5656  dff4  5676  dffo3  5677  dffo5  5679  f1ompt  5684  ffnfvf  5688  fmptco  5693  fsn2  5700  fconst3  5737  fconst4  5738  idref  5761  abrexco  5768  opabex3  5771  abexssex  5783  dff13  5785  dff13f  5786  f1mpt  5787  foeqcnvco  5806  isocnv3  5831  isoini  5837  weniso  5854  oprabid  5884  dfoprab2  5897  eqoprab2b  5908  dmoprab  5930  rnoprab  5932  eloprabga  5936  mpt2mptx  5940  resoprab  5942  ffnov  5950  fnov  5954  elrnmpt2  5959  ralrnmpt2  5960  rexrnmpt2  5961  oprabex3  5964  oprabrexex2  5965  ovid  5966  ov3  5986  ov6g  5987  foov  5996  ndmovdistr  6011  difxp  6155  elopaba  6184  fmpt2  6193  curry1  6212  curry2  6215  fsplit  6225  frxp  6227  xporderlem  6228  soxp  6230  brtpos2  6242  dmtpos  6248  tpostpos  6256  tpossym  6268  tposoprab  6272  sorpsscmpl  6290  opiota  6292  eusvobj2  6339  dfsmo2  6366  tfrlem3  6395  tfrlem7  6401  tfrlem9  6403  tfrlem9a  6404  tz7.48lem  6455  tz7.49c  6460  el1o  6500  dif1o  6501  ondif2  6503  brwitnlem  6508  oarec  6562  omeulem1  6582  omeu  6585  oeordi  6587  oeeui  6602  oeeu  6603  omopthlem1  6655  dfer2  6663  brdifun  6689  swoso  6693  eqerlem  6694  qsid  6727  iiner  6733  erinxp  6735  brecop  6753  eroveu  6755  erovlem  6756  ecopovsym  6762  mapval2  6799  mapsn  6811  elixp  6825  ixpeq2  6832  ixpin  6843  ixpiin  6844  mptelixpg  6855  ixpsnf1o  6858  boxriin  6860  domen  6877  isfi  6887  en1  6930  xpsnen  6948  xpcomco  6954  xpassen  6958  sbthlem9  6981  0sdomg  6992  2pwuninel  7018  ssenen  7037  nneneq  7046  php  7047  modom2  7066  ac6sfi  7103  frfi  7104  fimaxg  7106  elfpw  7159  fissuni  7162  dffi3  7186  marypha1lem  7188  marypha2lem2  7191  dfsup2  7197  dfsup2OLD  7198  wofib  7262  wemapso2lem  7267  wdom2d  7296  unxpwdom2  7304  dford2  7323  inf2  7326  inf3lem2  7332  axinf2  7343  zfinf2  7345  cantnfp1lem2  7383  oemapso  7386  cantnflem1  7393  trcl  7412  epfrs  7415  rankvalb  7471  r1elss  7480  unbndrank  7516  scott0s  7560  cplem1  7561  bnd2  7565  isnum2  7580  iscard2  7611  infxpenlem  7643  fseqenlem1  7653  acnnum  7681  infpwfien  7691  alephnbtwn2  7701  alephord2  7705  alephislim  7712  cardaleph  7718  alephval3  7739  aceq1  7746  aceq2  7748  dfac3  7750  dfac4  7751  dfac5lem1  7752  dfac5lem2  7753  dfac5lem3  7754  dfac5lem4  7755  dfac5lem5  7756  dfac2  7759  dfac0  7761  dfac1  7762  dfac8  7763  dfac9  7764  dfac12  7777  kmlem3  7780  kmlem4  7781  kmlem7  7784  kmlem8  7785  kmlem9  7786  kmlem13  7790  kmlem14  7791  kmlem15  7792  dfackm  7794  pwsdompw  7832  ackbij2lem2  7868  cf0  7879  cfval2  7888  cflim2  7891  cfss  7893  cfslb  7894  isfin3  7924  isfin5  7927  isfin6  7928  sdom2en01  7930  fin23lem25  7952  fin23lem26  7953  fin23lem40  7979  isfin1-2  8013  isfin1-3  8014  fin1a2lem5  8032  fin1a2lem6  8033  fin1a2lem12  8039  fin12  8041  domtriomlem  8070  axdc2lem  8076  axdc3lem2  8079  axdc3lem4  8081  axcclem  8085  ac6num  8108  ac9  8112  ac6n  8114  ac9s  8122  zorn2lem6  8130  zornn0g  8134  ttukeylem6  8143  ttukey2g  8145  brdom7disj  8158  brdom6disj  8159  iunfo  8163  iundom2g  8164  konigthlem  8192  alephsuc3  8204  elgch  8246  fpwwe2lem9  8262  fpwwe2lem12  8265  fpwwe2lem13  8266  fpwwe2  8267  canth4  8271  canthwe  8275  wunex2  8362  uniwun  8364  axgroth5  8448  grothpw  8450  axgroth6  8452  grothprimlem  8457  grothprim  8458  elni  8502  ltexpi  8528  nqerf  8556  nqerid  8559  ordpipq  8568  recmulnq  8590  npomex  8622  genpnnp  8631  genpass  8635  addcompr  8647  mulcompr  8649  reclem2pr  8674  reclem3pr  8675  ltsosr  8718  ltasr  8724  mappsrpr  8732  map2psrpr  8734  opelcn  8753  elreal  8755  elreal2  8756  axaddf  8769  axmulf  8770  axicn  8774  axrrecex  8787  axpre-mulgt0  8792  xrlenlt  8892  ssxr  8894  leloe  8910  msq0i  9417  infm3  9715  supmullem2  9723  inelr  9738  arch  9964  elnnne0  9981  un0addcl  9999  un0mulcl  10000  elnnz  10036  elznn0nn  10039  elznn0  10040  elznn  10041  elz2  10042  raluz2  10270  rexuz2  10272  nnwos  10288  eluz2b2  10292  eluz2b3  10293  ublbneg  10304  zmin  10314  elq  10320  ralrp  10374  rexrp  10375  ltxr  10459  xrnemnf  10462  xrleloe  10480  xrltlen  10482  xrrebnd  10499  xaddf  10553  xmullem  10586  xmullem2  10587  xrsupss  10629  xrinfmss  10630  elfzp1  10838  fzprval  10846  fztpval  10847  fzm1  10864  fzolb  10882  fzolb2  10883  elfzo3  10892  fzouzsplit  10903  fzo0n0  10907  fzind2  10925  uzrdgfni  11023  subsq0i  11218  crreczi  11228  nn0le2msqi  11284  nn0opth2i  11288  hashkf  11341  hashfun  11391  hashbclem  11392  hashbc  11393  hashf1lem2  11396  leiso  11399  iswrd  11417  climeu  12031  lo1resb  12040  rlimresb  12041  o1resb  12042  climmpt2  12049  fsum2dlem  12235  rpnnen2  12506  sqr2irr  12529  divides  12535  odd2np1  12589  divalglem1  12595  divalglem6  12599  divalglem10  12603  divalgb  12605  bitsval2  12618  bitsmod  12629  bitscmp  12631  smueqlem  12683  isprm2  12768  isprm3  12769  isprm4  12770  isprm5  12793  pythagtriplem19  12888  pythagtrip  12889  pceu  12901  prmreclem2  12966  4sqlem2  12998  4sqlem12  13005  vdwpc  13029  vdwnn  13047  dec5dvds2  13082  pwsle  13393  imasleval  13445  xpsfrnel  13467  xpsfrnel2  13469  xpsle  13485  isacs2  13557  mreacs  13562  iscatd2  13585  comfeq  13611  oppcsect  13678  isssc  13699  isfunc  13740  funcoppc  13751  isffth2  13792  fucinv  13849  elhoma  13866  setcinv  13924  ispos  14083  ispos2  14084  tosso  14144  istsr2  14329  spwmo  14337  ismnd  14371  mndcl  14374  issubm  14427  gsumwspan  14470  issubg  14623  isnsg2  14649  eqger  14669  isgim2  14731  giclcl  14738  gicrcl  14739  gicsubgen  14744  gaorber  14764  resscntz  14809  cntzrec  14811  efgval2  15035  efgsfo  15050  efgrelexlemb  15061  isabl2  15099  iscyggen2  15170  iscyg2  15171  iscyg3  15175  lt6abl  15183  gsumval3eu  15192  gsum2d2  15227  dmdprdd  15239  subgdmdprd  15271  iscrng2  15358  dvdsrtr  15436  isunit  15441  isnirred  15484  isirred2  15485  isrhm  15503  isdrng2  15524  drngprop  15525  isabv  15586  issrng  15617  islmod  15633  islss  15694  lss1d  15722  islmim2  15821  lmiclcl  15825  lmicrcl  15826  lsmelval2  15840  lspsolvlem  15897  lspsncv0  15901  islpidl  16000  islpir2  16005  isnzr2  16017  isdomn2  16042  fiidomfld  16051  aspval2  16088  mplcoe1  16211  mplcoe2  16213  evlslem4  16247  xrsdsreclb  16420  unocv  16582  iunocv  16583  ishil2  16621  isobs  16622  obselocv  16630  iinopn  16650  istps4OLD  16663  istps5OLD  16664  istps  16676  istps2  16677  isbasis2g  16688  tgval2  16696  elcls  16812  islpi  16882  isperf2  16885  isperf3  16886  restntr  16914  ordtbaslem  16920  ordtrest2lem  16935  cnrest  17015  ist0-3  17075  ist1-2  17077  ist1-3  17079  nrmsep3  17085  isnrm2  17088  perfcls  17095  ordthaus  17114  cmpcov2  17119  cmpsub  17129  hauscmplem  17135  cmpfi  17137  iscon2  17142  dfcon2  17147  is1stc2  17170  is2ndc  17174  1stcelcls  17189  1stccn  17191  llyi  17202  subislly  17209  iskgen3  17246  txuni2  17262  ptpjpre1  17268  ptbasin  17274  tx1cn  17305  tx2cn  17306  uptx  17321  txdis1cn  17331  ptrescn  17335  txtube  17336  txcmplem1  17337  hausdiag  17341  txkgen  17348  xkohaus  17349  xkococnlem  17355  xkoinjcn  17383  qtopeu  17409  isr0  17430  regr1lem2  17433  hmphsym  17475  elmptrab2  17525  isfbas  17526  isfbas2  17532  trfbas  17541  snfil  17561  fbunfip  17566  elfg  17568  fgcl  17575  fbasrn  17581  filuni  17582  trfil2  17584  cfinfil  17590  csdfil  17591  supfil  17592  ufinffr  17626  rnelfmlem  17649  elflim2  17661  hausflim  17678  hauspwpwf1  17684  txflf  17703  isfcls2  17710  fclsopn  17711  fclsrest  17721  alexsubALTlem2  17744  alexsubALTlem3  17745  alexsubALTlem4  17746  tmdcn2  17774  divstgplem  17805  divstgphaus  17807  tsmssubm  17827  istdrg2  17862  metn0  17926  prdsxmetlem  17934  imasdsf1olem  17939  xpsdsval  17947  blres  17979  xmeterval  17980  xmeter  17981  isxms2  17996  isms2  17998  dscopn  18098  isngp3  18122  isnvc2  18211  isnghm  18234  qtopbaslem  18269  xrtgioo  18314  zcld  18321  elii1  18435  pi1cpbl  18544  tchcph  18669  cmetss  18742  bcth  18753  lssbn  18775  ishl2  18789  minveclem3b  18794  minveclem6  18800  pmltpc  18812  ovolfcl  18828  ovolgelb  18841  ovolunlem1  18858  ovoliunlem1  18863  ismbl  18887  ismbl2  18888  iundisj2  18908  dyadmax  18955  dyadmbllem  18956  vitalilem2  18966  mbfimaopnlem  19012  itg1climres  19071  itg2l  19086  itg2leub  19091  iblcnlem1  19144  ellimc2  19229  ellimc3  19231  limcmpt  19235  limcres  19238  elaa  19698  aaliou3lem9  19732  taylthlem2  19755  ulmcau  19774  pilem1  19829  sincosq1lem  19867  sineq0  19891  coseq1  19892  ellogrn  19919  logtayl2  20011  cxpcn3lem  20089  cxpcn3  20090  cubic  20147  atandm  20174  atandm2  20175  atandm4  20177  atans2  20229  xrlimcnp  20265  wilthlem2  20309  dvdsflsumcom  20430  dvdsmulf1o  20436  fsumvma  20454  logfac2  20458  dchrelbas2  20478  dchrelbas3  20479  lgsdir2lem4  20567  lgsquadlem1  20595  lgsquadlem2  20596  2sqlem1  20604  pntlem3  20760  ostth  20790  avril1  20838  grpoidinvlem3  20875  issubgo  20972  elghom  21032  islno  21333  nmoubi  21352  nmobndseqi  21359  siii  21433  minvecolem5  21462  minvecolem6  21463  hvsubaddi  21647  normsub0i  21716  bcsiALT  21760  hcau  21765  hlimadd  21774  hhcmpl  21781  hhcms  21784  issh2  21790  isch2  21805  hlim0  21817  isch3  21823  norm1exi  21831  elch0  21835  hhsssh2  21849  choc0  21907  pjhtheu  21975  pjpreeq  21979  omlsilem  21983  pjoc2i  22019  chsscon1i  22043  spanuni  22125  h1deoi  22130  h1dei  22131  elspansni  22139  cmcm4i  22176  cmbr3i  22181  cmbr4i  22182  osumcor2i  22225  5oalem7  22241  3oalem3  22245  pjss2i  22261  mayete3iOLD  22310  elcnop  22439  ellnop  22440  elhmop  22455  elcnfn  22464  ellnfn  22465  cnvadj  22474  nmopub  22490  nmfnleub  22507  eleigvec  22539  nmop0  22568  nmfn0  22569  nmopun  22596  lncnopbd  22619  riesz2  22648  nmopcoadj0i  22685  rnbra  22689  pjnmopi  22730  pjssdif1i  22757  pjin2i  22775  pjin3i  22776  pjclem1  22777  cvbr2  22865  cvnbtwn3  22870  cvnbtwn4  22871  mdsl2bi  22905  mdsldmd1i  22913  elat2  22922  chrelat2i  22947  atomli  22964  chirredi  22976  mdsymlem6  22990  mdsymlem8  22992  sumdmdii  22997  dmdbr5ati  23004  cdj3i  23023  xfree2  23027  ballotlemelo  23048  ballotlem2  23049  ballotlemfmpn  23055  ballotlemodife  23058  ballotlem4  23059  ballotth  23098  elxrge02  23118  or3dir  23126  difeq  23130  abeq2f  23131  rabid2f  23137  2reuswap2  23139  reuxfr3d  23140  rexunirn  23142  mo5f  23145  nmo  23146  elim2if  23154  ssiun3  23158  iuninc  23160  r19.41vv  23165  disjex  23178  disjexc  23179  rmo3f  23180  rmo4fOLD  23181  rmo4f  23182  suppss2f  23203  dfrel4  23206  abfmpunirn  23218  fmptdF  23223  mptfnf  23228  fmptcof2  23231  funcnvmptOLD  23236  funcnvmpt  23237  funcnv5mpt  23238  gtiso  23243  disjorf  23358  disjorsf  23359  iundisj2fi  23366  iundisj2f  23368  disjdsct  23371  eldiftp  23397  esumnul  23429  esumpfinvalf  23446  esumpcvgval  23448  esumcvg  23456  isrnsigaOLD  23475  isrnsiga  23476  measiuns  23546  elunirnmbfm  23560  1stmbfm  23567  2ndmbfm  23568  eldmgm  23696  subfacp1lem5  23717  subfacp1lem6  23718  cvmscld  23806  cvmlift2lem12  23847  vdgrun  23895  eupath  23907  ghomgrpilem2  23995  axextprim  24049  axrepprim  24050  axunprim  24051  axpowprim  24052  axregprim  24053  axinfprim  24054  axacprim  24055  untangtr  24062  biimpexp  24072  divelunit  24082  dftr6  24109  coep  24110  coepr  24111  dffr5  24112  dfpo2  24114  cnvco1  24119  cnvco2  24120  eldm3  24121  fundmpss  24124  dfdm5  24134  dfrn5  24135  elpotr  24139  dford5reg  24140  dfon2lem5  24145  dfon2lem6  24146  dfon2lem8  24148  dfon2lem9  24149  dfon2  24150  wfi  24209  eltrpred  24231  frind  24245  poseq  24255  soseq  24256  wfrlem4  24261  wfrlem5  24262  wfrlem9  24266  wfrlem11  24268  wfrlem12  24269  wfrlem13  24270  wfrlem14  24271  wfrlem15  24272  tfrALTlem  24278  tfr3ALT  24281  frrlem5  24287  frrlem5e  24291  frrlem11  24295  nosgnn0  24314  nodenselem5  24341  nobnddown  24357  nofulllem5  24362  elsymdif  24369  brsymdif  24374  brtxp  24422  brpprod  24427  brpprod3b  24429  brsset  24431  idsset  24432  dfon3  24434  brtxpsd  24436  brtxpsd2  24437  brbigcup  24440  elfix  24445  dffix2  24447  ellimits  24452  dffun10  24455  elfuns  24456  snelsingles  24463  dfiota3  24464  brcart  24473  brimg  24478  brapply  24479  brcup  24480  brcap  24481  brsuccf  24482  funpartfun  24483  fullfunfnv  24486  brrestrict  24489  dfrdg4  24490  tfrqfree  24491  altopthsn  24497  altopelaltxp  24512  altxpsspw  24513  mptelee  24525  brbtwn2  24535  colinearalg  24540  ax5seg  24568  axpasch  24571  axlowdimlem6  24577  axlowdimlem13  24584  axeuclidlem  24592  axeuclid  24593  axcontlem3  24596  axcontlem4  24597  axcontlem12  24605  brcolinear2  24683  broutsideof  24746  outsideofcom  24753  fvray  24766  fvline  24769  lineunray  24772  linecom  24775  linerflx2  24776  ellines  24777  bpoly2  24794  bpoly3  24795  rankeq1o  24803  elhf  24806  elhf2  24807  supadd  24928  itg2addnclem2  24934  itg2addnc  24935  r19.26-2a  24945  eeeeanv  24955  altdftru  24959  pm11.53g  24975  eqvinopb  24976  copsexgb  24977  ltl4ev  25003  albineal  25010  evevifev  25025  cnvref  25076  restidsing  25087  dffn5a  25141  repcpwti  25172  dfdir2  25302  apnei  25531  ismonc  25825  isepic  25835  isfunb  25846  issubcata  25857  isntr  25884  clscnc  26021  bisig0  26073  isconcl5a  26112  isconcl5ab  26113  isibg2  26121  bosser  26178  hpd  26180  ecase13d  26233  cnvresimaOLD  26237  trer  26238  elicc3  26239  finminlem  26242  opnrebl  26246  nn0prpw  26250  clsun  26257  fneval  26298  fnessref  26304  neibastop1  26319  neifg  26331  filnetlem4  26341  f1opr  26402  inixp  26410  sdclem2  26463  sdclem1  26464  fdc  26466  neificl  26478  istotbnd3  26506  sstotbnd3  26511  isbndx  26517  isbnd3b  26520  cntotbnd  26531  heibor1lem  26544  heibor1  26545  isdrngo2  26600  isdrngo3  26601  iscrngo2  26634  smprngopr  26688  isdmn2  26691  isfldidl2  26705  ispridlc  26706  isdmn3  26710  an43OLD  26724  prtlem70  26726  prtlem100  26732  n0el  26736  prter2  26760  funsnfsup  26773  cmpfiiin  26783  isnacs2  26792  elmzpcl  26815  diophrex  26866  2sbcrex  26875  sbcrot3  26879  sbcrot5  26880  3rexfrabdioph  26889  4rexfrabdioph  26890  6rexfrabdioph  26891  7rexfrabdioph  26892  ftp  26904  fphpd  26910  fiphp3d  26913  rencldnfilem  26914  jm2.23  27100  expdiophlem1  27125  expdiophlem2  27126  expdioph  27127  dford4  27133  wopprc  27134  ttac  27140  fnwe2lem2  27159  islmodfg  27178  islnm2  27187  lnmlmic  27197  uvcvv0  27250  isnumbasgrplem1  27277  dfacbasgrp  27284  islinds2  27294  lmiclbs  27318  islnr2  27329  islnr3  27330  f1omvdco3  27403  matrcl  27477  issdrg2  27517  sdrgacs  27520  phisum  27529  isdomn3  27534  pm10.541  27573  pm10.542  27574  19.21vv  27585  19.36vv  27592  19.31vv  27593  19.37vv  27594  19.28vv  27595  pm11.6  27602  pm11.62  27604  pm14.12  27632  elnev  27649  evth2f  27697  elunif  27698  evthf  27709  stoweidlem14  27774  stoweidlem24  27784  stoweidlem31  27791  stoweidlem34  27794  stoweidlem37  27797  stoweidlem51  27811  stoweidlem54  27814  stoweidlem57  27817  stoweidlem59  27819  aiffnbandciffatnotciffb  27883  mdandyvr0  27921  mdandyvr1  27922  mdandyvr2  27923  mdandyvr3  27924  mdandyvr4  27925  mdandyvr5  27926  mdandyvr6  27927  mdandyvr7  27928  mdandyvr8  27929  mdandyvr9  27930  mdandyvr10  27931  mdandyvr11  27932  mdandyvr12  27933  mdandyvr13  27934  mdandyvr14  27935  mdandyvr15  27936  rexrsb  27958  2rexsb  27959  2rexrsb  27960  cbvral2  27961  cbvrex2  27962  2ralbiim  27963  2reu5a  27966  rmoanim  27968  2rmoswap  27973  2reu1  27975  2reu3  27977  2reu4a  27978  afvpcfv0  28020  ffnaov  28070  ndmaovass  28077  ndmaovdistr  28078  f1oun2prg  28087  mpt2xopovel  28097  nbgrasym  28163  cusgra2v  28169  uvtx01vtx  28175  frgra3v  28191  gte-lteh  28207  gt-lth  28208  sgnn  28262  onfrALTlem5  28363  onfrALTlem4  28364  onfrALTlem1  28369  2uasbanh  28383  dfvd2  28404  dfvd2an  28407  dfvd3  28416  dfvd3an  28419  eelT00  28542  eelTTT  28543  eelT12  28549  uunT1  28626  uunT1p1  28627  uun132p1  28632  un2122  28636  uunTT1p1  28640  uunTT1p2  28641  uunT11p1  28643  uunT11p2  28644  uunT12  28645  uunT12p1  28646  uunT12p2  28647  uunT12p3  28648  uunT12p4  28649  uunT12p5  28650  uun2221  28659  uun2221p1  28660  uun2221p2  28661  undif3VD  28731  onfrALTlem5VD  28734  onfrALTlem4VD  28735  onfrALTlem1VD  28739  2uasbanhVD  28760  bnj170  28796  bnj248  28798  bnj251  28800  bnj256  28804  bnj258  28806  bnj291  28809  bnj422  28813  bnj432  28814  bnj23  28817  bnj89  28820  bnj132  28825  bnj156  28829  bnj158  28830  bnj538  28842  bnj563  28845  bnj945  28878  bnj946  28879  bnj976  28882  bnj1098  28888  bnj1138  28893  bnj1209  28902  bnj1476  28952  bnj1542  28962  bnj110  28963  bnj91  28966  bnj92  28967  bnj106  28973  bnj118  28974  bnj124  28976  bnj125  28977  bnj153  28985  bnj207  28986  bnj222  28988  bnj518  28991  bnj535  28995  bnj539  28996  bnj543  28998  bnj553  29003  bnj556  29005  bnj558  29007  bnj571  29011  bnj605  29012  bnj591  29016  bnj594  29017  bnj580  29018  bnj609  29022  bnj611  29023  bnj865  29028  bnj849  29030  bnj882  29031  bnj916  29038  bnj917  29039  bnj934  29040  bnj929  29041  bnj944  29043  bnj953  29044  bnj1000  29046  bnj969  29051  bnj970  29052  bnj978  29054  bnj983  29056  bnj984  29057  bnj985  29058  bnj986  29059  bnj1021  29069  bnj1033  29072  bnj1049  29077  bnj1052  29078  bnj1083  29081  bnj1112  29086  bnj1030  29090  bnj1137  29098  bnj1189  29112  bnj1204  29115  bnj1253  29120  bnj1279  29121  bnj1373  29133  bnj1388  29136  bnj1398  29137  bnj1450  29153  equvelv  29189  a12study4  29190  a12study8  29192  a12peros  29194  a12lem2  29204  a12study10  29209  a12study10n  29210  lsateln0  29258  islshpat  29280  lcvbr2  29285  lcvbr3  29286  lcvnbtwn3  29291  islfl  29323  lshpsmreu  29372  lub0N  29452  glb0N  29456  cvrnbtwn3  29539  leat2  29557  isat3  29570  iscvlat2N  29587  ishlat2  29616  ishlat3N  29617  hlrelat5N  29663  hlrelat2  29665  3dim0  29719  2dim  29732  islpln5  29797  islvol5  29841  4atlem3  29858  dalem20  29955  ispsubsp2  30008  snatpsubN  30012  pmapglb  30032  elpadd  30061  paddasslem17  30098  dalawlem13  30145  pclfinN  30162  polval2N  30168  pclfinclN  30212  lhpex2leN  30275  isltrn2N  30382  cdleme0nex  30552  cdleme22b  30603  cdlemftr3  30827  tendoset  31021  diarnN  31392  dibopelvalN  31406  dibopelval2  31408  dibelval3  31410  diblsmopel  31434  dicelval3  31443  dihglb2  31605  doch11  31636  islpolN  31746  lcfls1N  31798  mapdval4N  31895  mapdrvallem2  31908
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