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

Theorem bitri 242
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 188 . . 3  |-  ( ph  ->  ps )
3 bitri.2 . . 3  |-  ( ps  <->  ch )
42, 3sylib 190 . 2  |-  ( ph  ->  ch )
53biimpri 199 . . 3  |-  ( ch 
->  ps )
65, 1sylibr 205 . 2  |-  ( ch 
->  ph )
74, 6impbii 182 1  |-  ( ph  <->  ch )
Colors of variables: wff set class
Syntax hints:    <-> wb 178
This theorem is referenced by:  bitr2i  243  bitr3i  244  bitr4i  245  bitrd  246  3bitri  264  3bitr2i  266  3bitr3i  268  3bitr4i  270  xchbinx  303  bibi12i  308  imbi12i  318  mt2bi  330  iman  415  orbi12i  509  or42  517  pm4.71r  615  biadan2  626  anbi2ci  680  anbi12i  681  anbi12ci  682  pm5.3  695  pm5.53  774  an42  801  orddi  844  anddi  845  rbaib  878  rbaibr  879  pm4.43  898  biluk  904  pm5.75  908  dn1  937  3orass  942  3anass  943  3ancomb  948  3anan32  951  3anan12  952  3anor  953  an6  1266  xor2  1306  falbitru  1348  falnantru  1352  truxortru  1354  truxorfal  1355  falxorfal  1357  exp3acom23g  1367  hadass  1382  hadbi  1383  hadrot  1386  cador  1387  cadan  1388  cadnot  1390  cadcomb  1392  cadrot  1393  cad1  1394  had1  1398  alex  1570  alinexa  1576  alexn  1577  exanali  1583  19.26-2  1593  19.26-3an  1594  alrot3  1610  alrot4  1611  albiim  1612  2albiim  1613  19.21-2  1772  nf2  1778  19.27  1786  19.28  1787  19.36  1788  19.37  1790  19.44  1796  19.45  1797  exrot3  1802  exrot4  1803  aaan  1811  eeor  1812  ax12b  1834  sbor  1959  sbrim  1960  sblim  1961  sban  1962  sbbi  1964  sblbis  1965  sbrbis  1966  sbrbif  1967  sbid2  1979  sbco2d  1982  sb8e  1988  19.23vv  2023  pm11.53  2025  19.41vv  2036  19.41vvv  2037  19.41vvvv  2038  19.42vv  2041  19.42vvv  2042  4exdistr  2045  cbvex4v  2056  eean  2057  sbnf2  2071  2sb5  2075  2sb6  2076  sbcom2  2077  sb6a  2079  2sb5rf  2080  2sb6rf  2081  sbex  2091  sbalv  2092  exsbOLD  2094  2exsb  2095  eujust  2120  euf  2124  cbveu  2138  eu2  2143  mo2  2147  sbmo  2148  mo3  2149  mo4f  2150  eu4  2157  moanim  2174  2mo  2196  2mos  2197  2eu1  2198  2eu3  2200  2eu4  2201  2eu6  2203  exists1  2207  abid  2246  eleq12i  2323  abeq2  2363  abeq2i  2365  clabel  2379  abid2f  2419  sbabel  2420  neeq12i  2433  necon1abii  2472  neanior  2506  ralnex  2528  rexnal  2529  ralinexa  2563  rexanali  2564  r3al  2575  r19.26-2  2651  ralbiim  2655  r19.30  2660  ralcomf  2673  rexcomf  2674  rexrot4  2678  reean  2681  3reeanv  2683  rabbi  2693  cbvralf  2733  cbvreu  2737  cbvral2v  2747  cbvrex2v  2748  cbvral3v  2749  cbvralsv  2750  cbvrexsv  2751  sbralie  2752  rabeq2i  2760  issetf  2768  2gencl  2792  3gencl  2793  ceqsex2  2799  ceqsex3v  2801  ceqsex6v  2803  ceqsex8v  2804  gencbvex  2805  cla43gv  2848  eqvincf  2871  ceqsrex2v  2878  elrab2  2900  ralab  2901  ralrab  2902  rexab  2903  rexrab  2904  ralab2  2905  rexab2  2907  eueq3  2915  morex  2924  euxfr2  2925  euxfr  2926  euind  2927  reu2  2928  reu6  2929  rmo4  2933  reu4  2934  reu7  2935  rmoim  2939  2reuswap  2942  reuind  2943  2reu5lem1  2945  2reu5lem2  2946  2reu5  2948  sbcco  2988  sbccomlem  3036  sbccom  3037  ra5  3050  rmo3  3053  csbco  3065  sbnfc2  3116  csbabg  3117  cbvralcsf  3118  cbvreucsf  3120  dfss  3142  dfss2f  3146  ss2ab  3216  dfpss2  3236  dfpss3  3237  psseq12i  3242  sspsstri  3253  difeqri  3271  uneqri  3292  ssequn2  3323  unss  3324  rexun  3330  ralunb  3331  elin2  3334  ineqri  3337  dfss1  3348  dfss5  3349  nsspssun  3377  indifdir  3400  inrab2  3416  rabun2  3422  reuun2  3426  eq0  3444  0el  3446  abn0  3448  0pss  3467  disjr  3471  disj1  3472  disjpss  3480  undif4  3486  difin0ss  3495  inssdif0  3496  uneqdifeq  3517  r19.3rz  3520  r19.3rzv  3522  ralidm  3532  pwss  3613  dfpr2  3630  ralsns  3644  rexsns  3645  eltpg  3650  ralprg  3656  rexprg  3657  raltpg  3658  rextpg  3659  euabsn2  3672  eusn  3677  eldifsn  3723  rexdifsn  3727  difsnpss  3732  pwpw0  3737  ssunsn  3748  eqsn  3749  sstp  3752  tpss  3753  prel12  3763  preqsn  3766  pwsnALT  3796  pwtp  3798  eluniab  3813  elunirab  3814  unipr  3815  dfnfc2  3819  uniun  3820  uniin  3821  unissb  3831  elintab  3847  elintrab  3848  ssintab  3853  ssintrab  3859  intun  3868  intpr  3869  elrint  3877  iuncom4  3886  iuneq2  3895  dfiun2g  3909  ssiinf  3925  elriin  3948  iunxiun  3958  pwssb  3962  iunpwss  3965  dfdisj2  3969  nfdisj  3979  disjor  3981  disjors  3983  invdisj  3986  disjiun  3987  disjxiun  3994  disjxun  3995  cbvopab1  4063  dftr5  4090  trint  4102  inex1  4129  inuni  4149  axpweq  4159  nfnid  4176  zfpair2  4187  moabex  4204  exss  4208  elop  4211  otth  4222  copsex4g  4227  opeqsn  4234  opthwiener  4240  opelopabsbOLD  4245  brabga  4251  opelopabaf  4260  opabn0  4267  iunopab  4268  pwunss  4270  pwundifOLD  4273  dfid3  4282  pocl  4293  sotric  4312  isso2i  4318  somo  4320  frminex  4345  dfepfr  4350  wefrc  4359  ordtri3or  4396  ordtri2  4399  elsuci  4430  elsucg  4431  sucel  4437  on0eqel  4482  uniuni  4499  reusv2lem4  4510  reusv2lem5  4511  reusv2  4512  reusv3  4514  reuxfr2d  4529  elpwun  4539  iunpw  4542  dfwe2  4545  onintrab2  4565  ordpwsuc  4578  ordzsl  4608  dflim4  4611  tfindsg  4623  tfindes  4625  findsg  4655  elxp  4694  opelxp  4707  brxp  4708  rabxp  4713  opthprc  4724  brab2a  4726  opeliunxp  4728  xpundi  4729  xpundir  4730  elvvv  4737  brinxp  4740  brab2ga  4751  xp0r  4756  eqrelrel  4776  reliun  4794  reluni  4796  raliunxp  4813  rexiunxp  4814  ralxpf  4818  rexxpf  4819  iunxpf  4820  relop  4822  elcnv  4846  elcnv2  4847  dmin  4874  dmuni  4876  dmopab  4877  dmi  4881  rnopab  4912  elrnmpt1  4916  rncoeq  4936  resiexg  4985  dfima2  5002  dfima3  5003  elima2  5006  elima3  5007  imai  5015  elimasn  5026  epini  5031  dfse2  5034  cotr  5043  issref  5044  intasym  5046  asymref  5047  asymref2  5048  somin1  5067  cnvopab  5071  cnvi  5073  cnvdif  5075  imainss  5084  dfrel2  5112  dfrel3  5118  rnsnn0  5126  relsn2  5130  dmsnopg  5131  cnvcnvsn  5137  elxp4  5147  elxp5  5148  cnvresima  5149  mptpreima  5153  dfco2  5159  coundi  5161  coundir  5162  imaco  5165  coiun  5169  coi1  5175  relssdmrn  5180  relrelss  5183  ressn  5198  cnviin  5199  cnvpo  5200  dffun2  5204  dffun3  5205  dffun4  5206  dffun5  5207  dffun7  5219  dffun8  5220  dffun9  5221  funopab  5226  funun  5234  funcnvsn  5235  funcnv2  5247  funcnv  5248  fun2cnv  5250  fncnv  5252  fun11  5253  fununi  5254  imadif  5265  funimaexg  5267  fnunsn  5289  fnres  5298  fnopabg  5305  mptfng  5307  mptun  5312  fun  5343  fresaunres1  5352  fcnvres  5356  dff12  5374  f1cnvcnv  5383  funforn  5396  dff1o2  5415  dff1o5  5419  f1orn  5420  resdif  5432  ffoss  5443  f11o  5444  f1o00  5446  fo00  5447  elfv  5456  fv3  5474  dffn5f  5511  dffv2  5526  eqfnfv3  5558  fndmdifeq0  5565  fneqeql  5567  unpreima  5585  respreima  5588  dff4  5608  dffo3  5609  dffo5  5611  f1ompt  5616  ffnfvf  5620  fmptco  5625  fsn2  5632  fconst3  5669  fconst4  5670  idref  5693  abrexco  5700  opabex3  5703  abexssex  5715  dff13  5717  dff13f  5718  f1mpt  5719  foeqcnvco  5738  isocnv3  5763  isoini  5769  weniso  5786  oprabid  5816  dfoprab2  5829  eqoprab2b  5840  dmoprab  5862  rnoprab  5864  eloprabga  5868  mpt2mptx  5872  resoprab  5874  ffnov  5882  fnov  5886  elrnmpt2  5891  ralrnmpt2  5892  rexrnmpt2  5893  oprabex3  5896  oprabrexex2  5897  ovid  5898  ov3  5918  ov6g  5919  foov  5928  ndmovdistr  5943  difxp  6087  elopaba  6116  fmpt2  6125  curry1  6144  curry2  6147  fsplit  6157  frxp  6159  xporderlem  6160  soxp  6162  brtpos2  6174  dmtpos  6180  tpostpos  6188  tpossym  6200  tposoprab  6204  sorpsscmpl  6222  cbviota  6230  opiota  6256  eusvobj2  6305  dfsmo2  6332  tfrlem3  6361  tfrlem7  6367  tfrlem9  6369  tfrlem9a  6370  tz7.48lem  6421  tz7.49c  6426  el1o  6466  dif1o  6467  ondif2  6469  brwitnlem  6474  oarec  6528  omeulem1  6548  omeu  6551  oeordi  6553  oeeui  6568  oeeu  6569  omopthlem1  6621  dfer2  6629  brdifun  6655  swoso  6659  eqerlem  6660  qsid  6693  iiner  6699  erinxp  6701  brecop  6719  eroveu  6721  erovlem  6722  ecopovsym  6728  mapval2  6765  mapsn  6777  elixp  6791  ixpeq2  6798  ixpin  6809  ixpiin  6810  mptelixpg  6821  ixpsnf1o  6824  boxriin  6826  domen  6843  isfi  6853  en1  6896  xpsnen  6914  xpcomco  6920  xpassen  6924  sbthlem9  6947  0sdomg  6958  2pwuninel  6984  ssenen  7003  nneneq  7012  php  7013  modom2  7032  ac6sfi  7069  frfi  7070  fimaxg  7072  elfpw  7125  fissuni  7128  dffi3  7152  marypha1lem  7154  marypha2lem2  7157  dfsup2  7163  dfsup2OLD  7164  wofib  7228  wemapso2lem  7233  wdom2d  7262  unxpwdom2  7270  dford2  7289  inf2  7292  inf3lem2  7298  axinf2  7309  zfinf2  7311  cantnfp1lem2  7349  oemapso  7352  cantnflem1  7359  trcl  7378  epfrs  7381  rankvalb  7437  r1elss  7446  unbndrank  7482  scott0s  7526  cplem1  7527  bnd2  7531  isnum2  7546  iscard2  7577  infxpenlem  7609  fseqenlem1  7619  acnnum  7647  infpwfien  7657  alephnbtwn2  7667  alephord2  7671  alephislim  7678  cardaleph  7684  alephval3  7705  aceq1  7712  aceq2  7714  dfac3  7716  dfac4  7717  dfac5lem1  7718  dfac5lem2  7719  dfac5lem3  7720  dfac5lem4  7721  dfac5lem5  7722  dfac2  7725  dfac0  7727  dfac1  7728  dfac8  7729  dfac9  7730  dfac12  7743  kmlem3  7746  kmlem4  7747  kmlem7  7750  kmlem8  7751  kmlem9  7752  kmlem13  7756  kmlem14  7757  kmlem15  7758  dfackm  7760  pwsdompw  7798  ackbij2lem2  7834  cf0  7845  cfval2  7854  cflim2  7857  cfss  7859  cfslb  7860  isfin3  7890  isfin5  7893  isfin6  7894  sdom2en01  7896  fin23lem25  7918  fin23lem26  7919  fin23lem40  7945  isfin1-2  7979  isfin1-3  7980  fin1a2lem5  7998  fin1a2lem6  7999  fin1a2lem12  8005  fin12  8007  domtriomlem  8036  axdc2lem  8042  axdc3lem2  8045  axdc3lem4  8047  axcclem  8051  ac6num  8074  ac9  8078  ac6n  8080  ac9s  8088  zorn2lem6  8096  zornn0g  8100  ttukeylem6  8109  ttukey2g  8111  brdom7disj  8124  brdom6disj  8125  iunfo  8129  iundom2g  8130  konigthlem  8158  alephsuc3  8170  elgch  8212  fpwwe2lem9  8228  fpwwe2lem12  8231  fpwwe2lem13  8232  fpwwe2  8233  canth4  8237  canthwe  8241  wunex2  8328  uniwun  8330  axgroth5  8414  grothpw  8416  axgroth6  8418  grothprimlem  8423  grothprim  8424  elni  8468  ltexpi  8494  nqerf  8522  nqerid  8525  ordpipq  8534  recmulnq  8556  npomex  8588  genpnnp  8597  genpass  8601  addcompr  8613  mulcompr  8615  reclem2pr  8640  reclem3pr  8641  ltsosr  8684  ltasr  8690  mappsrpr  8698  map2psrpr  8700  opelcn  8719  elreal  8721  elreal2  8722  axaddf  8735  axmulf  8736  axicn  8740  axrrecex  8753  axpre-mulgt0  8758  xrlenlt  8858  ssxr  8860  leloe  8876  msq0i  9383  infm3  9681  supmullem2  9689  inelr  9704  arch  9930  elnnne0  9947  un0addcl  9965  un0mulcl  9966  elnnz  10002  elznn0nn  10005  elznn0  10006  elznn  10007  elz2  10008  raluz2  10236  rexuz2  10238  nnwos  10254  eluz2b2  10258  eluz2b3  10259  ublbneg  10270  zmin  10280  elq  10286  ralrp  10340  rexrp  10341  ltxr  10425  xrnemnf  10428  xrleloe  10446  xrltlen  10448  xrrebnd  10465  xaddf  10518  xmullem  10551  xmullem2  10552  xrsupss  10594  xrinfmss  10595  elfzp1  10803  fzprval  10811  fztpval  10812  fzm1  10829  fzolb  10847  fzolb2  10848  elfzo3  10857  fzouzsplit  10868  fzo0n0  10872  fzind2  10890  uzrdgfni  10988  subsq0i  11183  crreczi  11193  nn0le2msqi  11249  nn0opth2i  11253  hashkf  11306  hashfun  11355  hashbclem  11356  hashbc  11357  hashf1lem2  11360  leiso  11363  iswrd  11381  climeu  11995  lo1resb  12004  rlimresb  12005  o1resb  12006  climmpt2  12013  fsum2dlem  12199  rpnnen2  12467  sqr2irr  12490  divides  12496  odd2np1  12550  divalglem1  12556  divalglem6  12560  divalglem10  12564  divalgb  12566  bitsval2  12579  bitsmod  12590  bitscmp  12592  smueqlem  12644  isprm2  12729  isprm3  12730  isprm4  12731  isprm5  12754  pythagtriplem19  12849  pythagtrip  12850  pceu  12862  prmreclem2  12927  4sqlem2  12959  4sqlem12  12966  vdwpc  12990  vdwnn  13008  dec5dvds2  13043  pwsle  13354  imasleval  13406  xpsfrnel  13428  xpsfrnel2  13430  xpsle  13446  isacs2  13518  mreacs  13523  iscatd2  13546  comfeq  13572  oppcsect  13639  isssc  13660  isfunc  13701  funcoppc  13712  isffth2  13753  fucinv  13810  elhoma  13827  setcinv  13885  ispos  14044  ispos2  14045  tosso  14105  istsr2  14290  spwmo  14298  ismnd  14332  mndcl  14335  issubm  14388  gsumwspan  14431  issubg  14584  isnsg2  14610  eqger  14630  isgim2  14692  giclcl  14699  gicrcl  14700  gicsubgen  14705  gaorber  14725  resscntz  14770  cntzrec  14772  efgval2  14996  efgsfo  15011  efgrelexlemb  15022  isabl2  15060  iscyggen2  15131  iscyg2  15132  iscyg3  15136  lt6abl  15144  gsumval3eu  15153  gsum2d2  15188  dmdprdd  15200  subgdmdprd  15232  iscrng2  15319  dvdsrtr  15397  isunit  15402  isnirred  15445  isirred2  15446  isrhm  15464  isdrng2  15485  drngprop  15486  isabv  15547  issrng  15578  islmod  15594  islss  15655  lss1d  15683  islmim2  15782  lmiclcl  15786  lmicrcl  15787  lsmelval2  15801  lspsolvlem  15858  lspsncv0  15862  islpidl  15961  islpir2  15966  isnzr2  15978  isdomn2  16003  fiidomfld  16012  aspval2  16049  mplcoe1  16172  mplcoe2  16174  evlslem4  16208  xrsdsreclb  16381  unocv  16543  iunocv  16544  ishil2  16582  isobs  16583  obselocv  16591  iinopn  16611  istps4OLD  16624  istps5OLD  16625  istps  16637  istps2  16638  isbasis2g  16649  tgval2  16657  elcls  16773  islpi  16843  isperf2  16846  isperf3  16847  restntr  16875  ordtbaslem  16881  ordtrest2lem  16896  cnrest  16976  ist0-3  17036  ist1-2  17038  ist1-3  17040  nrmsep3  17046  isnrm2  17049  perfcls  17056  ordthaus  17075  cmpcov2  17080  cmpsub  17090  hauscmplem  17096  cmpfi  17098  iscon2  17103  dfcon2  17108  is1stc2  17131  is2ndc  17135  1stcelcls  17150  1stccn  17152  llyi  17163  subislly  17170  iskgen3  17207  txuni2  17223  ptpjpre1  17229  ptbasin  17235  tx1cn  17266  tx2cn  17267  uptx  17282  txdis1cn  17292  ptrescn  17296  txtube  17297  txcmplem1  17298  hausdiag  17302  txkgen  17309  xkohaus  17310  xkococnlem  17316  xkoinjcn  17344  qtopeu  17370  isr0  17391  regr1lem2  17394  hmphsym  17436  elmptrab2  17486  isfbas  17487  isfbas2  17493  trfbas  17502  snfil  17522  fbunfip  17527  elfg  17529  fgcl  17536  fbasrn  17542  filuni  17543  trfil2  17545  cfinfil  17551  csdfil  17552  supfil  17553  ufinffr  17587  rnelfmlem  17610  elflim2  17622  hausflim  17639  hauspwpwf1  17645  txflf  17664  isfcls2  17671  fclsopn  17672  fclsrest  17682  alexsubALTlem2  17705  alexsubALTlem3  17706  alexsubALTlem4  17707  tmdcn2  17735  divstgplem  17766  divstgphaus  17768  tsmssubm  17788  istdrg2  17823  metn0  17887  prdsxmetlem  17895  imasdsf1olem  17900  xpsdsval  17908  blres  17940  xmeterval  17941  xmeter  17942  isxms2  17957  isms2  17959  dscopn  18059  isngp3  18083  isnvc2  18172  isnghm  18195  qtopbaslem  18230  xrtgioo  18275  zcld  18282  elii1  18396  pi1cpbl  18505  tchcph  18630  cmetss  18703  bcth  18714  lssbn  18736  ishl2  18750  minveclem3b  18755  minveclem6  18761  pmltpc  18773  ovolfcl  18789  ovolgelb  18802  ovolunlem1  18819  ovoliunlem1  18824  ismbl  18848  ismbl2  18849  iundisj2  18869  dyadmax  18916  dyadmbllem  18917  vitalilem2  18927  mbfimaopnlem  18973  itg1climres  19032  itg2l  19047  itg2leub  19052  iblcnlem1  19105  ellimc2  19190  ellimc3  19192  limcmpt  19196  limcres  19199  elaa  19659  aaliou3lem9  19693  taylthlem2  19716  ulmcau  19735  pilem1  19790  sincosq1lem  19828  sineq0  19852  coseq1  19853  ellogrn  19880  logtayl2  19972  cxpcn3lem  20050  cxpcn3  20051  cubic  20108  atandm  20135  atandm2  20136  atandm4  20138  atans2  20190  xrlimcnp  20226  wilthlem2  20270  dvdsflsumcom  20391  dvdsmulf1o  20397  fsumvma  20415  logfac2  20419  dchrelbas2  20439  dchrelbas3  20440  lgsdir2lem4  20528  lgsquadlem1  20556  lgsquadlem2  20557  2sqlem1  20565  pntlem3  20721  ostth  20751  avril1  20797  grpoidinvlem3  20834  issubgo  20931  elghom  20991  islno  21292  nmoubi  21311  nmobndseqi  21318  siii  21392  minvecolem5  21421  minvecolem6  21422  hvsubaddi  21606  normsub0i  21675  bcsiALT  21719  hcau  21724  hlimadd  21733  hhcmpl  21740  hhcms  21743  issh2  21749  isch2  21764  hlim0  21776  isch3  21782  norm1exi  21790  elch0  21794  hhsssh2  21808  choc0  21866  pjhtheu  21934  pjpreeq  21938  omlsilem  21942  pjoc2i  21978  chsscon1i  22002  spanuni  22084  h1deoi  22089  h1dei  22090  elspansni  22098  cmcm4i  22135  cmbr3i  22140  cmbr4i  22141  osumcor2i  22184  5oalem7  22200  3oalem3  22204  pjss2i  22220  mayete3iOLD  22269  elcnop  22398  ellnop  22399  elhmop  22414  elcnfn  22423  ellnfn  22424  cnvadj  22433  nmopub  22449  nmfnleub  22466  eleigvec  22498  nmop0  22527  nmfn0  22528  nmopun  22555  lncnopbd  22578  riesz2  22607  nmopcoadj0i  22644  rnbra  22648  pjnmopi  22689  pjssdif1i  22716  pjin2i  22734  pjin3i  22735  pjclem1  22736  cvbr2  22824  cvnbtwn3  22829  cvnbtwn4  22830  mdsl2bi  22864  mdsldmd1i  22872  elat2  22881  chrelat2i  22906  atomli  22923  chirredi  22935  mdsymlem6  22949  mdsymlem8  22951  sumdmdii  22956  dmdbr5ati  22963  cdj3i  22982  xfree2  22986  ballotlemelo  23008  ballotlem2  23009  ballotlemfmpn  23015  ballotlemodife  23018  ballotlem4  23019  ballotth  23058  eldmgm  23067  subfacp1lem5  23088  subfacp1lem6  23089  cvmscld  23177  cvmlift2lem12  23218  vdgrun  23266  eupath  23278  ghomgrpilem2  23366  axextprim  23420  axrepprim  23421  axunprim  23422  axpowprim  23423  axregprim  23424  axinfprim  23425  axacprim  23426  untangtr  23433  biimpexp  23443  divelunit  23452  dftr6  23479  coep  23480  coepr  23481  dffr5  23482  dfpo2  23484  cnvco1  23489  cnvco2  23490  fundmpss  23492  dfdm5  23502  dfrn5  23503  elpotr  23507  dford5reg  23508  dfon2lem5  23513  dfon2lem6  23514  dfon2lem8  23516  dfon2lem9  23517  dfon2  23518  wfi  23577  eltrpred  23599  frind  23613  poseq  23623  soseq  23624  wfrlem4  23629  wfrlem5  23630  wfrlem9  23634  wfrlem11  23636  wfrlem12  23637  wfrlem13  23638  wfrlem14  23639  wfrlem15  23640  tfrALTlem  23646  tfr3ALT  23649  frrlem5  23655  frrlem5e  23659  frrlem11  23663  nosgnn0  23681  axdenselem5  23709  axfelem12  23727  axfelem15  23730  axfelem18  23733  axfelem22  23737  elsymdif  23744  brsymdif  23749  brtxp  23797  brpprod  23802  brpprod3b  23804  brsset  23806  idsset  23807  dfon3  23809  brtxpsd  23811  brtxpsd2  23812  brbigcup  23815  elfix  23820  dffix2  23822  ellimits  23827  elfuns  23830  snelsingles  23837  dfiota3  23838  brcart  23847  brimg  23852  brapply  23853  brcup  23854  brcap  23855  brsuccf  23856  funpartfun  23857  fullfunfnv  23860  brrestrict  23863  dfrdg4  23864  tfrqfree  23865  altopthsn  23871  altopelaltxp  23886  altxpsspw  23887  mptelee  23899  brbtwn2  23909  colinearalg  23914  ax5seg  23942  axpasch  23945  axlowdimlem6  23951  axlowdimlem13  23958  axeuclidlem  23966  axeuclid  23967  axcontlem3  23970  axcontlem4  23971  axcontlem12  23979  brcolinear2  24057  broutsideof  24120  outsideofcom  24127  fvray  24140  fvline  24143  lineunray  24146  linecom  24149  linerflx2  24150  ellines  24151  bpoly2  24168  bpoly3  24169  rankeq1o  24177  elhf  24180  elhf2  24181  r19.26-2a  24301  eeeeanv  24311  altdftru  24315  pm11.53g  24331  eqvinopb  24332  copsexgb  24333  ltl4ev  24359  albineal  24366  evevifev  24381  cnvref  24432  restidsing  24443  dffn5a  24498  repcpwti  24529  dfdir2  24659  apnei  24888  ismonc  25182  isepic  25192  isfunb  25203  issubcata  25214  isntr  25241  clscnc  25378  bisig0  25430  isconcl5a  25469  isconcl5ab  25470  isibg2  25478  bosser  25535  hpd  25537  ecase13d  25590  cnvresimaOLD  25594  trer  25595  elicc3  25596  finminlem  25599  opnrebl  25603  nn0prpw  25607  clsun  25614  fneval  25655  fnessref  25661  neibastop1  25676  neifg  25688  filnetlem4  25698  f1opr  25759  inixp  25767  sdclem2  25820  sdclem1  25821  fdc  25823  neificl  25835  istotbnd3  25863  sstotbnd3  25868  isbndx  25874  isbnd3b  25877  cntotbnd  25888  heibor1lem  25901  heibor1  25902  isdrngo2  25957  isdrngo3  25958  iscrngo2  25991  smprngopr  26045  isdmn2  26048  isfldidl2  26062  ispridlc  26063  isdmn3  26067  an43OLD  26081  prtlem70  26083  prtlem100  26089  n0el  26093  prter2  26117  funsnfsup  26130  cmpfiiin  26140  isnacs2  26149  elmzpcl  26172  diophrex  26223  2sbcrex  26232  sbcrot3  26236  sbcrot5  26237  3rexfrabdioph  26246  4rexfrabdioph  26247  6rexfrabdioph  26248  7rexfrabdioph  26249  ftp  26261  fphpd  26267  fiphp3d  26270  rencldnfilem  26271  jm2.23  26457  expdiophlem1  26482  expdiophlem2  26483  expdioph  26484  dford4  26490  wopprc  26491  ttac  26497  fnwe2lem2  26516  islmodfg  26535  islnm2  26544  lnmlmic  26554  uvcvv0  26607  isnumbasgrplem1  26634  dfacbasgrp  26641  islinds2  26651  lmiclbs  26675  islnr2  26686  islnr3  26687  f1omvdco3  26760  matrcl  26834  issdrg2  26874  sdrgacs  26877  phisum  26886  isdomn3  26891  pm10.541  26930  pm10.542  26931  19.21vv  26942  19.36vv  26949  19.31vv  26950  19.37vv  26951  19.28vv  26952  pm11.6  26959  pm11.62  26961  pm14.12  26990  elnev  27007  evth2f  27055  elunif  27056  evthf  27067  stoweidlem14  27132  stoweidlem24  27142  stoweidlem31  27149  stoweidlem34  27152  stoweidlem37  27155  stoweidlem51  27169  stoweidlem54  27172  stoweidlem57  27175  stoweidlem59  27177  aiffnbandciffatnotciffb  27221  mdandyvr0  27259  mdandyvr1  27260  mdandyvr2  27261  mdandyvr3  27262  mdandyvr4  27263  mdandyvr5  27264  mdandyvr6  27265  mdandyvr7  27266  mdandyvr8  27267  mdandyvr9  27268  mdandyvr10  27269  mdandyvr11  27270  mdandyvr12  27271  mdandyvr13  27272  mdandyvr14  27273  mdandyvr15  27274  rexrsb  27296  2rexsb  27297  2rexrsb  27298  cbvral2  27299  cbvrex2  27300  2ralbiim  27301  2reu5a  27304  rmoanim  27306  2rmoswap  27311  2reu1  27313  2reu3  27315  2reu4a  27316  gte-lteh  27329  gt-lth  27330  sgnn  27384  onfrALTlem5  27443  onfrALTlem4  27444  onfrALTlem1  27449  2uasbanh  27463  dfvd2  27484  dfvd2an  27487  dfvd3  27496  dfvd3an  27499  eelT00  27613  eelTTT  27614  eelT12  27619  uunT1  27688  uunT1p1  27689  uun132p1  27694  un2122  27698  uunTT1p1  27702  uunTT1p2  27703  uunT11p1  27705  uunT11p2  27706  uunT12  27707  uunT12p1  27708  uunT12p2  27709  uunT12p3  27710  uunT12p4  27711  uunT12p5  27712  uun2221  27721  uun2221p1  27722  uun2221p2  27723  undif3VD  27791  onfrALTlem5VD  27794  onfrALTlem4VD  27795  onfrALTlem1VD  27799  2uasbanhVD  27820  bnj170  27855  bnj248  27857  bnj251  27859  bnj256  27863  bnj258  27865  bnj291  27868  bnj422  27872  bnj432  27873  bnj23  27876  bnj89  27879  bnj132  27884  bnj156  27888  bnj158  27889  bnj538  27901  bnj563  27904  bnj945  27937  bnj946  27938  bnj976  27941  bnj1098  27947  bnj1138  27952  bnj1209  27961  bnj1476  28011  bnj1542  28021  bnj110  28022  bnj91  28025  bnj92  28026  bnj106  28032  bnj118  28033  bnj124  28035  bnj125  28036  bnj153  28044  bnj207  28045  bnj222  28047  bnj518  28050  bnj535  28054  bnj539  28055  bnj543  28057  bnj553  28062  bnj556  28064  bnj558  28066  bnj571  28070  bnj605  28071  bnj591  28075  bnj594  28076  bnj580  28077  bnj609  28081  bnj611  28082  bnj865  28087  bnj849  28089  bnj882  28090  bnj916  28097  bnj917  28098  bnj934  28099  bnj929  28100  bnj944  28102  bnj953  28103  bnj1000  28105  bnj969  28110  bnj970  28111  bnj978  28113  bnj983  28115  bnj984  28116  bnj985  28117  bnj986  28118  bnj1021  28128  bnj1033  28131  bnj1049  28136  bnj1052  28137  bnj1083  28140  bnj1112  28145  bnj1030  28149  bnj1137  28157  bnj1189  28171  bnj1204  28174  bnj1253  28179  bnj1279  28180  bnj1373  28192  bnj1388  28195  bnj1398  28196  bnj1450  28212  19.8vK  28254  equextvK  28323  equvelv  28366  a12study4  28367  a12study8  28369  a12peros  28371  a12lem2  28381  a12study10  28386  a12study10n  28387  lsateln0  28435  islshpat  28457  lcvbr2  28462  lcvbr3  28463  lcvnbtwn3  28468  islfl  28500  lshpsmreu  28549  lub0N  28629  glb0N  28633  cvrnbtwn3  28716  leat2  28734  isat3  28747  iscvlat2N  28764  ishlat2  28793  ishlat3N  28794  hlrelat5N  28840  hlrelat2  28842  3dim0  28896  2dim  28909  islpln5  28974  islvol5  29018  4atlem3  29035  dalem20  29132  ispsubsp2  29185  snatpsubN  29189  pmapglb  29209  elpadd  29238  paddasslem17  29275  dalawlem13  29322  pclfinN  29339  polval2N  29345  pclfinclN  29389  lhpex2leN  29452  isltrn2N  29559  cdleme0nex  29729  cdleme22b  29780  cdlemftr3  30004  tendoset  30198  diarnN  30569  dibopelvalN  30583  dibopelval2  30585  dibelval3  30587  diblsmopel  30611  dicelval3  30620  dihglb2  30782  doch11  30813  islpolN  30923  lcfls1N  30975  mapdval4N  31072  mapdrvallem2  31085
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10
This theorem depends on definitions:  df-bi 179
  Copyright terms: Public domain W3C validator