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  exsb  2093  2exsb  2094  eujust  2119  euf  2123  cbveu  2136  eu2  2141  mo2  2145  sbmo  2146  mo3  2147  mo4f  2148  eu4  2155  moanim  2172  2mo  2194  2mos  2195  2eu1  2196  2eu3  2198  2eu4  2199  2eu6  2201  exists1  2205  abid  2244  eleq12i  2321  abeq2  2361  abeq2i  2363  clabel  2377  abid2f  2417  sbabel  2418  neeq12i  2431  necon1abii  2470  neanior  2504  ralnex  2524  rexnal  2525  ralinexa  2559  rexanali  2560  r3al  2571  r19.26-2  2647  ralbiim  2651  r19.30  2656  ralcomf  2669  rexcomf  2670  rexrot4  2674  reean  2677  3reeanv  2679  rabbi  2686  cbvralf  2712  cbvreu  2716  cbvral2v  2724  cbvrex2v  2725  cbvral3v  2726  cbvralsv  2727  cbvrexsv  2728  sbralie  2729  rabeq2i  2737  issetf  2745  2gencl  2768  3gencl  2769  ceqsex2  2775  ceqsex3v  2777  ceqsex6v  2779  ceqsex8v  2780  gencbvex  2781  cla43gv  2824  eqvincf  2847  ceqsrex2v  2854  elrab2  2876  ralab  2877  ralrab  2878  rexab  2879  rexrab  2880  ralab2  2881  rexab2  2883  eueq3  2891  morex  2900  euxfr2  2901  euxfr  2902  euind  2903  reu2  2906  reu6  2907  rmo4  2911  reu4  2912  reu7  2913  2reuswap  2916  reuind  2917  sbcco  2957  sbccomlem  3005  sbccom  3006  ra5  3019  rmo3  3020  csbco  3032  sbnfc2  3083  csbabg  3084  cbvralcsf  3085  cbvreucsf  3087  dfss  3109  dfss2f  3113  ss2ab  3183  dfpss2  3203  dfpss3  3204  psseq12i  3209  sspsstri  3220  difeqri  3238  uneqri  3259  ssequn2  3290  unss  3291  rexun  3297  ralunb  3298  elin2  3301  ineqri  3304  dfss1  3315  dfss5  3316  nsspssun  3344  indifdir  3367  inrab2  3383  rabun2  3389  reuun2  3393  eq0  3411  0el  3413  abn0  3415  0pss  3434  disjr  3438  disj1  3439  disjpss  3447  undif4  3453  difin0ss  3462  inssdif0  3463  uneqdifeq  3484  r19.3rz  3487  r19.3rzv  3489  ralidm  3499  pwss  3580  dfpr2  3597  ralsns  3611  rexsns  3612  eltpg  3617  ralprg  3623  rexprg  3624  raltpg  3625  rextpg  3626  euabsn2  3639  eusn  3644  eldifsn  3690  rexdifsn  3694  difsnpss  3699  pwpw0  3704  ssunsn  3715  eqsn  3716  sstp  3719  tpss  3720  prel12  3730  preqsn  3733  pwsnALT  3763  pwtp  3765  eluniab  3780  elunirab  3781  unipr  3782  dfnfc2  3786  uniun  3787  uniin  3788  unissb  3798  elintab  3814  elintrab  3815  ssintab  3820  ssintrab  3826  intun  3835  intpr  3836  elrint  3844  iuncom4  3853  iuneq2  3862  dfiun2g  3876  ssiinf  3892  elriin  3915  iunxiun  3925  pwssb  3929  iunpwss  3932  disjor  3947  disjors  3949  disjiun  3953  disjxiun  3960  disjxun  3961  cbvopab1  4029  dftr5  4056  trint  4068  inex1  4095  inuni  4115  axpweq  4125  nfnid  4142  zfpair2  4153  moabex  4170  exss  4173  elop  4176  otth  4187  copsex4g  4192  opeqsn  4199  opthwiener  4205  opelopabsbOLD  4210  brabga  4216  opelopabaf  4225  opabn0  4232  iunopab  4233  pwunss  4235  pwundifOLD  4238  dfid3  4247  pocl  4258  sotric  4277  isso2i  4283  somo  4285  frminex  4310  dfepfr  4315  wefrc  4324  ordtri3or  4361  ordtri2  4364  elsuci  4395  elsucg  4396  sucel  4402  on0eqel  4447  uniuni  4464  reusv2lem4  4475  reusv2lem5  4476  reusv2  4477  reusv3  4479  reuxfr2d  4494  elpwun  4504  iunpw  4507  dfwe2  4510  onintrab2  4530  ordpwsuc  4543  ordzsl  4573  dflim4  4576  tfindsg  4588  tfindes  4590  findsg  4620  elxp  4659  opelxp  4672  brxp  4673  rabxp  4678  opthprc  4689  brab2a  4691  opeliunxp  4693  xpundi  4694  xpundir  4695  elvvv  4702  brinxp  4705  brab2ga  4716  xp0r  4721  eqrelrel  4741  reliun  4759  reluni  4761  raliunxp  4778  rexiunxp  4779  ralxpf  4783  rexxpf  4784  iunxpf  4785  relop  4787  elcnv  4811  elcnv2  4812  dmin  4839  dmuni  4841  dmopab  4842  dmi  4846  rnopab  4877  elrnmpt1  4881  rncoeq  4901  resiexg  4950  dfima2  4967  dfima3  4968  elima2  4971  elima3  4972  imai  4980  elimasn  4991  epini  4996  dfse2  4999  cotr  5008  issref  5009  intasym  5011  asymref  5012  asymref2  5013  somin1  5032  cnvopab  5036  cnvi  5038  cnvdif  5040  imainss  5049  dfrel2  5077  dfrel3  5083  rnsnn0  5091  relsn2  5095  dmsnopg  5096  cnvcnvsn  5102  elxp4  5112  elxp5  5113  cnvresima  5114  mptpreima  5118  dfco2  5124  coundi  5126  coundir  5127  imaco  5130  coiun  5134  coi1  5140  relssdmrn  5145  relrelss  5148  ressn  5163  cnviin  5164  cnvpo  5165  dffun2  5169  dffun3  5170  dffun4  5171  dffun5  5172  dffun7  5184  dffun8  5185  dffun9  5186  funopab  5191  funun  5199  funcnvsn  5200  funcnv2  5212  funcnv  5213  fun2cnv  5215  fncnv  5217  fun11  5218  fununi  5219  imadif  5230  funimaexg  5232  fnunsn  5254  fnres  5263  fnopabg  5270  mptfng  5272  mptun  5277  fun  5308  fresaunres1  5317  fcnvres  5321  dff12  5339  f1cnvcnv  5348  funforn  5361  dff1o2  5380  dff1o5  5384  f1orn  5385  resdif  5397  ffoss  5408  f11o  5409  f1o00  5411  fo00  5412  elfv  5421  fv3  5439  dffn5f  5476  dffv2  5491  eqfnfv3  5523  fndmdifeq0  5530  fneqeql  5532  unpreima  5550  respreima  5553  dff4  5573  dffo3  5574  dffo5  5576  f1ompt  5581  ffnfvf  5585  fmptco  5590  fsn2  5597  fconst3  5634  fconst4  5635  idref  5658  abrexco  5665  opabex3  5668  abexssex  5680  dff13  5682  dff13f  5683  f1mpt  5684  foeqcnvco  5703  isocnv3  5728  isoini  5734  weniso  5751  oprabid  5781  dfoprab2  5794  eqoprab2b  5805  dmoprab  5827  rnoprab  5829  eloprabga  5833  mpt2mptx  5837  resoprab  5839  ffnov  5847  fnov  5851  elrnmpt2  5856  ralrnmpt2  5857  rexrnmpt2  5858  oprabex3  5861  oprabrexex2  5862  ovid  5863  ov3  5883  ov6g  5884  foov  5893  ndmovdistr  5908  difxp  6052  elopaba  6081  fmpt2  6090  curry1  6109  curry2  6112  fsplit  6122  frxp  6124  xporderlem  6125  soxp  6127  brtpos2  6139  dmtpos  6145  tpostpos  6153  tpossym  6165  tposoprab  6169  sorpsscmpl  6187  cbviota  6195  opiota  6221  eusvobj2  6270  dfsmo2  6297  tfrlem3  6326  tfrlem7  6332  tfrlem9  6334  tfrlem9a  6335  tz7.48lem  6386  tz7.49c  6391  el1o  6431  dif1o  6432  ondif2  6434  brwitnlem  6439  oarec  6493  omeulem1  6513  omeu  6516  oeordi  6518  oeeui  6533  oeeu  6534  omopthlem1  6586  dfer2  6594  brdifun  6620  swoso  6624  eqerlem  6625  qsid  6658  iiner  6664  erinxp  6666  brecop  6684  eroveu  6686  erovlem  6687  ecopovsym  6693  mapval2  6730  mapsn  6742  elixp  6756  ixpeq2  6763  ixpin  6774  ixpiin  6775  mptelixpg  6786  ixpsnf1o  6789  boxriin  6791  domen  6808  isfi  6818  en1  6861  xpsnen  6879  xpcomco  6885  xpassen  6889  sbthlem9  6912  0sdomg  6923  2pwuninel  6949  ssenen  6968  nneneq  6977  php  6978  modom2  6997  ac6sfi  7034  frfi  7035  fimaxg  7037  elfpw  7090  fissuni  7093  dffi3  7117  marypha1lem  7119  marypha2lem2  7122  dfsup2  7128  dfsup2OLD  7129  wofib  7193  wemapso2lem  7198  wdom2d  7227  unxpwdom2  7235  dford2  7254  inf2  7257  inf3lem2  7263  axinf2  7274  zfinf2  7276  cantnfp1lem2  7314  oemapso  7317  cantnflem1  7324  trcl  7343  epfrs  7346  rankvalb  7402  r1elss  7411  unbndrank  7447  scott0s  7491  cplem1  7492  bnd2  7496  isnum2  7511  iscard2  7542  infxpenlem  7574  fseqenlem1  7584  acnnum  7612  infpwfien  7622  alephnbtwn2  7632  alephord2  7636  alephislim  7643  cardaleph  7649  alephval3  7670  aceq1  7677  aceq2  7679  dfac3  7681  dfac4  7682  dfac5lem1  7683  dfac5lem2  7684  dfac5lem3  7685  dfac5lem4  7686  dfac5lem5  7687  dfac2  7690  dfac0  7692  dfac1  7693  dfac8  7694  dfac9  7695  dfac12  7708  kmlem3  7711  kmlem4  7712  kmlem7  7715  kmlem8  7716  kmlem9  7717  kmlem13  7721  kmlem14  7722  kmlem15  7723  dfackm  7725  pwsdompw  7763  ackbij2lem2  7799  cf0  7810  cfval2  7819  cflim2  7822  cfss  7824  cfslb  7825  isfin3  7855  isfin5  7858  isfin6  7859  sdom2en01  7861  fin23lem25  7883  fin23lem26  7884  fin23lem40  7910  isfin1-2  7944  isfin1-3  7945  fin1a2lem5  7963  fin1a2lem6  7964  fin1a2lem12  7970  fin12  7972  domtriomlem  8001  axdc2lem  8007  axdc3lem2  8010  axdc3lem4  8012  axcclem  8016  ac6num  8039  ac9  8043  ac6n  8045  ac9s  8053  zorn2lem6  8061  zornn0g  8065  ttukeylem6  8074  ttukey2g  8076  brdom7disj  8089  brdom6disj  8090  iunfo  8094  iundom2g  8095  konigthlem  8123  alephsuc3  8135  elgch  8177  fpwwe2lem9  8193  fpwwe2lem12  8196  fpwwe2lem13  8197  fpwwe2  8198  canth4  8202  canthwe  8206  wunex2  8293  uniwun  8295  axgroth5  8379  grothpw  8381  axgroth6  8383  grothprimlem  8388  grothprim  8389  elni  8433  ltexpi  8459  nqerf  8487  nqerid  8490  ordpipq  8499  recmulnq  8521  npomex  8553  genpnnp  8562  genpass  8566  addcompr  8578  mulcompr  8580  reclem2pr  8605  reclem3pr  8606  ltsosr  8649  ltasr  8655  mappsrpr  8663  map2psrpr  8665  opelcn  8684  elreal  8686  elreal2  8687  axaddf  8700  axmulf  8701  axicn  8705  axrrecex  8718  axpre-mulgt0  8723  xrlenlt  8823  ssxr  8825  leloe  8841  msq0i  9348  infm3  9646  supmullem2  9654  inelr  9669  arch  9894  elnnne0  9911  un0addcl  9929  un0mulcl  9930  elnnz  9966  elznn0nn  9969  elznn0  9970  elznn  9971  elz2  9972  raluz2  10200  rexuz2  10202  nnwos  10218  eluz2b2  10222  eluz2b3  10223  ublbneg  10234  zmin  10244  elq  10250  ralrp  10304  rexrp  10305  ltxr  10389  xrnemnf  10392  xrleloe  10410  xrltlen  10412  xrrebnd  10429  xaddf  10482  xmullem  10515  xmullem2  10516  xrsupss  10558  xrinfmss  10559  elfzp1  10767  fzprval  10775  fztpval  10776  fzm1  10793  fzolb  10811  fzolb2  10812  elfzo3  10821  fzouzsplit  10832  fzo0n0  10836  fzind2  10854  uzrdgfni  10952  subsq0i  11147  crreczi  11157  nn0le2msqi  11213  nn0opth2i  11217  hashkf  11270  hashfun  11319  hashbclem  11320  hashbc  11321  hashf1lem2  11324  leiso  11327  iswrd  11345  climeu  11959  lo1resb  11968  rlimresb  11969  o1resb  11970  climmpt2  11977  fsum2dlem  12163  rpnnen2  12431  sqr2irr  12454  divides  12460  odd2np1  12514  divalglem1  12520  divalglem6  12524  divalglem10  12528  divalgb  12530  bitsval2  12543  bitsmod  12554  bitscmp  12556  smueqlem  12608  isprm2  12693  isprm3  12694  isprm4  12695  isprm5  12718  pythagtriplem19  12813  pythagtrip  12814  pceu  12826  prmreclem2  12891  4sqlem2  12923  4sqlem12  12930  vdwpc  12954  vdwnn  12972  dec5dvds2  13007  pwsle  13318  imasleval  13370  xpsfrnel  13392  xpsfrnel2  13394  xpsle  13410  isacs2  13482  mreacs  13487  iscatd2  13510  comfeq  13536  oppcsect  13603  isssc  13624  isfunc  13665  funcoppc  13676  isffth2  13717  fucinv  13774  elhoma  13791  setcinv  13849  ispos  14008  ispos2  14009  tosso  14069  istsr2  14254  spwmo  14262  ismnd  14296  mndcl  14299  issubm  14352  gsumwspan  14395  issubg  14548  isnsg2  14574  eqger  14594  isgim2  14656  giclcl  14663  gicrcl  14664  gicsubgen  14669  gaorber  14689  resscntz  14734  cntzrec  14736  efgval2  14960  efgsfo  14975  efgrelexlemb  14986  isabl2  15024  iscyggen2  15095  iscyg2  15096  iscyg3  15100  lt6abl  15108  gsumval3eu  15117  gsum2d2  15152  dmdprdd  15164  subgdmdprd  15196  iscrng2  15283  dvdsrtr  15361  isunit  15366  isnirred  15409  isirred2  15410  isrhm  15428  isdrng2  15449  drngprop  15450  isabv  15511  issrng  15542  islmod  15558  islss  15619  lss1d  15647  islmim2  15746  lmiclcl  15750  lmicrcl  15751  lsmelval2  15765  lspsolvlem  15822  lspsncv0  15826  islpidl  15925  islpir2  15930  isnzr2  15942  isdomn2  15967  fiidomfld  15976  aspval2  16013  mplcoe1  16136  mplcoe2  16138  evlslem4  16172  xrsdsreclb  16345  unocv  16507  iunocv  16508  ishil2  16546  isobs  16547  obselocv  16555  iinopn  16575  istps4OLD  16588  istps5OLD  16589  istps  16601  istps2  16602  isbasis2g  16613  tgval2  16621  elcls  16737  islpi  16807  isperf2  16810  isperf3  16811  restntr  16839  ordtbaslem  16845  ordtrest2lem  16860  cnrest  16940  ist0-3  17000  ist1-2  17002  ist1-3  17004  nrmsep3  17010  isnrm2  17013  perfcls  17020  ordthaus  17039  cmpcov2  17044  cmpsub  17054  hauscmplem  17060  cmpfi  17062  iscon2  17067  dfcon2  17072  is1stc2  17095  is2ndc  17099  1stcelcls  17114  1stccn  17116  llyi  17127  subislly  17134  iskgen3  17171  txuni2  17187  ptpjpre1  17193  ptbasin  17199  tx1cn  17230  tx2cn  17231  uptx  17246  txdis1cn  17256  ptrescn  17260  txtube  17261  txcmplem1  17262  hausdiag  17266  txkgen  17273  xkohaus  17274  xkococnlem  17280  xkoinjcn  17308  qtopeu  17334  isr0  17355  regr1lem2  17358  hmphsym  17400  elmptrab2  17450  isfbas  17451  isfbas2  17457  trfbas  17466  snfil  17486  fbunfip  17491  elfg  17493  fgcl  17500  fbasrn  17506  filuni  17507  trfil2  17509  cfinfil  17515  csdfil  17516  supfil  17517  ufinffr  17551  rnelfmlem  17574  elflim2  17586  hausflim  17603  hauspwpwf1  17609  txflf  17628  isfcls2  17635  fclsopn  17636  fclsrest  17646  alexsubALTlem2  17669  alexsubALTlem3  17670  alexsubALTlem4  17671  tmdcn2  17699  divstgplem  17730  divstgphaus  17732  tsmssubm  17752  istdrg2  17787  metn0  17851  prdsxmetlem  17859  imasdsf1olem  17864  xpsdsval  17872  blres  17904  xmeterval  17905  xmeter  17906  isxms2  17921  isms2  17923  dscopn  18023  isngp3  18047  isnvc2  18136  isnghm  18159  qtopbaslem  18194  xrtgioo  18239  zcld  18246  elii1  18360  pi1cpbl  18469  tchcph  18594  cmetss  18667  bcth  18678  lssbn  18700  ishl2  18714  minveclem3b  18719  minveclem6  18725  pmltpc  18737  ovolfcl  18753  ovolgelb  18766  ovolunlem1  18783  ovoliunlem1  18788  ismbl  18812  ismbl2  18813  iundisj2  18833  dyadmax  18880  dyadmbllem  18881  vitalilem2  18891  mbfimaopnlem  18937  itg1climres  18996  itg2l  19011  itg2leub  19016  iblcnlem1  19069  ellimc2  19154  ellimc3  19156  limcmpt  19160  limcres  19163  elaa  19623  aaliou3lem9  19657  taylthlem2  19680  ulmcau  19699  pilem1  19754  sincosq1lem  19792  sineq0  19816  coseq1  19817  ellogrn  19844  logtayl2  19936  cxpcn3lem  20014  cxpcn3  20015  cubic  20072  atandm  20099  atandm2  20100  atandm4  20102  atans2  20154  xrlimcnp  20190  wilthlem2  20234  dvdsflsumcom  20355  dvdsmulf1o  20361  fsumvma  20379  logfac2  20383  dchrelbas2  20403  dchrelbas3  20404  lgsdir2lem4  20492  lgsquadlem1  20520  lgsquadlem2  20521  2sqlem1  20529  pntlem3  20685  ostth  20715  avril1  20761  grpoidinvlem3  20798  issubgo  20895  elghom  20955  islno  21256  nmoubi  21275  nmobndseqi  21282  siii  21356  minvecolem5  21385  minvecolem6  21386  hvsubaddi  21570  normsub0i  21639  bcsiALT  21683  hcau  21688  hlimadd  21697  hhcmpl  21704  hhcms  21707  issh2  21713  isch2  21728  hlim0  21740  isch3  21746  norm1exi  21754  elch0  21758  hhsssh2  21772  choc0  21830  omlsilem  21906  pjoc2i  21942  chsscon1i  21966  spanuni  22048  h1deoi  22053  h1dei  22054  elspansni  22062  cmcm4i  22117  cmbr3i  22122  cmbr4i  22123  osumcor2i  22166  5oalem7  22182  3oalem3  22186  pjss2i  22202  mayete3iOLD  22251  elcnop  22362  ellnop  22363  elhmop  22378  elcnfn  22387  ellnfn  22388  cnvadj  22397  nmopub  22413  nmfnleub  22430  eleigvec  22462  nmop0  22491  nmfn0  22492  nmopun  22519  lncnopbd  22542  riesz2  22571  nmopcoadj0i  22608  rnbra  22612  pjnmopi  22653  pjssdif1i  22680  pjin2i  22698  pjin3i  22699  pjclem1  22700  cvbr2  22788  cvnbtwn3  22793  cvnbtwn4  22794  mdsl2bi  22828  mdsldmd1i  22836  elat2  22845  chrelat2i  22870  atomli  22887  chirredi  22899  mdsymlem6  22913  mdsymlem8  22915  sumdmdii  22920  dmdbr5ati  22927  cdj3i  22946  xfree2  22950  ballotlemelo  22972  ballotlem2  22973  ballotlemfmpn  22979  ballotlemodife  22982  ballotlem4  22983  ballotth  23022  eldmgm  23031  subfacp1lem5  23052  subfacp1lem6  23053  cvmscld  23141  cvmlift2lem12  23182  vdgrun  23230  eupath  23242  ghomgrpilem2  23330  axextprim  23384  axrepprim  23385  axunprim  23386  axpowprim  23387  axregprim  23388  axinfprim  23389  axacprim  23390  untangtr  23397  biimpexp  23407  divelunit  23416  dftr6  23443  coep  23444  coepr  23445  dffr5  23446  dfpo2  23448  cnvco1  23453  cnvco2  23454  fundmpss  23456  dfdm5  23466  dfrn5  23467  elpotr  23471  dford5reg  23472  dfon2lem5  23477  dfon2lem6  23478  dfon2lem8  23480  dfon2lem9  23481  dfon2  23482  wfi  23541  eltrpred  23563  frind  23577  poseq  23587  soseq  23588  wfrlem4  23593  wfrlem5  23594  wfrlem9  23598  wfrlem11  23600  wfrlem12  23601  wfrlem13  23602  wfrlem14  23603  wfrlem15  23604  tfrALTlem  23610  tfr3ALT  23613  frrlem5  23619  frrlem5e  23623  frrlem11  23627  nosgnn0  23645  axdenselem5  23673  axfelem12  23691  axfelem15  23694  axfelem18  23697  axfelem22  23701  elsymdif  23708  brsymdif  23713  brtxp  23761  brpprod  23766  brpprod3b  23768  brsset  23770  idsset  23771  dfon3  23773  brtxpsd  23775  brtxpsd2  23776  brbigcup  23779  elfix  23784  dffix2  23786  ellimits  23791  elfuns  23794  snelsingles  23801  dfiota3  23802  brcart  23811  brimg  23816  brapply  23817  brcup  23818  brcap  23819  brsuccf  23820  funpartfun  23821  fullfunfnv  23824  brrestrict  23827  dfrdg4  23828  tfrqfree  23829  altopthsn  23835  altopelaltxp  23850  altxpsspw  23851  mptelee  23863  brbtwn2  23873  colinearalg  23878  ax5seg  23906  axpasch  23909  axlowdimlem6  23915  axlowdimlem13  23922  axeuclidlem  23930  axeuclid  23931  axcontlem3  23934  axcontlem4  23935  axcontlem12  23943  brcolinear2  24021  broutsideof  24084  outsideofcom  24091  fvray  24104  fvline  24107  lineunray  24110  linecom  24113  linerflx2  24114  ellines  24115  bpoly2  24132  bpoly3  24133  rankeq1o  24141  elhf  24144  elhf2  24145  r19.26-2a  24265  eeeeanv  24275  altdftru  24279  pm11.53g  24295  eqvinopb  24296  copsexgb  24297  ltl4ev  24323  albineal  24330  evevifev  24345  cnvref  24396  restidsing  24407  dffn5a  24462  repcpwti  24493  dfdir2  24623  apnei  24852  ismonc  25146  isepic  25156  isfunb  25167  issubcata  25178  isntr  25205  clscnc  25342  bisig0  25394  isconcl5a  25433  isconcl5ab  25434  isibg2  25442  bosser  25499  hpd  25501  ecase13d  25554  cnvresimaOLD  25558  trer  25559  elicc3  25560  finminlem  25563  opnrebl  25567  nn0prpw  25571  clsun  25578  fneval  25619  fnessref  25625  neibastop1  25640  neifg  25652  filnetlem4  25662  f1opr  25723  inixp  25731  sdclem2  25784  sdclem1  25785  fdc  25787  neificl  25799  istotbnd3  25827  sstotbnd3  25832  isbndx  25838  isbnd3b  25841  cntotbnd  25852  heibor1lem  25865  heibor1  25866  isdrngo2  25921  isdrngo3  25922  iscrngo2  25955  smprngopr  26009  isdmn2  26012  isfldidl2  26026  ispridlc  26027  isdmn3  26031  an43OLD  26045  prtlem70  26047  prtlem100  26053  n0el  26057  prter2  26081  funsnfsup  26094  cmpfiiin  26104  isnacs2  26113  elmzpcl  26136  diophrex  26187  2sbcrex  26196  sbcrot3  26200  sbcrot5  26201  3rexfrabdioph  26210  4rexfrabdioph  26211  6rexfrabdioph  26212  7rexfrabdioph  26213  ftp  26225  fphpd  26231  fiphp3d  26234  rencldnfilem  26235  jm2.23  26421  expdiophlem1  26446  expdiophlem2  26447  expdioph  26448  dford4  26454  wopprc  26455  ttac  26461  fnwe2lem2  26480  islmodfg  26499  islnm2  26508  lnmlmic  26518  uvcvv0  26571  isnumbasgrplem1  26598  dfacbasgrp  26605  islinds2  26615  lmiclbs  26639  islnr2  26650  islnr3  26651  f1omvdco3  26724  matrcl  26798  issdrg2  26838  sdrgacs  26841  phisum  26850  isdomn3  26855  pm10.541  26894  pm10.542  26895  19.21vv  26906  19.36vv  26913  19.31vv  26914  19.37vv  26915  19.28vv  26916  pm11.6  26923  pm11.62  26925  pm14.12  26954  elnev  26971  evth2f  27019  elunif  27020  evthf  27031  stoweidlem14  27063  stoweidlem24  27073  stoweidlem31  27080  stoweidlem34  27083  stoweidlem37  27086  stoweidlem51  27100  stoweidlem54  27103  stoweidlem57  27106  stoweidlem59  27108  aiffnbandciffatnotciffb  27126  mdandyvr0  27164  mdandyvr1  27165  mdandyvr2  27166  mdandyvr3  27167  mdandyvr4  27168  mdandyvr5  27169  mdandyvr6  27170  mdandyvr7  27171  mdandyvr8  27172  mdandyvr9  27173  mdandyvr10  27174  mdandyvr11  27175  mdandyvr12  27176  mdandyvr13  27177  mdandyvr14  27178  mdandyvr15  27179  gte-lteh  27208  gt-lth  27209  sgnn  27263  onfrALTlem5  27323  onfrALTlem4  27324  onfrALTlem1  27329  2uasbanh  27343  dfvd2  27364  dfvd2an  27367  dfvd3  27376  dfvd3an  27379  eelT00  27493  eelTTT  27494  eelT12  27499  uunT1  27568  uunT1p1  27569  uun132p1  27574  un2122  27578  uunTT1p1  27582  uunTT1p2  27583  uunT11p1  27585  uunT11p2  27586  uunT12  27587  uunT12p1  27588  uunT12p2  27589  uunT12p3  27590  uunT12p4  27591  uunT12p5  27592  uun2221  27601  uun2221p1  27602  uun2221p2  27603  undif3VD  27671  onfrALTlem5VD  27674  onfrALTlem4VD  27675  onfrALTlem1VD  27679  2uasbanhVD  27700  bnj170  27735  bnj248  27737  bnj251  27739  bnj256  27743  bnj258  27745  bnj291  27748  bnj422  27752  bnj432  27753  bnj23  27756  bnj89  27759  bnj132  27764  bnj156  27768  bnj158  27769  bnj538  27781  bnj563  27784  bnj945  27817  bnj946  27818  bnj976  27821  bnj1098  27827  bnj1138  27832  bnj1209  27841  bnj1476  27891  bnj1542  27901  bnj110  27902  bnj91  27905  bnj92  27906  bnj106  27912  bnj118  27913  bnj124  27915  bnj125  27916  bnj153  27924  bnj207  27925  bnj222  27927  bnj518  27930  bnj535  27934  bnj539  27935  bnj543  27937  bnj553  27942  bnj556  27944  bnj558  27946  bnj571  27950  bnj605  27951  bnj591  27955  bnj594  27956  bnj580  27957  bnj609  27961  bnj611  27962  bnj865  27967  bnj849  27969  bnj882  27970  bnj916  27977  bnj917  27978  bnj934  27979  bnj929  27980  bnj944  27982  bnj953  27983  bnj1000  27985  bnj969  27990  bnj970  27991  bnj978  27993  bnj983  27995  bnj984  27996  bnj985  27997  bnj986  27998  bnj1021  28008  bnj1033  28011  bnj1049  28016  bnj1052  28017  bnj1083  28020  bnj1112  28025  bnj1030  28029  bnj1137  28037  bnj1189  28051  bnj1204  28054  bnj1253  28059  bnj1279  28060  bnj1373  28072  bnj1388  28075  bnj1398  28076  bnj1450  28092  19.8vK  28134  equextvK  28203  equvelv  28246  a12study4  28247  a12study8  28249  a12peros  28251  a12lem2  28261  a12study10  28266  a12study10n  28267  lsateln0  28315  islshpat  28337  lcvbr2  28342  lcvbr3  28343  lcvnbtwn3  28348  islfl  28380  lshpsmreu  28429  lub0N  28509  glb0N  28513  cvrnbtwn3  28596  leat2  28614  isat3  28627  iscvlat2N  28644  ishlat2  28673  ishlat3N  28674  hlrelat5N  28720  hlrelat2  28722  3dim0  28776  2dim  28789  islpln5  28854  islvol5  28898  4atlem3  28915  dalem20  29012  ispsubsp2  29065  snatpsubN  29069  pmapglb  29089  elpadd  29118  paddasslem17  29155  dalawlem13  29202  pclfinN  29219  polval2N  29225  pclfinclN  29269  lhpex2leN  29332  isltrn2N  29439  cdleme0nex  29609  cdleme22b  29660  cdlemftr3  29884  tendoset  30078  diarnN  30449  dibopelvalN  30463  dibopelval2  30465  dibelval3  30467  diblsmopel  30491  dicelval3  30500  dihglb2  30662  doch11  30693  islpolN  30803  lcfls1N  30855  mapdval4N  30952  mapdrvallem2  30965
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