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  2526  rexnal  2527  ralinexa  2561  rexanali  2562  r3al  2573  r19.26-2  2649  ralbiim  2653  r19.30  2658  ralcomf  2671  rexcomf  2672  rexrot4  2676  reean  2679  3reeanv  2681  rabbi  2691  cbvralf  2728  cbvreu  2732  cbvral2v  2741  cbvrex2v  2742  cbvral3v  2743  cbvralsv  2744  cbvrexsv  2745  sbralie  2746  rabeq2i  2754  issetf  2762  2gencl  2785  3gencl  2786  ceqsex2  2792  ceqsex3v  2794  ceqsex6v  2796  ceqsex8v  2797  gencbvex  2798  cla43gv  2841  eqvincf  2864  ceqsrex2v  2871  elrab2  2893  ralab  2894  ralrab  2895  rexab  2896  rexrab  2897  ralab2  2898  rexab2  2900  eueq3  2908  morex  2917  euxfr2  2918  euxfr  2919  euind  2920  reu2  2921  reu6  2922  rmo4  2926  reu4  2927  reu7  2928  imrmo  2932  2reuswap  2933  reuind  2934  sbcco  2974  sbccomlem  3022  sbccom  3023  ra5  3036  rmo3  3039  csbco  3051  sbnfc2  3102  csbabg  3103  cbvralcsf  3104  cbvreucsf  3106  dfss  3128  dfss2f  3132  ss2ab  3202  dfpss2  3222  dfpss3  3223  psseq12i  3228  sspsstri  3239  difeqri  3257  uneqri  3278  ssequn2  3309  unss  3310  rexun  3316  ralunb  3317  elin2  3320  ineqri  3323  dfss1  3334  dfss5  3335  nsspssun  3363  indifdir  3386  inrab2  3402  rabun2  3408  reuun2  3412  eq0  3430  0el  3432  abn0  3434  0pss  3453  disjr  3457  disj1  3458  disjpss  3466  undif4  3472  difin0ss  3481  inssdif0  3482  uneqdifeq  3503  r19.3rz  3506  r19.3rzv  3508  ralidm  3518  pwss  3599  dfpr2  3616  ralsns  3630  rexsns  3631  eltpg  3636  ralprg  3642  rexprg  3643  raltpg  3644  rextpg  3645  euabsn2  3658  eusn  3663  eldifsn  3709  rexdifsn  3713  difsnpss  3718  pwpw0  3723  ssunsn  3734  eqsn  3735  sstp  3738  tpss  3739  prel12  3749  preqsn  3752  pwsnALT  3782  pwtp  3784  eluniab  3799  elunirab  3800  unipr  3801  dfnfc2  3805  uniun  3806  uniin  3807  unissb  3817  elintab  3833  elintrab  3834  ssintab  3839  ssintrab  3845  intun  3854  intpr  3855  elrint  3863  iuncom4  3872  iuneq2  3881  dfiun2g  3895  ssiinf  3911  elriin  3934  iunxiun  3944  pwssb  3948  iunpwss  3951  dfdisj2  3955  nfdisj  3965  disjor  3967  disjors  3969  invdisj  3972  disjiun  3973  disjxiun  3980  disjxun  3981  cbvopab1  4049  dftr5  4076  trint  4088  inex1  4115  inuni  4135  axpweq  4145  nfnid  4162  zfpair2  4173  moabex  4190  exss  4194  elop  4197  otth  4208  copsex4g  4213  opeqsn  4220  opthwiener  4226  opelopabsbOLD  4231  brabga  4237  opelopabaf  4246  opabn0  4253  iunopab  4254  pwunss  4256  pwundifOLD  4259  dfid3  4268  pocl  4279  sotric  4298  isso2i  4304  somo  4306  frminex  4331  dfepfr  4336  wefrc  4345  ordtri3or  4382  ordtri2  4385  elsuci  4416  elsucg  4417  sucel  4423  on0eqel  4468  uniuni  4485  reusv2lem4  4496  reusv2lem5  4497  reusv2  4498  reusv3  4500  reuxfr2d  4515  elpwun  4525  iunpw  4528  dfwe2  4531  onintrab2  4551  ordpwsuc  4564  ordzsl  4594  dflim4  4597  tfindsg  4609  tfindes  4611  findsg  4641  elxp  4680  opelxp  4693  brxp  4694  rabxp  4699  opthprc  4710  brab2a  4712  opeliunxp  4714  xpundi  4715  xpundir  4716  elvvv  4723  brinxp  4726  brab2ga  4737  xp0r  4742  eqrelrel  4762  reliun  4780  reluni  4782  raliunxp  4799  rexiunxp  4800  ralxpf  4804  rexxpf  4805  iunxpf  4806  relop  4808  elcnv  4832  elcnv2  4833  dmin  4860  dmuni  4862  dmopab  4863  dmi  4867  rnopab  4898  elrnmpt1  4902  rncoeq  4922  resiexg  4971  dfima2  4988  dfima3  4989  elima2  4992  elima3  4993  imai  5001  elimasn  5012  epini  5017  dfse2  5020  cotr  5029  issref  5030  intasym  5032  asymref  5033  asymref2  5034  somin1  5053  cnvopab  5057  cnvi  5059  cnvdif  5061  imainss  5070  dfrel2  5098  dfrel3  5104  rnsnn0  5112  relsn2  5116  dmsnopg  5117  cnvcnvsn  5123  elxp4  5133  elxp5  5134  cnvresima  5135  mptpreima  5139  dfco2  5145  coundi  5147  coundir  5148  imaco  5151  coiun  5155  coi1  5161  relssdmrn  5166  relrelss  5169  ressn  5184  cnviin  5185  cnvpo  5186  dffun2  5190  dffun3  5191  dffun4  5192  dffun5  5193  dffun7  5205  dffun8  5206  dffun9  5207  funopab  5212  funun  5220  funcnvsn  5221  funcnv2  5233  funcnv  5234  fun2cnv  5236  fncnv  5238  fun11  5239  fununi  5240  imadif  5251  funimaexg  5253  fnunsn  5275  fnres  5284  fnopabg  5291  mptfng  5293  mptun  5298  fun  5329  fresaunres1  5338  fcnvres  5342  dff12  5360  f1cnvcnv  5369  funforn  5382  dff1o2  5401  dff1o5  5405  f1orn  5406  resdif  5418  ffoss  5429  f11o  5430  f1o00  5432  fo00  5433  elfv  5442  fv3  5460  dffn5f  5497  dffv2  5512  eqfnfv3  5544  fndmdifeq0  5551  fneqeql  5553  unpreima  5571  respreima  5574  dff4  5594  dffo3  5595  dffo5  5597  f1ompt  5602  ffnfvf  5606  fmptco  5611  fsn2  5618  fconst3  5655  fconst4  5656  idref  5679  abrexco  5686  opabex3  5689  abexssex  5701  dff13  5703  dff13f  5704  f1mpt  5705  foeqcnvco  5724  isocnv3  5749  isoini  5755  weniso  5772  oprabid  5802  dfoprab2  5815  eqoprab2b  5826  dmoprab  5848  rnoprab  5850  eloprabga  5854  mpt2mptx  5858  resoprab  5860  ffnov  5868  fnov  5872  elrnmpt2  5877  ralrnmpt2  5878  rexrnmpt2  5879  oprabex3  5882  oprabrexex2  5883  ovid  5884  ov3  5904  ov6g  5905  foov  5914  ndmovdistr  5929  difxp  6073  elopaba  6102  fmpt2  6111  curry1  6130  curry2  6133  fsplit  6143  frxp  6145  xporderlem  6146  soxp  6148  brtpos2  6160  dmtpos  6166  tpostpos  6174  tpossym  6186  tposoprab  6190  sorpsscmpl  6208  cbviota  6216  opiota  6242  eusvobj2  6291  dfsmo2  6318  tfrlem3  6347  tfrlem7  6353  tfrlem9  6355  tfrlem9a  6356  tz7.48lem  6407  tz7.49c  6412  el1o  6452  dif1o  6453  ondif2  6455  brwitnlem  6460  oarec  6514  omeulem1  6534  omeu  6537  oeordi  6539  oeeui  6554  oeeu  6555  omopthlem1  6607  dfer2  6615  brdifun  6641  swoso  6645  eqerlem  6646  qsid  6679  iiner  6685  erinxp  6687  brecop  6705  eroveu  6707  erovlem  6708  ecopovsym  6714  mapval2  6751  mapsn  6763  elixp  6777  ixpeq2  6784  ixpin  6795  ixpiin  6796  mptelixpg  6807  ixpsnf1o  6810  boxriin  6812  domen  6829  isfi  6839  en1  6882  xpsnen  6900  xpcomco  6906  xpassen  6910  sbthlem9  6933  0sdomg  6944  2pwuninel  6970  ssenen  6989  nneneq  6998  php  6999  modom2  7018  ac6sfi  7055  frfi  7056  fimaxg  7058  elfpw  7111  fissuni  7114  dffi3  7138  marypha1lem  7140  marypha2lem2  7143  dfsup2  7149  dfsup2OLD  7150  wofib  7214  wemapso2lem  7219  wdom2d  7248  unxpwdom2  7256  dford2  7275  inf2  7278  inf3lem2  7284  axinf2  7295  zfinf2  7297  cantnfp1lem2  7335  oemapso  7338  cantnflem1  7345  trcl  7364  epfrs  7367  rankvalb  7423  r1elss  7432  unbndrank  7468  scott0s  7512  cplem1  7513  bnd2  7517  isnum2  7532  iscard2  7563  infxpenlem  7595  fseqenlem1  7605  acnnum  7633  infpwfien  7643  alephnbtwn2  7653  alephord2  7657  alephislim  7664  cardaleph  7670  alephval3  7691  aceq1  7698  aceq2  7700  dfac3  7702  dfac4  7703  dfac5lem1  7704  dfac5lem2  7705  dfac5lem3  7706  dfac5lem4  7707  dfac5lem5  7708  dfac2  7711  dfac0  7713  dfac1  7714  dfac8  7715  dfac9  7716  dfac12  7729  kmlem3  7732  kmlem4  7733  kmlem7  7736  kmlem8  7737  kmlem9  7738  kmlem13  7742  kmlem14  7743  kmlem15  7744  dfackm  7746  pwsdompw  7784  ackbij2lem2  7820  cf0  7831  cfval2  7840  cflim2  7843  cfss  7845  cfslb  7846  isfin3  7876  isfin5  7879  isfin6  7880  sdom2en01  7882  fin23lem25  7904  fin23lem26  7905  fin23lem40  7931  isfin1-2  7965  isfin1-3  7966  fin1a2lem5  7984  fin1a2lem6  7985  fin1a2lem12  7991  fin12  7993  domtriomlem  8022  axdc2lem  8028  axdc3lem2  8031  axdc3lem4  8033  axcclem  8037  ac6num  8060  ac9  8064  ac6n  8066  ac9s  8074  zorn2lem6  8082  zornn0g  8086  ttukeylem6  8095  ttukey2g  8097  brdom7disj  8110  brdom6disj  8111  iunfo  8115  iundom2g  8116  konigthlem  8144  alephsuc3  8156  elgch  8198  fpwwe2lem9  8214  fpwwe2lem12  8217  fpwwe2lem13  8218  fpwwe2  8219  canth4  8223  canthwe  8227  wunex2  8314  uniwun  8316  axgroth5  8400  grothpw  8402  axgroth6  8404  grothprimlem  8409  grothprim  8410  elni  8454  ltexpi  8480  nqerf  8508  nqerid  8511  ordpipq  8520  recmulnq  8542  npomex  8574  genpnnp  8583  genpass  8587  addcompr  8599  mulcompr  8601  reclem2pr  8626  reclem3pr  8627  ltsosr  8670  ltasr  8676  mappsrpr  8684  map2psrpr  8686  opelcn  8705  elreal  8707  elreal2  8708  axaddf  8721  axmulf  8722  axicn  8726  axrrecex  8739  axpre-mulgt0  8744  xrlenlt  8844  ssxr  8846  leloe  8862  msq0i  9369  infm3  9667  supmullem2  9675  inelr  9690  arch  9915  elnnne0  9932  un0addcl  9950  un0mulcl  9951  elnnz  9987  elznn0nn  9990  elznn0  9991  elznn  9992  elz2  9993  raluz2  10221  rexuz2  10223  nnwos  10239  eluz2b2  10243  eluz2b3  10244  ublbneg  10255  zmin  10265  elq  10271  ralrp  10325  rexrp  10326  ltxr  10410  xrnemnf  10413  xrleloe  10431  xrltlen  10433  xrrebnd  10450  xaddf  10503  xmullem  10536  xmullem2  10537  xrsupss  10579  xrinfmss  10580  elfzp1  10788  fzprval  10796  fztpval  10797  fzm1  10814  fzolb  10832  fzolb2  10833  elfzo3  10842  fzouzsplit  10853  fzo0n0  10857  fzind2  10875  uzrdgfni  10973  subsq0i  11168  crreczi  11178  nn0le2msqi  11234  nn0opth2i  11238  hashkf  11291  hashfun  11340  hashbclem  11341  hashbc  11342  hashf1lem2  11345  leiso  11348  iswrd  11366  climeu  11980  lo1resb  11989  rlimresb  11990  o1resb  11991  climmpt2  11998  fsum2dlem  12184  rpnnen2  12452  sqr2irr  12475  divides  12481  odd2np1  12535  divalglem1  12541  divalglem6  12545  divalglem10  12549  divalgb  12551  bitsval2  12564  bitsmod  12575  bitscmp  12577  smueqlem  12629  isprm2  12714  isprm3  12715  isprm4  12716  isprm5  12739  pythagtriplem19  12834  pythagtrip  12835  pceu  12847  prmreclem2  12912  4sqlem2  12944  4sqlem12  12951  vdwpc  12975  vdwnn  12993  dec5dvds2  13028  pwsle  13339  imasleval  13391  xpsfrnel  13413  xpsfrnel2  13415  xpsle  13431  isacs2  13503  mreacs  13508  iscatd2  13531  comfeq  13557  oppcsect  13624  isssc  13645  isfunc  13686  funcoppc  13697  isffth2  13738  fucinv  13795  elhoma  13812  setcinv  13870  ispos  14029  ispos2  14030  tosso  14090  istsr2  14275  spwmo  14283  ismnd  14317  mndcl  14320  issubm  14373  gsumwspan  14416  issubg  14569  isnsg2  14595  eqger  14615  isgim2  14677  giclcl  14684  gicrcl  14685  gicsubgen  14690  gaorber  14710  resscntz  14755  cntzrec  14757  efgval2  14981  efgsfo  14996  efgrelexlemb  15007  isabl2  15045  iscyggen2  15116  iscyg2  15117  iscyg3  15121  lt6abl  15129  gsumval3eu  15138  gsum2d2  15173  dmdprdd  15185  subgdmdprd  15217  iscrng2  15304  dvdsrtr  15382  isunit  15387  isnirred  15430  isirred2  15431  isrhm  15449  isdrng2  15470  drngprop  15471  isabv  15532  issrng  15563  islmod  15579  islss  15640  lss1d  15668  islmim2  15767  lmiclcl  15771  lmicrcl  15772  lsmelval2  15786  lspsolvlem  15843  lspsncv0  15847  islpidl  15946  islpir2  15951  isnzr2  15963  isdomn2  15988  fiidomfld  15997  aspval2  16034  mplcoe1  16157  mplcoe2  16159  evlslem4  16193  xrsdsreclb  16366  unocv  16528  iunocv  16529  ishil2  16567  isobs  16568  obselocv  16576  iinopn  16596  istps4OLD  16609  istps5OLD  16610  istps  16622  istps2  16623  isbasis2g  16634  tgval2  16642  elcls  16758  islpi  16828  isperf2  16831  isperf3  16832  restntr  16860  ordtbaslem  16866  ordtrest2lem  16881  cnrest  16961  ist0-3  17021  ist1-2  17023  ist1-3  17025  nrmsep3  17031  isnrm2  17034  perfcls  17041  ordthaus  17060  cmpcov2  17065  cmpsub  17075  hauscmplem  17081  cmpfi  17083  iscon2  17088  dfcon2  17093  is1stc2  17116  is2ndc  17120  1stcelcls  17135  1stccn  17137  llyi  17148  subislly  17155  iskgen3  17192  txuni2  17208  ptpjpre1  17214  ptbasin  17220  tx1cn  17251  tx2cn  17252  uptx  17267  txdis1cn  17277  ptrescn  17281  txtube  17282  txcmplem1  17283  hausdiag  17287  txkgen  17294  xkohaus  17295  xkococnlem  17301  xkoinjcn  17329  qtopeu  17355  isr0  17376  regr1lem2  17379  hmphsym  17421  elmptrab2  17471  isfbas  17472  isfbas2  17478  trfbas  17487  snfil  17507  fbunfip  17512  elfg  17514  fgcl  17521  fbasrn  17527  filuni  17528  trfil2  17530  cfinfil  17536  csdfil  17537  supfil  17538  ufinffr  17572  rnelfmlem  17595  elflim2  17607  hausflim  17624  hauspwpwf1  17630  txflf  17649  isfcls2  17656  fclsopn  17657  fclsrest  17667  alexsubALTlem2  17690  alexsubALTlem3  17691  alexsubALTlem4  17692  tmdcn2  17720  divstgplem  17751  divstgphaus  17753  tsmssubm  17773  istdrg2  17808  metn0  17872  prdsxmetlem  17880  imasdsf1olem  17885  xpsdsval  17893  blres  17925  xmeterval  17926  xmeter  17927  isxms2  17942  isms2  17944  dscopn  18044  isngp3  18068  isnvc2  18157  isnghm  18180  qtopbaslem  18215  xrtgioo  18260  zcld  18267  elii1  18381  pi1cpbl  18490  tchcph  18615  cmetss  18688  bcth  18699  lssbn  18721  ishl2  18735  minveclem3b  18740  minveclem6  18746  pmltpc  18758  ovolfcl  18774  ovolgelb  18787  ovolunlem1  18804  ovoliunlem1  18809  ismbl  18833  ismbl2  18834  iundisj2  18854  dyadmax  18901  dyadmbllem  18902  vitalilem2  18912  mbfimaopnlem  18958  itg1climres  19017  itg2l  19032  itg2leub  19037  iblcnlem1  19090  ellimc2  19175  ellimc3  19177  limcmpt  19181  limcres  19184  elaa  19644  aaliou3lem9  19678  taylthlem2  19701  ulmcau  19720  pilem1  19775  sincosq1lem  19813  sineq0  19837  coseq1  19838  ellogrn  19865  logtayl2  19957  cxpcn3lem  20035  cxpcn3  20036  cubic  20093  atandm  20120  atandm2  20121  atandm4  20123  atans2  20175  xrlimcnp  20211  wilthlem2  20255  dvdsflsumcom  20376  dvdsmulf1o  20382  fsumvma  20400  logfac2  20404  dchrelbas2  20424  dchrelbas3  20425  lgsdir2lem4  20513  lgsquadlem1  20541  lgsquadlem2  20542  2sqlem1  20550  pntlem3  20706  ostth  20736  avril1  20782  grpoidinvlem3  20819  issubgo  20916  elghom  20976  islno  21277  nmoubi  21296  nmobndseqi  21303  siii  21377  minvecolem5  21406  minvecolem6  21407  hvsubaddi  21591  normsub0i  21660  bcsiALT  21704  hcau  21709  hlimadd  21718  hhcmpl  21725  hhcms  21728  issh2  21734  isch2  21749  hlim0  21761  isch3  21767  norm1exi  21775  elch0  21779  hhsssh2  21793  choc0  21851  pjhtheu  21919  pjpreeq  21923  omlsilem  21927  pjoc2i  21963  chsscon1i  21987  spanuni  22069  h1deoi  22074  h1dei  22075  elspansni  22083  cmcm4i  22138  cmbr3i  22143  cmbr4i  22144  osumcor2i  22187  5oalem7  22203  3oalem3  22207  pjss2i  22223  mayete3iOLD  22272  elcnop  22383  ellnop  22384  elhmop  22399  elcnfn  22408  ellnfn  22409  cnvadj  22418  nmopub  22434  nmfnleub  22451  eleigvec  22483  nmop0  22512  nmfn0  22513  nmopun  22540  lncnopbd  22563  riesz2  22592  nmopcoadj0i  22629  rnbra  22633  pjnmopi  22674  pjssdif1i  22701  pjin2i  22719  pjin3i  22720  pjclem1  22721  cvbr2  22809  cvnbtwn3  22814  cvnbtwn4  22815  mdsl2bi  22849  mdsldmd1i  22857  elat2  22866  chrelat2i  22891  atomli  22908  chirredi  22920  mdsymlem6  22934  mdsymlem8  22936  sumdmdii  22941  dmdbr5ati  22948  cdj3i  22967  xfree2  22971  ballotlemelo  22993  ballotlem2  22994  ballotlemfmpn  23000  ballotlemodife  23003  ballotlem4  23004  ballotth  23043  eldmgm  23052  subfacp1lem5  23073  subfacp1lem6  23074  cvmscld  23162  cvmlift2lem12  23203  vdgrun  23251  eupath  23263  ghomgrpilem2  23351  axextprim  23405  axrepprim  23406  axunprim  23407  axpowprim  23408  axregprim  23409  axinfprim  23410  axacprim  23411  untangtr  23418  biimpexp  23428  divelunit  23437  dftr6  23464  coep  23465  coepr  23466  dffr5  23467  dfpo2  23469  cnvco1  23474  cnvco2  23475  fundmpss  23477  dfdm5  23487  dfrn5  23488  elpotr  23492  dford5reg  23493  dfon2lem5  23498  dfon2lem6  23499  dfon2lem8  23501  dfon2lem9  23502  dfon2  23503  wfi  23562  eltrpred  23584  frind  23598  poseq  23608  soseq  23609  wfrlem4  23614  wfrlem5  23615  wfrlem9  23619  wfrlem11  23621  wfrlem12  23622  wfrlem13  23623  wfrlem14  23624  wfrlem15  23625  tfrALTlem  23631  tfr3ALT  23634  frrlem5  23640  frrlem5e  23644  frrlem11  23648  nosgnn0  23666  axdenselem5  23694  axfelem12  23712  axfelem15  23715  axfelem18  23718  axfelem22  23722  elsymdif  23729  brsymdif  23734  brtxp  23782  brpprod  23787  brpprod3b  23789  brsset  23791  idsset  23792  dfon3  23794  brtxpsd  23796  brtxpsd2  23797  brbigcup  23800  elfix  23805  dffix2  23807  ellimits  23812  elfuns  23815  snelsingles  23822  dfiota3  23823  brcart  23832  brimg  23837  brapply  23838  brcup  23839  brcap  23840  brsuccf  23841  funpartfun  23842  fullfunfnv  23845  brrestrict  23848  dfrdg4  23849  tfrqfree  23850  altopthsn  23856  altopelaltxp  23871  altxpsspw  23872  mptelee  23884  brbtwn2  23894  colinearalg  23899  ax5seg  23927  axpasch  23930  axlowdimlem6  23936  axlowdimlem13  23943  axeuclidlem  23951  axeuclid  23952  axcontlem3  23955  axcontlem4  23956  axcontlem12  23964  brcolinear2  24042  broutsideof  24105  outsideofcom  24112  fvray  24125  fvline  24128  lineunray  24131  linecom  24134  linerflx2  24135  ellines  24136  bpoly2  24153  bpoly3  24154  rankeq1o  24162  elhf  24165  elhf2  24166  r19.26-2a  24286  eeeeanv  24296  altdftru  24300  pm11.53g  24316  eqvinopb  24317  copsexgb  24318  ltl4ev  24344  albineal  24351  evevifev  24366  cnvref  24417  restidsing  24428  dffn5a  24483  repcpwti  24514  dfdir2  24644  apnei  24873  ismonc  25167  isepic  25177  isfunb  25188  issubcata  25199  isntr  25226  clscnc  25363  bisig0  25415  isconcl5a  25454  isconcl5ab  25455  isibg2  25463  bosser  25520  hpd  25522  ecase13d  25575  cnvresimaOLD  25579  trer  25580  elicc3  25581  finminlem  25584  opnrebl  25588  nn0prpw  25592  clsun  25599  fneval  25640  fnessref  25646  neibastop1  25661  neifg  25673  filnetlem4  25683  f1opr  25744  inixp  25752  sdclem2  25805  sdclem1  25806  fdc  25808  neificl  25820  istotbnd3  25848  sstotbnd3  25853  isbndx  25859  isbnd3b  25862  cntotbnd  25873  heibor1lem  25886  heibor1  25887  isdrngo2  25942  isdrngo3  25943  iscrngo2  25976  smprngopr  26030  isdmn2  26033  isfldidl2  26047  ispridlc  26048  isdmn3  26052  an43OLD  26066  prtlem70  26068  prtlem100  26074  n0el  26078  prter2  26102  funsnfsup  26115  cmpfiiin  26125  isnacs2  26134  elmzpcl  26157  diophrex  26208  2sbcrex  26217  sbcrot3  26221  sbcrot5  26222  3rexfrabdioph  26231  4rexfrabdioph  26232  6rexfrabdioph  26233  7rexfrabdioph  26234  ftp  26246  fphpd  26252  fiphp3d  26255  rencldnfilem  26256  jm2.23  26442  expdiophlem1  26467  expdiophlem2  26468  expdioph  26469  dford4  26475  wopprc  26476  ttac  26482  fnwe2lem2  26501  islmodfg  26520  islnm2  26529  lnmlmic  26539  uvcvv0  26592  isnumbasgrplem1  26619  dfacbasgrp  26626  islinds2  26636  lmiclbs  26660  islnr2  26671  islnr3  26672  f1omvdco3  26745  matrcl  26819  issdrg2  26859  sdrgacs  26862  phisum  26871  isdomn3  26876  pm10.541  26915  pm10.542  26916  19.21vv  26927  19.36vv  26934  19.31vv  26935  19.37vv  26936  19.28vv  26937  pm11.6  26944  pm11.62  26946  pm14.12  26975  elnev  26992  evth2f  27040  elunif  27041  evthf  27052  stoweidlem14  27084  stoweidlem24  27094  stoweidlem31  27101  stoweidlem34  27104  stoweidlem37  27107  stoweidlem51  27121  stoweidlem54  27124  stoweidlem57  27127  stoweidlem59  27129  aiffnbandciffatnotciffb  27147  mdandyvr0  27185  mdandyvr1  27186  mdandyvr2  27187  mdandyvr3  27188  mdandyvr4  27189  mdandyvr5  27190  mdandyvr6  27191  mdandyvr7  27192  mdandyvr8  27193  mdandyvr9  27194  mdandyvr10  27195  mdandyvr11  27196  mdandyvr12  27197  mdandyvr13  27198  mdandyvr14  27199  mdandyvr15  27200  gte-lteh  27229  gt-lth  27230  sgnn  27284  onfrALTlem5  27344  onfrALTlem4  27345  onfrALTlem1  27350  2uasbanh  27364  dfvd2  27385  dfvd2an  27388  dfvd3  27397  dfvd3an  27400  eelT00  27514  eelTTT  27515  eelT12  27520  uunT1  27589  uunT1p1  27590  uun132p1  27595  un2122  27599  uunTT1p1  27603  uunTT1p2  27604  uunT11p1  27606  uunT11p2  27607  uunT12  27608  uunT12p1  27609  uunT12p2  27610  uunT12p3  27611  uunT12p4  27612  uunT12p5  27613  uun2221  27622  uun2221p1  27623  uun2221p2  27624  undif3VD  27692  onfrALTlem5VD  27695  onfrALTlem4VD  27696  onfrALTlem1VD  27700  2uasbanhVD  27721  bnj170  27756  bnj248  27758  bnj251  27760  bnj256  27764  bnj258  27766  bnj291  27769  bnj422  27773  bnj432  27774  bnj23  27777  bnj89  27780  bnj132  27785  bnj156  27789  bnj158  27790  bnj538  27802  bnj563  27805  bnj945  27838  bnj946  27839  bnj976  27842  bnj1098  27848  bnj1138  27853  bnj1209  27862  bnj1476  27912  bnj1542  27922  bnj110  27923  bnj91  27926  bnj92  27927  bnj106  27933  bnj118  27934  bnj124  27936  bnj125  27937  bnj153  27945  bnj207  27946  bnj222  27948  bnj518  27951  bnj535  27955  bnj539  27956  bnj543  27958  bnj553  27963  bnj556  27965  bnj558  27967  bnj571  27971  bnj605  27972  bnj591  27976  bnj594  27977  bnj580  27978  bnj609  27982  bnj611  27983  bnj865  27988  bnj849  27990  bnj882  27991  bnj916  27998  bnj917  27999  bnj934  28000  bnj929  28001  bnj944  28003  bnj953  28004  bnj1000  28006  bnj969  28011  bnj970  28012  bnj978  28014  bnj983  28016  bnj984  28017  bnj985  28018  bnj986  28019  bnj1021  28029  bnj1033  28032  bnj1049  28037  bnj1052  28038  bnj1083  28041  bnj1112  28046  bnj1030  28050  bnj1137  28058  bnj1189  28072  bnj1204  28075  bnj1253  28080  bnj1279  28081  bnj1373  28093  bnj1388  28096  bnj1398  28097  bnj1450  28113  19.8vK  28155  equextvK  28224  equvelv  28267  a12study4  28268  a12study8  28270  a12peros  28272  a12lem2  28282  a12study10  28287  a12study10n  28288  lsateln0  28336  islshpat  28358  lcvbr2  28363  lcvbr3  28364  lcvnbtwn3  28369  islfl  28401  lshpsmreu  28450  lub0N  28530  glb0N  28534  cvrnbtwn3  28617  leat2  28635  isat3  28648  iscvlat2N  28665  ishlat2  28694  ishlat3N  28695  hlrelat5N  28741  hlrelat2  28743  3dim0  28797  2dim  28810  islpln5  28875  islvol5  28919  4atlem3  28936  dalem20  29033  ispsubsp2  29086  snatpsubN  29090  pmapglb  29110  elpadd  29139  paddasslem17  29176  dalawlem13  29223  pclfinN  29240  polval2N  29246  pclfinclN  29290  lhpex2leN  29353  isltrn2N  29460  cdleme0nex  29630  cdleme22b  29681  cdlemftr3  29905  tendoset  30099  diarnN  30470  dibopelvalN  30484  dibopelval2  30486  dibelval3  30488  diblsmopel  30512  dicelval3  30521  dihglb2  30683  doch11  30714  islpolN  30824  lcfls1N  30876  mapdval4N  30973  mapdrvallem2  30986
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