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  1657  alrot3  1713  alrot4  1714  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  1957  sbor  2005  sbrim  2006  sblim  2007  sban  2008  sbbi  2010  sblbis  2011  sbrbis  2012  sbrbif  2013  sbid2  2023  sbco2d  2026  sb8e  2032  sbnf2  2047  2sb5  2054  2sb6  2055  sbcom2  2056  sb6a  2058  2sb5rf  2059  2sb6rf  2060  sbex  2070  sbalv  2071  exsbOLD  2073  2exsb  2074  eujust  2146  euf  2150  cbveu  2164  eu2  2169  mo2  2173  sbmo  2174  mo3  2175  mo4f  2176  eu4  2183  moanim  2200  2mo  2222  2mos  2223  2eu1  2224  2eu3  2226  2eu4  2227  2eu6  2229  exists1  2233  abid  2272  eleq12i  2349  abeq2  2389  abeq2i  2391  clabel  2405  abid2f  2445  sbabel  2446  neeq12i  2459  necon1abii  2498  neanior  2532  ralnex  2554  rexnal  2555  ralinexa  2589  rexanali  2590  r3al  2601  r19.26-2  2677  ralbiim  2681  r19.30  2686  ralcomf  2699  rexcomf  2700  rexrot4  2704  reean  2707  3reeanv  2709  rabbi  2719  cbvralf  2759  cbvreu  2763  cbvral2v  2773  cbvrex2v  2774  cbvral3v  2775  cbvralsv  2776  cbvrexsv  2777  sbralie  2778  rabeq2i  2786  issetf  2794  2gencl  2818  3gencl  2819  ceqsex2  2825  ceqsex3v  2827  ceqsex6v  2829  ceqsex8v  2830  gencbvex  2831  spc3gv  2874  eqvincf  2897  ceqsrex2v  2904  elrab2  2926  ralab  2927  ralrab  2928  rexab  2929  rexrab  2930  ralab2  2931  rexab2  2933  eueq3  2941  morex  2950  euxfr2  2951  euxfr  2952  euind  2953  reu2  2954  reu6  2955  rmo4  2959  reu4  2960  reu7  2961  rmoim  2965  2reuswap  2968  reuind  2969  2reu5lem1  2971  2reu5lem2  2972  2reu5  2974  sbcco  3014  sbccomlem  3062  sbccom  3063  ra5  3076  rmo3  3079  csbco  3091  sbnfc2  3142  csbabg  3143  cbvralcsf  3144  cbvreucsf  3146  dfss  3168  dfss2f  3172  ss2ab  3242  dfpss2  3262  dfpss3  3263  psseq12i  3268  sspsstri  3279  difeqri  3297  uneqri  3318  ssequn2  3349  unss  3350  rexun  3356  ralunb  3357  elin2  3360  ineqri  3363  dfss1  3374  dfss5  3375  nsspssun  3403  indifdir  3426  inrab2  3442  rabun2  3448  reuun2  3452  eq0  3470  0el  3472  abn0  3474  0pss  3493  disjr  3497  disj1  3498  disjpss  3506  undif4  3512  difin0ss  3521  inssdif0  3522  uneqdifeq  3543  r19.3rz  3546  r19.3rzv  3548  ralidm  3558  pwss  3640  dfpr2  3657  ralsns  3671  rexsns  3672  eltpg  3677  ralprg  3683  rexprg  3684  raltpg  3685  rextpg  3686  euabsn2  3699  eusn  3704  eldifsn  3750  rexdifsn  3754  difsnpss  3759  pwpw0  3764  ssunsn  3775  eqsn  3776  sstp  3779  tpss  3780  prel12  3790  preqsn  3793  pwsnALT  3823  pwtp  3825  eluniab  3840  elunirab  3841  unipr  3842  dfnfc2  3846  uniun  3847  uniin  3848  unissb  3858  elintab  3874  elintrab  3875  ssintab  3880  ssintrab  3886  intun  3895  intpr  3896  elrint  3904  iuncom4  3913  iuneq2  3922  dfiun2g  3936  ssiinf  3952  elriin  3975  iunxiun  3985  pwssb  3989  iunpwss  3992  dfdisj2  3996  nfdisj  4006  disjor  4008  disjors  4010  invdisj  4013  disjiun  4014  disjxiun  4021  disjxun  4022  cbvopab1  4090  dftr5  4117  trint  4129  inex1  4156  inuni  4176  axpweq  4186  nfnid  4203  zfpair2  4214  moabex  4231  exss  4235  elop  4238  otth  4249  copsex4g  4254  opeqsn  4261  opthwiener  4267  opelopabsbOLD  4272  brabga  4278  opelopabaf  4287  opabn0  4294  iunopab  4295  pwunss  4297  pwundifOLD  4300  dfid3  4309  pocl  4320  sotric  4339  isso2i  4345  somo  4347  frminex  4372  dfepfr  4377  wefrc  4386  ordtri3or  4423  ordtri2  4426  elsuci  4457  elsucg  4458  sucel  4464  on0eqel  4509  uniuni  4526  reusv2lem4  4537  reusv2lem5  4538  reusv2  4539  reusv3  4541  reuxfr2d  4556  elpwun  4566  iunpw  4569  dfwe2  4572  onintrab2  4592  ordpwsuc  4605  ordzsl  4635  dflim4  4638  tfindsg  4650  tfindes  4652  findsg  4682  elxp  4705  opelxp  4718  brxp  4719  rabxp  4724  opthprc  4735  brab2a  4737  opeliunxp  4739  xpundi  4740  xpundir  4741  elvvv  4748  brinxp  4751  brab2ga  4762  xp0r  4767  eqrelrel  4787  reliun  4805  reluni  4807  raliunxp  4824  rexiunxp  4825  ralxpf  4829  rexxpf  4830  iunxpf  4831  relop  4833  elcnv  4857  elcnv2  4858  dmin  4885  dmuni  4887  dmopab  4888  dmi  4892  rnopab  4923  elrnmpt1  4927  rncoeq  4947  resiexg  4996  dfima2  5013  dfima3  5014  elima2  5017  elima3  5018  imai  5026  elimasn  5037  epini  5042  dfse2  5045  cotr  5054  issref  5055  intasym  5057  asymref  5058  asymref2  5059  somin1  5078  cnvopab  5082  cnvi  5084  cnvdif  5086  imainss  5095  dfrel2  5123  dfrel3  5129  rnsnn0  5137  relsn2  5141  dmsnopg  5142  cnvcnvsn  5148  elxp4  5158  elxp5  5159  cnvresima  5160  mptpreima  5164  dfco2  5170  coundi  5172  coundir  5173  imaco  5176  coiun  5180  coi1  5186  relssdmrn  5191  relrelss  5194  ressn  5209  cnviin  5210  cnvpo  5211  dffun2  5231  dffun3  5232  dffun4  5233  dffun5  5234  dffun7  5246  dffun8  5247  dffun9  5248  funopab  5253  funun  5262  funcnvsn  5263  funcnv2  5275  funcnv  5276  fun2cnv  5278  fncnv  5280  fun11  5281  fununi  5282  imadif  5293  funimaexg  5295  fnunsn  5317  fnres  5326  fnopabg  5333  mptfng  5335  mptun  5340  fun  5371  fresaunres1  5380  fcnvres  5384  dff12  5402  f1cnvcnv  5411  funforn  5424  dff1o2  5443  dff1o5  5447  f1orn  5448  resdif  5460  ffoss  5471  f11o  5472  f1o00  5474  fo00  5475  elfv  5484  fv3  5502  dffn5f  5539  dffv2  5554  eqfnfv3  5586  fndmdifeq0  5593  fneqeql  5595  unpreima  5613  respreima  5616  dff4  5636  dffo3  5637  dffo5  5639  f1ompt  5644  ffnfvf  5648  fmptco  5653  fsn2  5660  fconst3  5697  fconst4  5698  idref  5721  abrexco  5728  opabex3  5731  abexssex  5743  dff13  5745  dff13f  5746  f1mpt  5747  foeqcnvco  5766  isocnv3  5791  isoini  5797  weniso  5814  oprabid  5844  dfoprab2  5857  eqoprab2b  5868  dmoprab  5890  rnoprab  5892  eloprabga  5896  mpt2mptx  5900  resoprab  5902  ffnov  5910  fnov  5914  elrnmpt2  5919  ralrnmpt2  5920  rexrnmpt2  5921  oprabex3  5924  oprabrexex2  5925  ovid  5926  ov3  5946  ov6g  5947  foov  5956  ndmovdistr  5971  difxp  6115  elopaba  6144  fmpt2  6153  curry1  6172  curry2  6175  fsplit  6185  frxp  6187  xporderlem  6188  soxp  6190  brtpos2  6202  dmtpos  6208  tpostpos  6216  tpossym  6228  tposoprab  6232  sorpsscmpl  6250  cbviota  6258  opiota  6284  eusvobj2  6333  dfsmo2  6360  tfrlem3  6389  tfrlem7  6395  tfrlem9  6397  tfrlem9a  6398  tz7.48lem  6449  tz7.49c  6454  el1o  6494  dif1o  6495  ondif2  6497  brwitnlem  6502  oarec  6556  omeulem1  6576  omeu  6579  oeordi  6581  oeeui  6596  oeeu  6597  omopthlem1  6649  dfer2  6657  brdifun  6683  swoso  6687  eqerlem  6688  qsid  6721  iiner  6727  erinxp  6729  brecop  6747  eroveu  6749  erovlem  6750  ecopovsym  6756  mapval2  6793  mapsn  6805  elixp  6819  ixpeq2  6826  ixpin  6837  ixpiin  6838  mptelixpg  6849  ixpsnf1o  6852  boxriin  6854  domen  6871  isfi  6881  en1  6924  xpsnen  6942  xpcomco  6948  xpassen  6952  sbthlem9  6975  0sdomg  6986  2pwuninel  7012  ssenen  7031  nneneq  7040  php  7041  modom2  7060  ac6sfi  7097  frfi  7098  fimaxg  7100  elfpw  7153  fissuni  7156  dffi3  7180  marypha1lem  7182  marypha2lem2  7185  dfsup2  7191  dfsup2OLD  7192  wofib  7256  wemapso2lem  7261  wdom2d  7290  unxpwdom2  7298  dford2  7317  inf2  7320  inf3lem2  7326  axinf2  7337  zfinf2  7339  cantnfp1lem2  7377  oemapso  7380  cantnflem1  7387  trcl  7406  epfrs  7409  rankvalb  7465  r1elss  7474  unbndrank  7510  scott0s  7554  cplem1  7555  bnd2  7559  isnum2  7574  iscard2  7605  infxpenlem  7637  fseqenlem1  7647  acnnum  7675  infpwfien  7685  alephnbtwn2  7695  alephord2  7699  alephislim  7706  cardaleph  7712  alephval3  7733  aceq1  7740  aceq2  7742  dfac3  7744  dfac4  7745  dfac5lem1  7746  dfac5lem2  7747  dfac5lem3  7748  dfac5lem4  7749  dfac5lem5  7750  dfac2  7753  dfac0  7755  dfac1  7756  dfac8  7757  dfac9  7758  dfac12  7771  kmlem3  7774  kmlem4  7775  kmlem7  7778  kmlem8  7779  kmlem9  7780  kmlem13  7784  kmlem14  7785  kmlem15  7786  dfackm  7788  pwsdompw  7826  ackbij2lem2  7862  cf0  7873  cfval2  7882  cflim2  7885  cfss  7887  cfslb  7888  isfin3  7918  isfin5  7921  isfin6  7922  sdom2en01  7924  fin23lem25  7946  fin23lem26  7947  fin23lem40  7973  isfin1-2  8007  isfin1-3  8008  fin1a2lem5  8026  fin1a2lem6  8027  fin1a2lem12  8033  fin12  8035  domtriomlem  8064  axdc2lem  8070  axdc3lem2  8073  axdc3lem4  8075  axcclem  8079  ac6num  8102  ac9  8106  ac6n  8108  ac9s  8116  zorn2lem6  8124  zornn0g  8128  ttukeylem6  8137  ttukey2g  8139  brdom7disj  8152  brdom6disj  8153  iunfo  8157  iundom2g  8158  konigthlem  8186  alephsuc3  8198  elgch  8240  fpwwe2lem9  8256  fpwwe2lem12  8259  fpwwe2lem13  8260  fpwwe2  8261  canth4  8265  canthwe  8269  wunex2  8356  uniwun  8358  axgroth5  8442  grothpw  8444  axgroth6  8446  grothprimlem  8451  grothprim  8452  elni  8496  ltexpi  8522  nqerf  8550  nqerid  8553  ordpipq  8562  recmulnq  8584  npomex  8616  genpnnp  8625  genpass  8629  addcompr  8641  mulcompr  8643  reclem2pr  8668  reclem3pr  8669  ltsosr  8712  ltasr  8718  mappsrpr  8726  map2psrpr  8728  opelcn  8747  elreal  8749  elreal2  8750  axaddf  8763  axmulf  8764  axicn  8768  axrrecex  8781  axpre-mulgt0  8786  xrlenlt  8886  ssxr  8888  leloe  8904  msq0i  9411  infm3  9709  supmullem2  9717  inelr  9732  arch  9958  elnnne0  9975  un0addcl  9993  un0mulcl  9994  elnnz  10030  elznn0nn  10033  elznn0  10034  elznn  10035  elz2  10036  raluz2  10264  rexuz2  10266  nnwos  10282  eluz2b2  10286  eluz2b3  10287  ublbneg  10298  zmin  10308  elq  10314  ralrp  10368  rexrp  10369  ltxr  10453  xrnemnf  10456  xrleloe  10474  xrltlen  10476  xrrebnd  10493  xaddf  10547  xmullem  10580  xmullem2  10581  xrsupss  10623  xrinfmss  10624  elfzp1  10832  fzprval  10840  fztpval  10841  fzm1  10858  fzolb  10876  fzolb2  10877  elfzo3  10886  fzouzsplit  10897  fzo0n0  10901  fzind2  10919  uzrdgfni  11017  subsq0i  11212  crreczi  11222  nn0le2msqi  11278  nn0opth2i  11282  hashkf  11335  hashfun  11385  hashbclem  11386  hashbc  11387  hashf1lem2  11390  leiso  11393  iswrd  11411  climeu  12025  lo1resb  12034  rlimresb  12035  o1resb  12036  climmpt2  12043  fsum2dlem  12229  rpnnen2  12500  sqr2irr  12523  divides  12529  odd2np1  12583  divalglem1  12589  divalglem6  12593  divalglem10  12597  divalgb  12599  bitsval2  12612  bitsmod  12623  bitscmp  12625  smueqlem  12677  isprm2  12762  isprm3  12763  isprm4  12764  isprm5  12787  pythagtriplem19  12882  pythagtrip  12883  pceu  12895  prmreclem2  12960  4sqlem2  12992  4sqlem12  12999  vdwpc  13023  vdwnn  13041  dec5dvds2  13076  pwsle  13387  imasleval  13439  xpsfrnel  13461  xpsfrnel2  13463  xpsle  13479  isacs2  13551  mreacs  13556  iscatd2  13579  comfeq  13605  oppcsect  13672  isssc  13693  isfunc  13734  funcoppc  13745  isffth2  13786  fucinv  13843  elhoma  13860  setcinv  13918  ispos  14077  ispos2  14078  tosso  14138  istsr2  14323  spwmo  14331  ismnd  14365  mndcl  14368  issubm  14421  gsumwspan  14464  issubg  14617  isnsg2  14643  eqger  14663  isgim2  14725  giclcl  14732  gicrcl  14733  gicsubgen  14738  gaorber  14758  resscntz  14803  cntzrec  14805  efgval2  15029  efgsfo  15044  efgrelexlemb  15055  isabl2  15093  iscyggen2  15164  iscyg2  15165  iscyg3  15169  lt6abl  15177  gsumval3eu  15186  gsum2d2  15221  dmdprdd  15233  subgdmdprd  15265  iscrng2  15352  dvdsrtr  15430  isunit  15435  isnirred  15478  isirred2  15479  isrhm  15497  isdrng2  15518  drngprop  15519  isabv  15580  issrng  15611  islmod  15627  islss  15688  lss1d  15716  islmim2  15815  lmiclcl  15819  lmicrcl  15820  lsmelval2  15834  lspsolvlem  15891  lspsncv0  15895  islpidl  15994  islpir2  15999  isnzr2  16011  isdomn2  16036  fiidomfld  16045  aspval2  16082  mplcoe1  16205  mplcoe2  16207  evlslem4  16241  xrsdsreclb  16414  unocv  16576  iunocv  16577  ishil2  16615  isobs  16616  obselocv  16624  iinopn  16644  istps4OLD  16657  istps5OLD  16658  istps  16670  istps2  16671  isbasis2g  16682  tgval2  16690  elcls  16806  islpi  16876  isperf2  16879  isperf3  16880  restntr  16908  ordtbaslem  16914  ordtrest2lem  16929  cnrest  17009  ist0-3  17069  ist1-2  17071  ist1-3  17073  nrmsep3  17079  isnrm2  17082  perfcls  17089  ordthaus  17108  cmpcov2  17113  cmpsub  17123  hauscmplem  17129  cmpfi  17131  iscon2  17136  dfcon2  17141  is1stc2  17164  is2ndc  17168  1stcelcls  17183  1stccn  17185  llyi  17196  subislly  17203  iskgen3  17240  txuni2  17256  ptpjpre1  17262  ptbasin  17268  tx1cn  17299  tx2cn  17300  uptx  17315  txdis1cn  17325  ptrescn  17329  txtube  17330  txcmplem1  17331  hausdiag  17335  txkgen  17342  xkohaus  17343  xkococnlem  17349  xkoinjcn  17377  qtopeu  17403  isr0  17424  regr1lem2  17427  hmphsym  17469  elmptrab2  17519  isfbas  17520  isfbas2  17526  trfbas  17535  snfil  17555  fbunfip  17560  elfg  17562  fgcl  17569  fbasrn  17575  filuni  17576  trfil2  17578  cfinfil  17584  csdfil  17585  supfil  17586  ufinffr  17620  rnelfmlem  17643  elflim2  17655  hausflim  17672  hauspwpwf1  17678  txflf  17697  isfcls2  17704  fclsopn  17705  fclsrest  17715  alexsubALTlem2  17738  alexsubALTlem3  17739  alexsubALTlem4  17740  tmdcn2  17768  divstgplem  17799  divstgphaus  17801  tsmssubm  17821  istdrg2  17856  metn0  17920  prdsxmetlem  17928  imasdsf1olem  17933  xpsdsval  17941  blres  17973  xmeterval  17974  xmeter  17975  isxms2  17990  isms2  17992  dscopn  18092  isngp3  18116  isnvc2  18205  isnghm  18228  qtopbaslem  18263  xrtgioo  18308  zcld  18315  elii1  18429  pi1cpbl  18538  tchcph  18663  cmetss  18736  bcth  18747  lssbn  18769  ishl2  18783  minveclem3b  18788  minveclem6  18794  pmltpc  18806  ovolfcl  18822  ovolgelb  18835  ovolunlem1  18852  ovoliunlem1  18857  ismbl  18881  ismbl2  18882  iundisj2  18902  dyadmax  18949  dyadmbllem  18950  vitalilem2  18960  mbfimaopnlem  19006  itg1climres  19065  itg2l  19080  itg2leub  19085  iblcnlem1  19138  ellimc2  19223  ellimc3  19225  limcmpt  19229  limcres  19232  elaa  19692  aaliou3lem9  19726  taylthlem2  19749  ulmcau  19768  pilem1  19823  sincosq1lem  19861  sineq0  19885  coseq1  19886  ellogrn  19913  logtayl2  20005  cxpcn3lem  20083  cxpcn3  20084  cubic  20141  atandm  20168  atandm2  20169  atandm4  20171  atans2  20223  xrlimcnp  20259  wilthlem2  20303  dvdsflsumcom  20424  dvdsmulf1o  20430  fsumvma  20448  logfac2  20452  dchrelbas2  20472  dchrelbas3  20473  lgsdir2lem4  20561  lgsquadlem1  20589  lgsquadlem2  20590  2sqlem1  20598  pntlem3  20754  ostth  20784  avril1  20830  grpoidinvlem3  20867  issubgo  20964  elghom  21024  islno  21325  nmoubi  21344  nmobndseqi  21351  siii  21425  minvecolem5  21454  minvecolem6  21455  hvsubaddi  21641  normsub0i  21710  bcsiALT  21754  hcau  21759  hlimadd  21768  hhcmpl  21775  hhcms  21778  issh2  21784  isch2  21799  hlim0  21811  isch3  21817  norm1exi  21825  elch0  21829  hhsssh2  21843  choc0  21901  pjhtheu  21969  pjpreeq  21973  omlsilem  21977  pjoc2i  22013  chsscon1i  22037  spanuni  22119  h1deoi  22124  h1dei  22125  elspansni  22133  cmcm4i  22170  cmbr3i  22175  cmbr4i  22176  osumcor2i  22219  5oalem7  22235  3oalem3  22239  pjss2i  22255  mayete3iOLD  22304  elcnop  22433  ellnop  22434  elhmop  22449  elcnfn  22458  ellnfn  22459  cnvadj  22468  nmopub  22484  nmfnleub  22501  eleigvec  22533  nmop0  22562  nmfn0  22563  nmopun  22590  lncnopbd  22613  riesz2  22642  nmopcoadj0i  22679  rnbra  22683  pjnmopi  22724  pjssdif1i  22751  pjin2i  22769  pjin3i  22770  pjclem1  22771  cvbr2  22859  cvnbtwn3  22864  cvnbtwn4  22865  mdsl2bi  22899  mdsldmd1i  22907  elat2  22916  chrelat2i  22941  atomli  22958  chirredi  22970  mdsymlem6  22984  mdsymlem8  22986  sumdmdii  22991  dmdbr5ati  22998  cdj3i  23017  xfree2  23021  ballotlemelo  23042  ballotlem2  23043  ballotlemfmpn  23049  ballotlemodife  23052  ballotlem4  23053  ballotth  23092  eldmgm  23101  subfacp1lem5  23122  subfacp1lem6  23123  cvmscld  23211  cvmlift2lem12  23252  vdgrun  23300  eupath  23312  ghomgrpilem2  23400  axextprim  23454  axrepprim  23455  axunprim  23456  axpowprim  23457  axregprim  23458  axinfprim  23459  axacprim  23460  untangtr  23467  biimpexp  23477  divelunit  23486  dftr6  23513  coep  23514  coepr  23515  dffr5  23516  dfpo2  23518  cnvco1  23523  cnvco2  23524  fundmpss  23526  dfdm5  23536  dfrn5  23537  elpotr  23541  dford5reg  23542  dfon2lem5  23547  dfon2lem6  23548  dfon2lem8  23550  dfon2lem9  23551  dfon2  23552  wfi  23611  eltrpred  23633  frind  23647  poseq  23657  soseq  23658  wfrlem4  23663  wfrlem5  23664  wfrlem9  23668  wfrlem11  23670  wfrlem12  23671  wfrlem13  23672  wfrlem14  23673  wfrlem15  23674  tfrALTlem  23680  tfr3ALT  23683  frrlem5  23689  frrlem5e  23693  frrlem11  23697  nosgnn0  23715  axdenselem5  23743  axfelem12  23761  axfelem15  23764  axfelem18  23767  axfelem22  23771  elsymdif  23778  brsymdif  23783  brtxp  23831  brpprod  23836  brpprod3b  23838  brsset  23840  idsset  23841  dfon3  23843  brtxpsd  23845  brtxpsd2  23846  brbigcup  23849  elfix  23854  dffix2  23856  ellimits  23861  elfuns  23864  snelsingles  23871  dfiota3  23872  brcart  23881  brimg  23886  brapply  23887  brcup  23888  brcap  23889  brsuccf  23890  funpartfun  23891  fullfunfnv  23894  brrestrict  23897  dfrdg4  23898  tfrqfree  23899  altopthsn  23905  altopelaltxp  23920  altxpsspw  23921  mptelee  23933  brbtwn2  23943  colinearalg  23948  ax5seg  23976  axpasch  23979  axlowdimlem6  23985  axlowdimlem13  23992  axeuclidlem  24000  axeuclid  24001  axcontlem3  24004  axcontlem4  24005  axcontlem12  24013  brcolinear2  24091  broutsideof  24154  outsideofcom  24161  fvray  24174  fvline  24177  lineunray  24180  linecom  24183  linerflx2  24184  ellines  24185  bpoly2  24202  bpoly3  24203  rankeq1o  24211  elhf  24214  elhf2  24215  r19.26-2a  24344  eeeeanv  24354  altdftru  24358  pm11.53g  24374  eqvinopb  24375  copsexgb  24376  ltl4ev  24402  albineal  24409  evevifev  24424  cnvref  24475  restidsing  24486  dffn5a  24541  repcpwti  24572  dfdir2  24702  apnei  24931  ismonc  25225  isepic  25235  isfunb  25246  issubcata  25257  isntr  25284  clscnc  25421  bisig0  25473  isconcl5a  25512  isconcl5ab  25513  isibg2  25521  bosser  25578  hpd  25580  ecase13d  25633  cnvresimaOLD  25637  trer  25638  elicc3  25639  finminlem  25642  opnrebl  25646  nn0prpw  25650  clsun  25657  fneval  25698  fnessref  25704  neibastop1  25719  neifg  25731  filnetlem4  25741  f1opr  25802  inixp  25810  sdclem2  25863  sdclem1  25864  fdc  25866  neificl  25878  istotbnd3  25906  sstotbnd3  25911  isbndx  25917  isbnd3b  25920  cntotbnd  25931  heibor1lem  25944  heibor1  25945  isdrngo2  26000  isdrngo3  26001  iscrngo2  26034  smprngopr  26088  isdmn2  26091  isfldidl2  26105  ispridlc  26106  isdmn3  26110  an43OLD  26124  prtlem70  26126  prtlem100  26132  n0el  26136  prter2  26160  funsnfsup  26173  cmpfiiin  26183  isnacs2  26192  elmzpcl  26215  diophrex  26266  2sbcrex  26275  sbcrot3  26279  sbcrot5  26280  3rexfrabdioph  26289  4rexfrabdioph  26290  6rexfrabdioph  26291  7rexfrabdioph  26292  ftp  26304  fphpd  26310  fiphp3d  26313  rencldnfilem  26314  jm2.23  26500  expdiophlem1  26525  expdiophlem2  26526  expdioph  26527  dford4  26533  wopprc  26534  ttac  26540  fnwe2lem2  26559  islmodfg  26578  islnm2  26587  lnmlmic  26597  uvcvv0  26650  isnumbasgrplem1  26677  dfacbasgrp  26684  islinds2  26694  lmiclbs  26718  islnr2  26729  islnr3  26730  f1omvdco3  26803  matrcl  26877  issdrg2  26917  sdrgacs  26920  phisum  26929  isdomn3  26934  pm10.541  26973  pm10.542  26974  19.21vv  26985  19.36vv  26992  19.31vv  26993  19.37vv  26994  19.28vv  26995  pm11.6  27002  pm11.62  27004  pm14.12  27032  elnev  27049  evth2f  27097  elunif  27098  evthf  27109  stoweidlem14  27174  stoweidlem24  27184  stoweidlem31  27191  stoweidlem34  27194  stoweidlem37  27197  stoweidlem51  27211  stoweidlem54  27214  stoweidlem57  27217  stoweidlem59  27219  aiffnbandciffatnotciffb  27263  mdandyvr0  27301  mdandyvr1  27302  mdandyvr2  27303  mdandyvr3  27304  mdandyvr4  27305  mdandyvr5  27306  mdandyvr6  27307  mdandyvr7  27308  mdandyvr8  27309  mdandyvr9  27310  mdandyvr10  27311  mdandyvr11  27312  mdandyvr12  27313  mdandyvr13  27314  mdandyvr14  27315  mdandyvr15  27316  rexrsb  27338  2rexsb  27339  2rexrsb  27340  cbvral2  27341  cbvrex2  27342  2ralbiim  27343  2reu5a  27346  rmoanim  27348  2rmoswap  27353  2reu1  27355  2reu3  27357  2reu4a  27358  afvpcfv0  27400  ffnaov  27450  ndmaovass  27457  ndmaovdistr  27458  gte-lteh  27468  gt-lth  27469  sgnn  27523  eldiftp  27534  onfrALTlem5  27590  onfrALTlem4  27591  onfrALTlem1  27596  2uasbanh  27610  dfvd2  27631  dfvd2an  27634  dfvd3  27643  dfvd3an  27646  eelT00  27760  eelTTT  27761  eelT12  27766  uunT1  27835  uunT1p1  27836  uun132p1  27841  un2122  27845  uunTT1p1  27849  uunTT1p2  27850  uunT11p1  27852  uunT11p2  27853  uunT12  27854  uunT12p1  27855  uunT12p2  27856  uunT12p3  27857  uunT12p4  27858  uunT12p5  27859  uun2221  27868  uun2221p1  27869  uun2221p2  27870  undif3VD  27938  onfrALTlem5VD  27941  onfrALTlem4VD  27942  onfrALTlem1VD  27946  2uasbanhVD  27967  bnj170  28002  bnj248  28004  bnj251  28006  bnj256  28010  bnj258  28012  bnj291  28015  bnj422  28019  bnj432  28020  bnj23  28023  bnj89  28026  bnj132  28031  bnj156  28035  bnj158  28036  bnj538  28048  bnj563  28051  bnj945  28084  bnj946  28085  bnj976  28088  bnj1098  28094  bnj1138  28099  bnj1209  28108  bnj1476  28158  bnj1542  28168  bnj110  28169  bnj91  28172  bnj92  28173  bnj106  28179  bnj118  28180  bnj124  28182  bnj125  28183  bnj153  28191  bnj207  28192  bnj222  28194  bnj518  28197  bnj535  28201  bnj539  28202  bnj543  28204  bnj553  28209  bnj556  28211  bnj558  28213  bnj571  28217  bnj605  28218  bnj591  28222  bnj594  28223  bnj580  28224  bnj609  28228  bnj611  28229  bnj865  28234  bnj849  28236  bnj882  28237  bnj916  28244  bnj917  28245  bnj934  28246  bnj929  28247  bnj944  28249  bnj953  28250  bnj1000  28252  bnj969  28257  bnj970  28258  bnj978  28260  bnj983  28262  bnj984  28263  bnj985  28264  bnj986  28265  bnj1021  28275  bnj1033  28278  bnj1049  28283  bnj1052  28284  bnj1083  28287  bnj1112  28292  bnj1030  28296  bnj1137  28304  bnj1189  28318  bnj1204  28321  bnj1253  28326  bnj1279  28327  bnj1373  28339  bnj1388  28342  bnj1398  28343  bnj1450  28359  equvelv  28395  a12study4  28396  a12study8  28398  a12peros  28400  a12lem2  28410  a12study10  28415  a12study10n  28416  lsateln0  28464  islshpat  28486  lcvbr2  28491  lcvbr3  28492  lcvnbtwn3  28497  islfl  28529  lshpsmreu  28578  lub0N  28658  glb0N  28662  cvrnbtwn3  28745  leat2  28763  isat3  28776  iscvlat2N  28793  ishlat2  28822  ishlat3N  28823  hlrelat5N  28869  hlrelat2  28871  3dim0  28925  2dim  28938  islpln5  29003  islvol5  29047  4atlem3  29064  dalem20  29161  ispsubsp2  29214  snatpsubN  29218  pmapglb  29238  elpadd  29267  paddasslem17  29304  dalawlem13  29351  pclfinN  29368  polval2N  29374  pclfinclN  29418  lhpex2leN  29481  isltrn2N  29588  cdleme0nex  29758  cdleme22b  29809  cdlemftr3  30033  tendoset  30227  diarnN  30598  dibopelvalN  30612  dibopelval2  30614  dibelval3  30616  diblsmopel  30640  dicelval3  30649  dihglb2  30811  doch11  30842  islpolN  30952  lcfls1N  31004  mapdval4N  31101  mapdrvallem2  31114
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