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  sbor  1958  sbrim  1959  sblim  1960  sban  1961  sbbi  1963  sblbis  1964  sbrbis  1965  sbrbif  1966  sbid2  1978  sbco2d  1981  sb8e  1987  19.23vv  2022  pm11.53  2024  19.41vv  2035  19.41vvv  2036  19.41vvvv  2037  19.42vv  2040  19.42vvv  2041  4exdistr  2044  cbvex4v  2053  eean  2054  sbnf2  2068  2sb5  2072  2sb6  2073  sbcom2  2074  sb6a  2076  2sb5rf  2077  2sb6rf  2078  sbex  2088  sbalv  2089  exsb  2090  2exsb  2091  eujust  2116  euf  2120  cbveu  2133  eu2  2138  mo2  2142  sbmo  2143  mo3  2144  mo4f  2145  eu4  2152  moanim  2169  2mo  2191  2mos  2192  2eu1  2193  2eu3  2195  2eu4  2196  2eu6  2198  exists1  2202  abid  2241  eleq12i  2318  abeq2  2354  abeq2i  2356  clabel  2370  abid2f  2410  sbabel  2411  neeq12i  2424  necon1abii  2463  neanior  2497  ralnex  2517  rexnal  2518  ralinexa  2550  rexanali  2551  r3al  2562  r19.26-2  2638  ralbiim  2642  r19.30  2647  ralcomf  2660  rexcomf  2661  rexrot4  2665  reean  2668  3reeanv  2670  rabbi  2677  cbvralf  2703  cbvreu  2707  cbvral2v  2711  cbvrex2v  2712  cbvral3v  2713  cbvralsv  2714  cbvrexsv  2715  sbralie  2716  rabeq2i  2724  issetf  2732  2gencl  2755  3gencl  2756  ceqsex2  2762  ceqsex3v  2764  ceqsex6v  2766  ceqsex8v  2767  gencbvex  2768  cla43gv  2810  eqvincf  2833  ceqsrex2v  2840  elrab2  2862  ralab  2863  ralrab  2864  rexab  2865  rexrab  2866  ralab2  2867  rexab2  2869  eueq3  2877  morex  2886  euxfr2  2887  euxfr  2888  euind  2889  reu2  2892  reu6  2893  rmo4  2897  reu4  2898  reu7  2899  2reuswap  2902  reuind  2903  sbcco  2943  sbccomlem  2991  sbccom  2992  ra5  3005  rmo3  3006  csbco  3018  sbnfc2  3069  csbabg  3070  cbvralcsf  3071  cbvreucsf  3073  dfss  3090  dfss2f  3094  ss2ab  3162  dfpss2  3182  dfpss3  3183  psseq12i  3188  sspsstri  3198  difeqri  3213  uneqri  3227  ssequn2  3258  unss  3259  rexun  3263  ralunb  3264  elin2  3267  ineqri  3270  dfss1  3281  nsspssun  3309  indifdir  3332  inrab2  3348  rabun2  3354  reuun2  3358  eq0  3376  0el  3378  abn0  3380  0pss  3399  disjr  3403  disj1  3404  disjpss  3412  undif4  3418  difin0ss  3426  inssdif0  3427  uneqdifeq  3448  r19.3rz  3451  r19.3rzv  3453  ralidm  3463  pwss  3543  dfpr2  3560  ralsns  3574  rexsns  3575  eltpg  3580  ralprg  3586  rexprg  3587  raltpg  3588  rextpg  3589  euabsn2  3602  eusn  3607  eldifsn  3653  rexdifsn  3655  pwpw0  3663  ssunsn  3674  eqsn  3675  sstp  3678  tpss  3679  prel12  3689  preqsn  3692  pwsnALT  3722  pwtp  3724  eluniab  3739  elunirab  3740  unipr  3741  dfnfc2  3745  uniun  3746  uniin  3747  unissb  3755  elintab  3771  elintrab  3772  ssintab  3777  ssintrab  3783  intun  3792  intpr  3793  elrint  3801  iuncom4  3810  iuneq2  3819  dfiun2g  3833  ssiinf  3849  elriin  3872  iunxiun  3882  pwssb  3886  iunpwss  3889  disjor  3904  disjors  3906  disjiun  3910  disjxiun  3917  disjxun  3918  cbvopab1  3986  dftr5  4013  trint  4025  inex1  4052  inuni  4071  axpweq  4081  nfnid  4098  zfpair2  4109  moabex  4126  exss  4129  elop  4132  otth  4143  copsex4g  4148  opeqsn  4155  opthwiener  4161  opelopabsbOLD  4166  brabga  4172  opelopabaf  4181  opabn0  4188  iunopab  4189  pwunss  4191  pwundifOLD  4194  dfid3  4203  pocl  4214  sotric  4233  isso2i  4239  somo  4241  frminex  4266  dfepfr  4271  wefrc  4280  ordtri3or  4317  ordtri2  4320  elsuci  4351  elsucg  4352  sucel  4358  on0eqel  4401  uniuni  4418  reusv2lem4  4429  reusv2lem5  4430  reusv2  4431  reusv3  4433  reuxfr2d  4448  elpwun  4458  iunpw  4461  dfwe2  4464  onintrab2  4484  ordpwsuc  4497  ordzsl  4527  dflim4  4530  tfindsg  4542  tfindes  4544  findsg  4574  elxp  4613  opelxp  4626  brxp  4627  rabxp  4632  opthprc  4643  brab2a  4645  opeliunxp  4647  xpundi  4648  xpundir  4649  elvvv  4656  brinxp  4659  brab2ga  4670  xp0r  4675  eqrelrel  4695  reliun  4713  reluni  4715  raliunxp  4732  rexiunxp  4733  ralxpf  4737  rexxpf  4738  iunxpf  4739  relop  4741  elcnv  4765  elcnv2  4766  dmin  4793  dmuni  4795  dmopab  4796  dmi  4800  rnopab  4831  elrnmpt1  4835  rncoeq  4855  resiexg  4904  dfima2  4921  dfima3  4922  elima2  4925  elima3  4926  imai  4934  elimasn  4945  epini  4950  dfse2  4953  cotr  4962  issref  4963  intasym  4965  asymref  4966  asymref2  4967  somin1  4986  cnvopab  4990  cnvi  4992  cnvdif  4994  imainss  5003  dfrel2  5031  dfrel3  5037  rnsnn0  5045  relsn2  5049  dmsnopg  5050  cnvcnvsn  5056  elxp4  5066  elxp5  5067  cnvresima  5068  mptpreima  5072  dfco2  5078  coundi  5080  coundir  5081  imaco  5084  coiun  5088  coi1  5094  relssdmrn  5099  relrelss  5102  ressn  5117  cnviin  5118  cnvpo  5119  dffun2  5123  dffun3  5124  dffun4  5125  dffun5  5126  dffun7  5138  dffun8  5139  dffun9  5140  funopab  5145  funun  5153  funcnvsn  5154  funcnv2  5166  funcnv  5167  fun2cnv  5169  fncnv  5171  fun11  5172  fununi  5173  imadif  5184  funimaexg  5186  fnunsn  5208  fnres  5217  fnopabg  5224  mptfng  5226  mptun  5231  fun  5262  fresaunres1  5271  fcnvres  5275  dff12  5293  f1cnvcnv  5302  funforn  5315  dff1o2  5334  dff1o5  5338  f1orn  5339  resdif  5351  ffoss  5362  f11o  5363  f1o00  5365  fo00  5366  elfv  5375  fv3  5393  dffn5f  5429  dffv2  5444  eqfnfv3  5476  fndmdifeq0  5483  fneqeql  5485  unpreima  5503  respreima  5506  dff4  5526  dffo3  5527  dffo5  5529  f1ompt  5534  ffnfvf  5538  fmptco  5543  fsn2  5550  fconst3  5587  fconst4  5588  idref  5611  abrexco  5618  opabex3  5621  abexssex  5633  dff13  5635  dff13f  5636  f1mpt  5637  foeqcnvco  5656  isocnv3  5681  isoini  5687  weniso  5704  oprabid  5734  dfoprab2  5747  eqoprab2b  5758  dmoprab  5780  rnoprab  5782  eloprabga  5786  mpt2mptx  5790  resoprab  5792  ffnov  5800  fnov  5804  elrnmpt2  5809  ralrnmpt2  5810  rexrnmpt2  5811  oprabex3  5814  oprabrexex2  5815  ovid  5816  ov3  5836  ov6g  5837  foov  5846  ndmovdistr  5861  difxp  6005  elopaba  6034  fmpt2  6043  curry1  6062  curry2  6065  fsplit  6075  frxp  6077  xporderlem  6078  soxp  6080  brtpos2  6092  dmtpos  6098  tpostpos  6106  tpossym  6118  tposoprab  6122  sorpsscmpl  6140  cbviota  6148  opiota  6174  eusvobj2  6223  dfsmo2  6250  tfrlem3  6279  tfrlem7  6285  tfrlem9  6287  tfrlem9a  6288  tz7.48lem  6339  tz7.49c  6344  el1o  6384  dif1o  6385  ondif2  6387  brwitnlem  6392  oarec  6446  omeulem1  6466  omeu  6469  oeordi  6471  oeeui  6486  oeeu  6487  omopthlem1  6539  dfer2  6547  brdifun  6573  swoso  6577  eqerlem  6578  qsid  6611  iiner  6617  erinxp  6619  brecop  6637  eroveu  6639  erovlem  6640  ecopovsym  6646  mapval2  6683  mapsn  6695  elixp  6709  ixpeq2  6716  ixpin  6727  ixpiin  6728  mptelixpg  6739  ixpsnf1o  6742  boxriin  6744  domen  6761  isfi  6771  en1  6813  xpsnen  6831  xpcomco  6837  xpassen  6841  sbthlem9  6864  0sdomg  6875  2pwuninel  6901  ssenen  6920  nneneq  6929  php  6930  modom2  6949  ac6sfi  6986  frfi  6987  fimaxg  6989  elfpw  7041  fissuni  7044  dffi3  7068  marypha1lem  7070  marypha2lem2  7073  dfsup2  7079  dfsup2OLD  7080  wofib  7144  wemapso2lem  7149  wdom2d  7178  unxpwdom2  7186  dford2  7205  inf2  7208  inf3lem2  7214  axinf2  7225  zfinf2  7227  cantnfp1lem2  7265  oemapso  7268  cantnflem1  7275  trcl  7294  epfrs  7297  rankvalb  7353  r1elss  7362  unbndrank  7398  scott0s  7442  cplem1  7443  bnd2  7447  isnum2  7462  iscard2  7493  infxpenlem  7525  fseqenlem1  7535  acnnum  7563  infpwfien  7573  alephnbtwn2  7583  alephord2  7587  alephislim  7594  cardaleph  7600  alephval3  7621  aceq1  7628  aceq2  7630  dfac3  7632  dfac4  7633  dfac5lem1  7634  dfac5lem2  7635  dfac5lem3  7636  dfac5lem4  7637  dfac5lem5  7638  dfac2  7641  dfac0  7643  dfac1  7644  dfac8  7645  dfac9  7646  dfac12  7659  kmlem3  7662  kmlem4  7663  kmlem7  7666  kmlem8  7667  kmlem9  7668  kmlem13  7672  kmlem14  7673  kmlem15  7674  dfackm  7676  pwsdompw  7714  ackbij2lem2  7750  cf0  7761  cfval2  7770  cflim2  7773  cfss  7775  cfslb  7776  isfin3  7806  isfin5  7809  isfin6  7810  sdom2en01  7812  fin23lem25  7834  fin23lem26  7835  fin23lem40  7861  isfin1-2  7895  isfin1-3  7896  fin1a2lem5  7914  fin1a2lem6  7915  fin1a2lem12  7921  fin12  7923  domtriomlem  7952  axdc2lem  7958  axdc3lem2  7961  axdc3lem4  7963  axcclem  7967  ac6num  7990  ac9  7994  ac6n  7996  ac9s  8004  zorn2lem6  8012  zornn0g  8016  ttukeylem6  8025  ttukey2g  8027  brdom7disj  8040  brdom6disj  8041  iunfo  8045  iundom2g  8046  konigthlem  8070  alephsuc3  8082  elgch  8124  fpwwe2lem9  8140  fpwwe2lem12  8143  fpwwe2lem13  8144  fpwwe2  8145  canth4  8149  canthwe  8153  wunex2  8240  uniwun  8242  axgroth5  8326  grothpw  8328  axgroth6  8330  grothprimlem  8335  grothprim  8336  elni  8380  ltexpi  8406  nqerf  8434  nqerid  8437  ordpipq  8446  recmulnq  8468  npomex  8500  genpnnp  8509  genpass  8513  addcompr  8525  mulcompr  8527  reclem2pr  8552  reclem3pr  8553  ltsosr  8596  ltasr  8602  mappsrpr  8610  map2psrpr  8612  opelcn  8631  elreal  8633  elreal2  8634  axaddf  8647  axmulf  8648  axicn  8652  axrrecex  8665  axpre-mulgt0  8670  xrlenlt  8770  ssxr  8772  leloe  8788  msq0i  9295  infm3  9593  supmullem2  9601  inelr  9616  arch  9841  elnnne0  9858  un0addcl  9876  un0mulcl  9877  elnnz  9913  elznn0nn  9916  elznn0  9917  elznn  9918  elz2  9919  raluz2  10147  rexuz2  10149  nnwos  10165  eluz2b2  10169  eluz2b3  10170  ublbneg  10181  zmin  10191  elq  10197  ralrp  10251  rexrp  10252  ltxr  10336  xrnemnf  10339  xrleloe  10357  xrltlen  10359  xrrebnd  10376  xaddf  10429  xmullem  10462  xmullem2  10463  xrsupss  10505  xrinfmss  10506  elfzp1  10714  fzprval  10722  fztpval  10723  fzm1  10740  fzolb  10758  fzolb2  10759  elfzo3  10768  fzouzsplit  10779  fzo0n0  10783  fzind2  10801  uzrdgfni  10899  subsq0i  11094  crreczi  11104  nn0le2msqi  11160  nn0opth2i  11164  hashkf  11217  hashfun  11266  hashbclem  11267  hashbc  11268  hashf1lem2  11271  leiso  11274  iswrd  11292  climeu  11906  lo1resb  11915  rlimresb  11916  o1resb  11917  climmpt2  11924  fsum2dlem  12110  rpnnen2  12378  sqr2irr  12401  divides  12407  odd2np1  12461  divalglem1  12467  divalglem6  12471  divalglem10  12475  divalgb  12477  bitsval2  12490  bitsmod  12501  bitscmp  12503  smueqlem  12555  isprm2  12640  isprm3  12641  isprm4  12642  isprm5  12665  pythagtriplem19  12760  pythagtrip  12761  pceu  12773  prmreclem2  12838  4sqlem2  12870  4sqlem12  12877  vdwpc  12901  vdwnn  12919  dec5dvds2  12954  pwsle  13265  imasleval  13317  xpsfrnel  13339  xpsfrnel2  13341  xpsle  13357  isacs2  13400  mreacs  13404  iscatd2  13427  comfeq  13453  oppcsect  13520  isssc  13541  isfunc  13582  funcoppc  13593  isffth2  13634  fucinv  13691  elhoma  13708  setcinv  13766  ispos  13925  ispos2  13926  tosso  13986  istsr2  14162  spwmo  14170  ismnd  14204  mndcl  14207  issubm  14260  gsumwspan  14303  issubg  14456  isnsg2  14482  eqger  14502  isgim2  14564  giclcl  14571  gicrcl  14572  gicsubgen  14577  gaorber  14597  resscntz  14642  cntzrec  14644  efgval2  14868  efgsfo  14883  efgrelexlemb  14894  isabl2  14932  iscyggen2  15003  iscyg2  15004  iscyg3  15008  lt6abl  15016  gsumval3eu  15025  gsum2d2  15060  dmdprdd  15072  subgdmdprd  15104  iscrng2  15191  dvdsrtr  15269  isunit  15274  isnirred  15317  isirred2  15318  isrhm  15336  isdrng2  15357  drngprop  15358  isabv  15419  issrng  15450  islmod  15466  islss  15527  lss1d  15555  islmim2  15654  lmiclcl  15658  lmicrcl  15659  lsmelval2  15673  lspsolvlem  15730  lspsncv0  15733  islpidl  15830  islpir2  15835  isnzr2  15847  isdomn2  15872  fiidomfld  15881  aspval2  15918  mplcoe1  16041  mplcoe2  16043  evlslem4  16077  xrsdsreclb  16250  unocv  16412  iunocv  16413  ishil2  16451  isobs  16452  obselocv  16460  iinopn  16480  istps4OLD  16493  istps5OLD  16494  istps  16506  istps2  16507  isbasis2g  16518  tgval2  16526  elcls  16642  islpi  16712  isperf2  16715  isperf3  16716  restntr  16744  ordtbaslem  16750  ordtrest2lem  16765  cnrest  16845  ist0-3  16905  ist1-2  16907  ist1-3  16909  nrmsep3  16915  isnrm2  16918  perfcls  16925  ordthaus  16944  cmpcov2  16949  cmpsub  16959  hauscmplem  16965  cmpfi  16967  iscon2  16972  dfcon2  16977  is1stc2  17000  is2ndc  17004  1stcelcls  17019  1stccn  17021  llyi  17032  subislly  17039  iskgen3  17076  txuni2  17092  ptpjpre1  17098  ptbasin  17104  tx1cn  17135  tx2cn  17136  uptx  17151  txdis1cn  17161  ptrescn  17165  txtube  17166  txcmplem1  17167  hausdiag  17171  txkgen  17178  xkohaus  17179  xkococnlem  17185  xkoinjcn  17213  qtopeu  17239  isr0  17260  regr1lem2  17263  hmphsym  17305  elmptrab2  17355  isfbas  17356  isfbas2  17362  trfbas  17371  snfil  17391  fbunfip  17396  elfg  17398  fgcl  17405  fbasrn  17411  filuni  17412  trfil2  17414  cfinfil  17420  csdfil  17421  supfil  17422  ufinffr  17456  rnelfmlem  17479  elflim2  17491  hausflim  17508  hauspwpwf1  17514  txflf  17533  isfcls2  17540  fclsopn  17541  fclsrest  17551  alexsubALTlem2  17574  alexsubALTlem3  17575  alexsubALTlem4  17576  tmdcn2  17604  divstgplem  17635  divstgphaus  17637  tsmssubm  17657  istdrg2  17692  metn0  17756  prdsxmetlem  17764  imasdsf1olem  17769  xpsdsval  17777  blres  17809  xmeterval  17810  xmeter  17811  isxms2  17826  isms2  17828  dscopn  17928  isngp3  17952  isnvc2  18041  isnghm  18064  qtopbaslem  18099  xrtgioo  18144  zcld  18151  elii1  18265  pi1cpbl  18374  tchcph  18499  cmetss  18572  bcth  18583  lssbn  18605  ishl2  18619  minveclem3b  18624  minveclem6  18630  pmltpc  18642  ovolfcl  18658  ovolgelb  18671  ovolunlem1  18688  ovoliunlem1  18693  ismbl  18717  ismbl2  18718  iundisj2  18738  dyadmax  18785  dyadmbllem  18786  vitalilem2  18796  mbfimaopnlem  18842  itg1climres  18901  itg2l  18916  itg2leub  18921  iblcnlem1  18974  ellimc2  19059  ellimc3  19061  limcmpt  19065  limcres  19068  elaa  19528  aaliou3lem9  19562  taylthlem2  19585  ulmcau  19604  pilem1  19659  sincosq1lem  19697  sineq0  19721  coseq1  19722  ellogrn  19749  logtayl2  19841  cxpcn3lem  19955  cxpcn3  19956  cubic  19977  atandm  20004  atandm2  20005  atandm4  20007  atans2  20059  xrlimcnp  20095  wilthlem2  20139  dvdsflsumcom  20260  dvdsmulf1o  20266  fsumvma  20284  logfac2  20288  dchrelbas2  20308  dchrelbas3  20309  lgsdir2lem4  20397  lgsquadlem1  20425  lgsquadlem2  20426  2sqlem1  20434  pntlem3  20590  ostth  20620  avril1  20666  grpoidinvlem3  20703  issubgo  20800  elghom  20860  islno  21161  nmoubi  21180  nmobndseqi  21187  siii  21261  minvecolem5  21290  minvecolem6  21291  hvsubaddi  21475  normsub0i  21544  bcsiALT  21588  hcau  21593  hlimadd  21602  hhcmpl  21609  hhcms  21612  issh2  21618  isch2  21633  hlim0  21645  isch3  21651  norm1exi  21659  elch0  21663  hhsssh2  21677  choc0  21735  omlsilem  21811  pjoc2i  21847  chsscon1i  21871  spanuni  21953  h1deoi  21958  h1dei  21959  elspansni  21967  cmcm4i  22022  cmbr3i  22027  cmbr4i  22028  osumcor2i  22071  5oalem7  22087  3oalem3  22091  pjss2i  22107  mayete3iOLD  22156  elcnop  22267  ellnop  22268  elhmop  22283  elcnfn  22292  ellnfn  22293  cnvadj  22302  nmopub  22318  nmfnleub  22335  eleigvec  22367  nmop0  22396  nmfn0  22397  nmopun  22424  lncnopbd  22447  riesz2  22476  nmopcoadj0i  22513  rnbra  22517  pjnmopi  22558  pjssdif1i  22585  pjin2i  22603  pjin3i  22604  pjclem1  22605  cvbr2  22693  cvnbtwn3  22698  cvnbtwn4  22699  mdsl2bi  22733  mdsldmd1i  22741  elat2  22750  chrelat2i  22775  atomli  22792  chirredi  22804  mdsymlem6  22818  mdsymlem8  22820  sumdmdii  22825  dmdbr5ati  22832  cdj3i  22851  xfree2  22855  eldmgm  22865  subfacp1lem5  22886  subfacp1lem6  22887  cvmscld  22975  cvmlift2lem12  23016  vdgrun  23064  eupath  23076  ghomgrpilem2  23164  axextprim  23218  axrepprim  23219  axunprim  23220  axpowprim  23221  axregprim  23222  axinfprim  23223  axacprim  23224  untangtr  23231  biimpexp  23241  divelunit  23250  dftr6  23277  coep  23278  coepr  23279  dffr5  23280  dfpo2  23282  cnvco1  23287  cnvco2  23288  fundmpss  23290  dfdm5  23300  dfrn5  23301  elpotr  23305  dford5reg  23306  dfon2lem5  23311  dfon2lem6  23312  dfon2lem8  23314  dfon2lem9  23315  dfon2  23316  wfi  23375  eltrpred  23397  frind  23411  poseq  23421  soseq  23422  wfrlem4  23427  wfrlem5  23428  wfrlem9  23432  wfrlem11  23434  wfrlem12  23435  wfrlem13  23436  wfrlem14  23437  wfrlem15  23438  tfrALTlem  23444  tfr3ALT  23447  frrlem5  23453  frrlem5e  23457  frrlem11  23461  nosgnn0  23479  axdenselem5  23507  axfelem12  23525  axfelem15  23528  axfelem18  23531  axfelem22  23535  elsymdif  23542  brsymdif  23547  brtxp  23595  brpprod  23600  brpprod3b  23602  brsset  23604  idsset  23605  dfon3  23607  brtxpsd  23609  brtxpsd2  23610  brbigcup  23613  elfix  23618  dffix2  23620  ellimits  23625  elfuns  23628  snelsingles  23635  dfiota3  23636  brcart  23645  brimg  23650  brapply  23651  brcup  23652  brcap  23653  brsuccf  23654  funpartfun  23655  fullfunfnv  23658  brrestrict  23661  dfrdg4  23662  tfrqfree  23663  altopthsn  23669  altopelaltxp  23684  altxpsspw  23685  mptelee  23697  brbtwn2  23707  colinearalg  23712  ax5seg  23740  axpasch  23743  axlowdimlem6  23749  axlowdimlem13  23756  axeuclidlem  23764  axeuclid  23765  axcontlem3  23768  axcontlem4  23769  axcontlem12  23777  brcolinear2  23855  broutsideof  23918  outsideofcom  23925  fvray  23938  fvline  23941  lineunray  23944  linecom  23947  linerflx2  23948  ellines  23949  bpoly2  23966  bpoly3  23967  rankeq1o  23975  elhf  23978  elhf2  23979  r19.26-2a  24099  eeeeanv  24109  altdftru  24113  pm11.53g  24129  eqvinopb  24130  copsexgb  24131  ltl4ev  24157  albineal  24164  evevifev  24179  cnvref  24230  restidsing  24241  dffn5a  24296  repcpwti  24327  dfdir2  24457  apnei  24686  ismonc  24980  isepic  24990  isfunb  25001  issubcata  25012  isntr  25039  clscnc  25176  bisig0  25228  isconcl5a  25267  isconcl5ab  25268  isibg2  25276  bosser  25333  hpd  25335  ecase13d  25388  cnvresimaOLD  25392  trer  25393  elicc3  25394  finminlem  25397  opnrebl  25401  nn0prpw  25405  clsun  25412  fneval  25453  fnessref  25459  neibastop1  25474  neifg  25486  filnetlem4  25496  f1opr  25557  inixp  25565  sdclem2  25618  sdclem1  25619  fdc  25621  neificl  25633  istotbnd3  25661  sstotbnd3  25666  isbndx  25672  isbnd3b  25675  cntotbnd  25686  heibor1lem  25699  heibor1  25700  isdrngo2  25755  isdrngo3  25756  iscrngo2  25789  smprngopr  25843  isdmn2  25846  isfldidl2  25860  ispridlc  25861  isdmn3  25865  an43OLD  25879  prtlem70  25881  prtlem100  25887  n0el  25891  prter2  25915  funsnfsup  25928  cmpfiiin  25938  isnacs2  25947  elmzpcl  25970  diophrex  26021  2sbcrex  26030  sbcrot3  26034  sbcrot5  26035  3rexfrabdioph  26044  4rexfrabdioph  26045  6rexfrabdioph  26046  7rexfrabdioph  26047  ftp  26059  fphpd  26065  fiphp3d  26068  rencldnfilem  26069  jm2.23  26255  expdiophlem1  26280  expdiophlem2  26281  expdioph  26282  dford4  26288  wopprc  26289  ttac  26295  fnwe2lem2  26314  islmodfg  26333  islnm2  26342  lnmlmic  26352  uvcvv0  26405  isnumbasgrplem1  26432  dfacbasgrp  26439  islinds2  26449  lmiclbs  26473  islnr2  26484  islnr3  26485  f1omvdco3  26558  matrcl  26632  issdrg2  26672  sdrgacs  26675  phisum  26684  isdomn3  26689  pm10.541  26728  pm10.542  26729  19.21vv  26740  19.36vv  26747  19.31vv  26748  19.37vv  26749  19.28vv  26750  pm11.6  26757  pm11.62  26759  pm14.12  26788  elnev  26805  aiffbbtat  26858  aisbbisfaisf  26859  abnotbtaxb  26869  gte-lteh  26885  gt-lth  26886  sgnn  26940  onfrALTlem5  27000  onfrALTlem4  27001  onfrALTlem1  27006  2uasbanh  27020  dfvd2  27041  dfvd2an  27044  dfvd3  27053  dfvd3an  27056  eelT00  27170  eelTTT  27171  eelT12  27176  uunT1  27245  uunT1p1  27246  uun132p1  27251  un2122  27255  uunTT1p1  27259  uunTT1p2  27260  uunT11p1  27262  uunT11p2  27263  uunT12  27264  uunT12p1  27265  uunT12p2  27266  uunT12p3  27267  uunT12p4  27268  uunT12p5  27269  uun2221  27278  uun2221p1  27279  uun2221p2  27280  undif3VD  27348  onfrALTlem5VD  27351  onfrALTlem4VD  27352  onfrALTlem1VD  27356  2uasbanhVD  27377  bnj170  27412  bnj248  27414  bnj251  27416  bnj256  27420  bnj258  27422  bnj291  27425  bnj422  27429  bnj432  27430  bnj23  27433  bnj89  27436  bnj132  27441  bnj156  27445  bnj158  27446  bnj538  27458  bnj563  27461  bnj945  27494  bnj946  27495  bnj976  27498  bnj1098  27504  bnj1138  27509  bnj1209  27518  bnj1476  27568  bnj1542  27578  bnj110  27579  bnj91  27582  bnj92  27583  bnj106  27589  bnj118  27590  bnj124  27592  bnj125  27593  bnj153  27601  bnj207  27602  bnj222  27604  bnj518  27607  bnj535  27611  bnj539  27612  bnj543  27614  bnj553  27619  bnj556  27621  bnj558  27623  bnj571  27627  bnj605  27628  bnj591  27632  bnj594  27633  bnj580  27634  bnj609  27638  bnj611  27639  bnj865  27644  bnj849  27646  bnj882  27647  bnj916  27654  bnj917  27655  bnj934  27656  bnj929  27657  bnj944  27659  bnj953  27660  bnj1000  27662  bnj969  27667  bnj970  27668  bnj978  27670  bnj983  27672  bnj984  27673  bnj985  27674  bnj986  27675  bnj1021  27685  bnj1033  27688  bnj1049  27693  bnj1052  27694  bnj1083  27697  bnj1112  27702  bnj1030  27706  bnj1137  27714  bnj1189  27728  bnj1204  27731  bnj1253  27736  bnj1279  27737  bnj1373  27749  bnj1388  27752  bnj1398  27753  bnj1450  27769  equvelv  27805  a12study4  27806  a12study8  27808  a12peros  27810  a12lem2  27820  a12study10  27825  a12study10n  27826  lsateln0  27874  islshpat  27896  lcvbr2  27901  lcvbr3  27902  lcvnbtwn3  27907  islfl  27939  lshpsmreu  27988  lub0N  28068  glb0N  28072  cvrnbtwn3  28155  leat2  28173  isat3  28186  iscvlat2N  28203  ishlat2  28232  ishlat3N  28233  hlrelat5N  28279  hlrelat2  28281  3dim0  28335  2dim  28348  islpln5  28413  islvol5  28457  4atlem3  28474  dalem20  28571  ispsubsp2  28624  snatpsubN  28628  pmapglb  28648  elpadd  28677  paddasslem17  28714  dalawlem13  28761  pclfinN  28778  polval2N  28784  pclfinclN  28828  lhpex2leN  28891  isltrn2N  28998  cdleme0nex  29168  cdleme22b  29219  cdlemftr3  29443  tendoset  29637  diarnN  30008  dibopelvalN  30022  dibopelval2  30024  dibelval3  30026  diblsmopel  30050  dicelval3  30059  dihglb2  30221  doch11  30252  islpolN  30362  lcfls1N  30414  mapdval4N  30511  mapdrvallem2  30524
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