Theorem bitri 279

Description: An inference from transitive law for logical equivalence. (The proof was 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

Step	Hyp	Ref	Expression
1		bitri.1	. . . 4 |- (ph <-> ps)
2	1	biimpi 224	. . 3 |- (ph -> ps)
3		bitri.2	. . 3 |- (ps <-> ch)
4	2, 3	sylib 242	. 2 |- (ph -> ch)
5	3	biimpri 230	. . 3 |- (ch -> ps)
6	5, 1	sylibr 243	. 2 |- (ch -> ph)
7	4, 6	impbii 223	1 |- (ph <-> ch)

Syntax hints:   <-> wb 219

This theorem is referenced by:  bitr2i 281  bitr3i 282  bitr4i 283  bitrd 284  3bitri 289  3bitr2i 291  3bitr3i 293  3bitr4i 295  imbi12i 301  mt2bi 326  dfor2OLD 350  iman 363  imanOLD 364  impexpOLD 405  anorOLD 422  pm4.52 425  oridmOLD 463  orbi12i 479  or42 491  pm4.14OLD 550  pm4.78OLD 556  anassOLD 634  anbi12i 710  bibi12i 714  pm5.3 773  pm5.53 843  an42 883  ibibr 934  orddi 946  anddi 947  pm4.71r 959  pm5.17OLD 982  pm5.18OLD 984  nbbn 985  dfbi3OLD 994  xor2OLD 996  xordi 997  pm5.55OLD 1001  pm4.43 1048  orbidiOLD 1056  biluk 1058  pm5.75 1062  ccaseOLD 1073  dn1 1098  3orass 1105  3anass 1106  3ancomb 1110  3anor 1113  3ioran 1115  nic-justbi 1509  nic-mpALT 1513  nic-axALT 1515  exp3acom23g 1568  alex 1670  alinexa 1678  exanali 1679  alexn 1680  19.21-2 1693  19.26-2 1704  19.26-3an 1705  19.27 1706  19.28 1707  19.36 1715  19.37 1717  19.44 1726  19.45 1727  alrot4 1734  exrot3 1736  exrot4 1737  albiim 1746  2albiim 1747  aaan 1759  eeor 1760  sbor 1881  sb19.21 1882  sban 1883  sbbi 1885  sblbis 1886  sbrbis 1887  sbrbif 1888  sbid2 1900  sbco2d 1903  sb8e 1909  19.23vv 1942  19.41vv 1954  19.41vvv 1955  19.41vvvv 1956  19.42vv 1959  19.42vvv 1960  4exdistr 1963  cbvex4v 1972  eean 1973  2sb5 1988  2sb6 1989  sbcom2 1990  sb6a 1992  2sb5rf 1993  2sb6rf 1994  sbex 2003  sbalv 2004  exsb 2005  2exsb 2006  a12lem2 2032  eujust 2039  euf 2043  sb8eu 2050  cbveu 2051  mo 2053  eu2 2056  mo2 2060  sbmo 2061  mo3 2062  mo4f 2063  eu4 2071  moanim 2088  2exeu 2109  2mo 2110  2mos 2111  2eu1 2112  2eu3 2114  2eu4 2115  2eu6 2117  exists1 2121  abid 2130  eleq12i 2209  abeq2 2248  abeq2i 2250  eq2ab 2253  abid2f 2261  clabel 2263  sbabel 2265  neeq12i 2277  necon3abii 2295  necon1abii 2316  neanior 2346  ralinexa 2393  rexanali 2394  r3al 2402  r19.26-2 2468  ralbiim 2471  r19.30 2476  ralcom 2488  rexcom 2489  ralcom2 2490  reean 2492  3reeanv 2494  2ralor 2495  cbvralf 2522  cbvrexf 2523  cbvreuv 2528  cbvral2v 2529  cbvral3v 2530  rabeq2i 2537  issetf 2543  ceqsex2 2573  ceqsex3v 2575  ceqsex6v 2577  ceqsex8v 2578  gencbvex 2579  vtoclgf 2587  cla4gf 2602  cla43gv 2609  eqvincf 2629  ceqsrex2v 2635  elab4g 2649  elrab2 2656  ralab 2657  rexrab 2659  morex 2682  euxfr2 2683  euxfr 2684  euind 2685  reu2 2688  rmo4 2691  reu4 2692  reu7 2693  2reuswap 2695  reuind 2696  sbralie 2699  cbvralsv 2729  cbvrexsv 2730  sbccomglem 2757  ra5 2770  rmo3 2771  rmoi 2772  cbvralcsf 2820  cbvrexcsf 2821  cbvreucsf 2822  dfss 2837  dfss2f 2843  ss2ab 2901  dfpss2 2919  dfpss3 2920  psseq12i 2925  sspsstri 2934  difeqri 2947  uneqri 2961  ssequn2 2992  unss 2993  rexun 2996  ralunb 2997  ineqri 3001  sseqin2 3025  nsspssun 3037  indifdir 3059  undif3 3063  inrab2 3074  reuun2 3080  eq0 3096  0el 3098  0pss 3115  disjr 3119  disj1 3120  disjpss 3127  undif4 3133  difin0ss 3140  inssdif0 3141  uneqdifeq 3157  r19.3rz 3160  r19.3rzv 3162  ralidm 3172  pwss 3237  dfpr2 3252  rexsng 3265  ralprg 3271  rexpr 3273  raltp 3274  ralsng 3276  disjsn 3280  euabsn 3285  eusn 3286  eldifsn 3318  pwpw0 3326  eqsn 3332  tpss 3334  prel12 3342  preqsn 3344  pwsnALT 3362  eluniab 3378  elunirab 3379  unipr 3380  uniun 3385  uniin 3386  unissb 3394  elintab 3411  elintrab 3412  intun 3430  intpr 3431  iuneq2 3450  dfiun2g 3459  dfiin2g 3461  iinxprg 3496  iunxsn 3497  iunun 3498  iunxun 3499  iununi 3501  pwssb 3503  iunpwss 3506  cbvopab1 3573  trint 3593  inex1 3619  inuni 3638  axpweq 3648  exss 3679  dtruALT 3680  zfpair2 3688  elop 3691  opcom 3710  opeqsn 3712  opthwiener 3717  opelopabsb 3725  brabg 3729  opelopabf 3733  opabn0 3736  pwunss 3738  pwundif 3740  dfid3 3748  pocl 3756  posn 3762  sotric 3774  so 3778  dfepfr 3796  wefrc 3806  ordtri3or 3843  ordtri2 3846  elsuci 3876  elsucg 3877  sucel 3883  trsuc2 3896  on0eqel 3927  uniuni 3944  reusv2lem2 3968  reusv2lem3 3969  reusv2lem4 3970  reusv2 3972  reusv3 3974  reusv6OLD 3977  eusvobj1 3980  reuxfr2d 3990  reuxfr2 3991  elpwun 4001  iunpw 4004  fr3nr 4005  dfwe2 4007  onintrab2 4026  ordzsl 4066  dflim4 4069  tfindsg 4080  findsg 4113  elxp 4151  brxp 4171  rexxp 4175  ralxpf 4176  rexxpf 4177  iunxpf 4178  opthprc 4179  xpundi 4183  xpundir 4184  elvvv 4187  xp0r 4198  eqrelrel 4216  reliun 4231  reluni 4233  relop 4242  brco 4260  elcnv 4265  elcnv2 4266  eldm2 4280  dmin 4290  dmi 4296  rncoeq 4337  opres 4348  resiexg 4374  dfima2 4385  dfima3 4386  elima2 4389  elima3 4390  imai 4398  elimasn 4408  epini 4413  cotr 4420  intasym 4422  asymref 4423  asymref2 4424  cnvopab 4429  cnvi 4431  imainss 4440  dfrel2 4463  rnsnn0 4469  dmsnop 4472  cnvsn 4477  elxp4 4482  elxp5 4483  dfrel3 4484  dfco2 4495  coundi 4497  coundir 4498  imaco 4501  coiun 4505  coi1 4511  coass 4514  relssdmrn 4516  relrelss 4517  cnviin 4530  cnvpo 4531  dffun2 4535  dffun3 4536  dffun4 4537  dffun5 4538  dffun7 4550  dffun8 4551  dffun9 4552  funopab 4557  funun 4564  funcnv 4576  fun2cnv 4578  fncnv 4580  fun11 4581  fununi 4582  imadif 4593  funimaexg 4595  isarep1 4597  iunfopab 4639  fnopabg 4642  fnopab2g 4643  fun 4673  fcnvres 4680  dff12 4696  funforn 4712  dff1o2 4727  dff1o3 4728  dff1o5 4731  resdif 4742  ffoss 4751  f11o 4752  f1o00 4754  fo00 4755  fv2 4761  elfv 4763  fv3 4779  tz6.12-1 4782  nfvres 4791  dffv2 4820  fvopab5 4842  fvopab6 4843  eqfnfv3 4855  unpreima 4870  respreima 4872  dff4 4881  dffo3 4882  dffo5 4884  ffnfvf 4894  fopabfv 4896  fsn2 4903  fconst3 4918  fconst4 4919  funfvima 4920  opabex3 4933  imaiun 4935  abexssex 4943  dff13 4945  dff13f 4946  isoini 4973  oprabid 5002  dfoprab2 5012  dmoprab 5024  rnoprab 5026  resoprab 5031  ffnoprv 5036  fnoprv 5039  foprv 5040  oprabex3 5044  oprabval3 5053  oprabval6g 5056  fooprv 5061  ndmoprdistr 5075  fnmpt 5114  dfopab2 5164  dfoprab3 5165  dfoprab5sf 5169  oprabopabf 5170  foprab2 5174  curry1 5198  curry2 5201  fsplit 5209  frxp 5210  xporderlem 5211  soxp 5213  dfiota2 5220  cbviotaf 5224  sb8iota 5226  reiota4 5241  dfsmo2 5258  tfrlem3 5284  tfrlem7 5289  tfrlem9 5291  dfrdg2 5305  tz7.48lem 5328  tz7.48-2OLD 5330  el1o 5357  oarec 5407  omeulem1 5424  omeu 5426  oeordi 5428  oaabs 5470  dfer2 5480  eqerlem 5488  erdisj 5504  uniqs 5515  0nelqs 5518  ecid 5520  qsid 5521  brecop 5526  ecopoprsym 5530  th3qlem1 5534  mapval2 5555  elpm 5556  elpm2 5557  mapsn 5565  ixpeq2 5575  domen 5599  isfi 5602  en1 5646  2dom 5647  xpsnen 5658  xpcomen 5662  xpassen 5664  pw2en 5671  ac6sfilem3 5674  sbthlem9 5684  sdomdomtr 5698  domtriord 5713  pwuninel 5719  2pwuninel 5720  xpen 5767  xpenOLD 5768  mapxpen 5780  xpmapenlem5 5785  ssenen 5789  nneneq 5798  php 5799  sucxpdom 5822  fineqvlem 5829  fimax 5846  frfi 5851  unfilem1 5860  abfii2 5874  abfii4 5876  indexfi 5878  iunfi 5883  dfsup2 5889  dfsup2OLD 5890  supmo 5895  ordiso 5914  ordtypelem6 5920  ordtypelem7 5921  hartogslem 5923  dford2 5943  inf2 5946  inf3lem2 5952  axinf2 5963  zfinf2 5965  trcl 5988  zfregs 5990  setind2 5996  tz9.12lem1 6006  tz9.12lem3 6008  rankel 6027  rankval3 6028  unbndrank 6030  rankun 6038  onfrALTlem5 6076  onfrALTlem4 6077  scottexs 6087  scott0s 6088  cplem1 6089  bnd2 6093  karden 6095  card1 6123  iscard 6130  iscard2 6131  cardprclem 6134  infxpenlem 6147  alephord2 6161  alephislim 6165  infenomsub 6180  aceq1 6183  aceq2 6185  aceq3lem 6186  aceq3 6187  aceq4 6188  aceq5lem1 6189  aceq5lem2 6190  aceq5lem3 6191  aceq5lem4 6192  aceq5lem5 6193  aceq6b 6196  aceq8 6203  alephnbtwn2 6210  cardaleph 6214  alephval3 6233  cdaen 6244  cdadom1 6253  pwsdompw 6264  cf0 6270  cfval2 6280  cflim2 6283  domtriomlem 6296  axdc2lem 6303  axdc3lem2 6306  axdc3lem4 6308  axcclem 6312  ac6n 6327  ac9s 6336  kmlem3 6339  kmlem4 6340  kmlem7 6343  kmlem8 6344  kmlem9 6345  kmlem13 6349  kmlem14 6350  kmlem15 6351  aceqkm 6353  zorn2lem6 6366  brdom7disj 6380  brdom6disj 6381  card1OLD 6397  iscardOLD 6419  iscard2OLD 6420  konigthlem 6429  alephord2OLD 6440  cardalephOLD 6443  cfeq0OLD 6446  cfsucOLD 6447  elni 6522  ltexpi 6547  ltsopq 6593  genpv 6620  genpn0 6624  genpass 6630  1pr 6635  addcompr 6641  mulcompr 6643  distrlem1pr 6645  distrlem5pr 6649  prlem934b 6656  reclem1pr 6674  reclem2pr 6675  suplem1pr 6679  ltsosr 6721  ltasr 6727  mappsrpr 6736  map2psrpr 6738  suppsr3 6742  opelcn 6766  elreal 6768  axaddopr 6783  axmulopr 6784  axicn 6788  axrnegex 6799  axrrecex 6800  pre-axmulgt0 6806  pre-axsup 6807  ltxrlt 6859  xrlenlt 6860  leloe 6877  ssxr 6899  xrleloe 6916  xrrebnd 6927  mul02lem2 6972  subadd2i 7026  neg11i 7059  ltadd1i 7120  leadd2i 7122  ltsubaddi 7123  lesubaddi 7124  ltnegi 7132  ltnegcon2i 7134  msqgt0i 7139  msq0i 7215  rec11ii 7284  halfposi 7420  ralrp 7586  infm3 7603  infmsup 7617  arch 7620  xrinfmss 7628  supxrre 7632  elnnz 7695  elznn0nn 7698  elznn0 7699  elznn 7700  elnn0nn 7721  elnnnn0 7722  zltp1le 7732  uzwo3 7776  zmin 7777  qjust 7781  elq 7783  icounlem 7927  snunioolem 7929  raluz2 7959  rexuz2 7961  nnwof 7975  nnwos 7976  eluz2b2 7980  eluz2b3 7981  ublbneg 7992  subsq0i 8278  nn0le2msqi 8297  nn0opth2i 8301  inelr 8369  replim 8395  abslti 8511  abslei 8512  cau4ii 8555  cau5i 8556  cvg3i 8560  bcpasci 8606  hashgval 8616  dffsum 8654  csbfsum 8683  clm4i 8736  climunii 8754  climeu 8756  climshft2i 8762  cvgcmp3cetlem1 8845  cvgcmp3cetlem2 8846  mulc1cncf 8939  ef1tllem 9041  eirrlem1 9049  ruclem1 9173  ruclem3 9175  ruclem8 9180  infxpidmlem6OLD 9220  infxpidmlem7OLD 9221  infxpidmlem9OLD 9223  infxpidmlem12OLD 9226  infmap2lem1 9242  infmap2lem2 9243  alephsuc3 9248  divides 9253  divalglem1 9291  divalglem6 9295  divalglem10 9299  divalgb 9301  gcd0id 9323  eucalgf 9346  eucalginv 9347  eucalglt 9348  isprm2 9369  isprm3 9370  isprm4 9371  4nprm 9376  grpcl 9470  grpidinvlem3 9475  ringcl 9510  istps4OLD 9715  istps5OLD 9716  istps 9717  istps4 9720  istps5 9721  isbasis2g 9732  tgval2 9738  tgval3 9746  tgss3 9759  basgen 9761  txbas 9791  clsval2 9825  elcls 9844  ntreq0 9848  islp2 9889  islpi 9891  qdensere 9893  cncnplem4 9920  sncld 9930  blrn2 9985  cncfmet 10049  metcn4 10115  fsumcnlem 10133  bcthlem7 10149  bcthlem29 10171  bcthlem32 10174  grp2grp 10189  grp2grpo 10190  grpoidinvlem3 10199  gapmlem 10330  sspval 10590  isphg 10686  isph 10691  siii 10723  ishl 10807  spwmo 10870  spwpr2 10872  pilem1 10891  sincosq1lem 10923  cosh111lem1 10939  cosh111lem3 10941  efifolem4 10950  effoi 10970  axgroth5 11003  grothpw 11005  grothomex 11007  axgroth6 11008  grothprimlem 11011  grothprim 11012  avril1 11013  elghom 11027  uptx 11061  subspi 11079  isfbas2 11101  fbssint 11117  fbunfip 11120  elfg 11122  extbas1 11129  filrn 11131  hausfillim 11141  elfilmap 11150  cncomp 11169  h2hcau 11319  axhcompl 11338  hvsubaddi 11403  normsub0i 11471  bcsiALT 11515  hhcmpl 11538  hlimuniii 11575  chcmhi 11580  norm1exi 11589  elch0 11593  hhsssh2 11607  pjthlem1 11686  omlsilem 11711  pjoc2i 11738  chsscon1i 11852  chsscon2i 11853  spanuni 11934  h1deoi 11939  h1dei 11940  elspansni 11948  cmcm4i 12003  cmbr3i 12008  cmbr4i 12009  osumlem5 12049  osumcor2i 12057  5oalem7 12072  3oalem3 12076  pjss2i 12092  mayete3i 12140  mayete3OLDi 12141  cnvadj 12285  nmopun 12408  nmcopexlem1 12420  lncnopbd 12435  nmcfnexlem1 12449  riesz2 12468  nmopcoadj0i 12505  bra11 12510  pjnmopi 12550  pjssdif1i 12578  pjin2i 12597  pjin3i 12598  pjclem1 12599  strlem1 12653  cvbr2 12686  cvnbtwn3 12691  cvnbtwn4 12692  mdsl2bi 12726  mdsldmd1i 12734  elat2 12743  chrelat2i 12768  atomli 12785  irredi 12797  mdsymlem6 12811  mdsymlem8 12813  sumdmdii 12818  dmdbr5ati 12825  cdj3i 12844  xfree2 12848  bnj169 12864  bnj170 12865  bnj171 12866  bnj173 12868  bnj174 12869  bnj176 12871  bnj177 12872  bnj178 12873  bnj182 12876  bnj186 12878  bnj188 12879  bnj189 12880  bnj190 12881  bnj191 12882  bnj192 12883  bnj194 12885  bnj195 12886  bnj196 12887  bnj197 12888  bnj198 12889  bnj200 12890  bnj201 12891  bnj202 12892  bnj203 12893  bnj204 12894  bnj248 12907  bnj249 12908  bnj250 12909  bnj251 12910  bnj256 12915  bnj258 12917  bnj259 12918  bnj260 12919  bnj261 12920  bnj279 12938  bnj280 12939  bnj281 12940  bnj282 12941  bnj283 12942  bnj284 12943  bnj285 12944  bnj286 12945  bnj287 12946  bnj288 12947  bnj289 12948  bnj291 12950  bnj292 12951  bnj293 12952  bnj294 12953  bnj295 12954  bnj296 12955  bnj297 12956  bnj298 12957  bnj299 12958  bnj300 12959  bnj301 12960  bnj302 12961  bnj303 12962  bnj304 12963  bnj305 12964  bnj306 12965  bnj307 12966  bnj308 12967  bnj309 12968  bnj310 12969  bnj311 12970  bnj313 12972  bnj314 12973  bnj315 12974  bnj316 12975  bnj317 12976  bnj318 12977  bnj319 12978  bnj320 12979  bnj321 12980  bnj322 12981  bnj323 12982  bnj324 12983  bnj325 12984  bnj326 12985  bnj327 12986  bnj328 12987  bnj329 12988  bnj330 12989  bnj331 12990  bnj332 12991  bnj333 12992  bnj334 12993  bnj335 12994  bnj336 12995  bnj337 12996  bnj338 12997  bnj339 12998  bnj340 12999  bnj341 13000  bnj342 13001  bnj343 13002  bnj344 13003  bnj346 13005  bnj347 13006  bnj348 13007  bnj349 13008  bnj350 13009  bnj351 13010  bnj352 13011  bnj353 13012  bnj354 13013  bnj355 13014  bnj356 13015  bnj357 13016  bnj358 13017  bnj359 13018  bnj360 13019  bnj361 13020  bnj362 13021  bnj363 13022  bnj364 13023  bnj365 13024  bnj366 13025  bnj367 13026  bnj368 13027  bnj369 13028  bnj370 13029  bnj371 13030  bnj372 13031  bnj373 13032  bnj374 13033  bnj375 13034  bnj376 13035  bnj377 13036  bnj378 13037  bnj379 13038  bnj380 13039  bnj381 13040  bnj382 13041  bnj383 13042  bnj384 13043  bnj385 13044  bnj386 13045  bnj387 13046  bnj388 13047  bnj389 13048  bnj390 13049  bnj391 13050  bnj392 13051  bnj393 13052  bnj394 13053  bnj395 13054  bnj396 13055  bnj397 13056  bnj398 13057  bnj399 13058  bnj400 13059  bnj401 13060  bnj402 13061  bnj403 13062  bnj404 13063  bnj405 13064  bnj406 13065  bnj407 13066  bnj408 13067  bnj409 13068  bnj410 13069  bnj411 13070  bnj412 13071  bnj413 13072  bnj414 13073  bnj415 13074  bnj416 13075  bnj417 13076  bnj418 13077  bnj419 13078  bnj420 13079  bnj421 13080  bnj422 13081  bnj423 13082  bnj424 13083  bnj425 13084  bnj426 13085  bnj427 13086  bnj428 13087  bnj429 13088  bnj430 13089  bnj431 13090  bnj432 13091  bnj434 13092  bnj435 13093  bnj436 13094  bnj437 13095  bnj438 13096  bnj439 13097  bnj440 13098  bnj441 13099  bnj442 13100  bnj443 13101  bnj444 13102  bnj446 13104  bnj447 13105  bnj448 13106  bnj449 13107  bnj450 13108  bnj451 13109  bnj452 13110  bnj453 13111  bnj454 13112  bnj455 13113  bnj457 13115  bnj458 13116  bnj459 13117  bnj460 13118  bnj461 13119  bnj462 13120  bnj463 13121  bnj464 13122  bnj465 13123  bnj466 13124  bnj468 13126  bnj469 13127  bnj470 13128  bnj471 13129  bnj472 13130  bnj473 13131  bnj474 13132  bnj475 13133  bnj476 13134  bnj478 13135  bnj479 13136  bnj480 13137  bnj481 13138  bnj482 13139  bnj483 13140  bnj484 13141  bnj485 13142  bnj486 13143  bnj487 13144  bnj488 13145  bnj489 13146  bnj491 13148  bnj492 13149  bnj493 13150  bnj494 13151  bnj511 13152  bnj495 13153  bnj496 13154  bnj497 13155  bnj498 13156  bnj499 13157  bnj500 13158  bnj501 13159  bnj502 13160  bnj503 13161  bnj504 13162  bnj505 13163  bnj506 13164  bnj507 13165  bnj508 13166  bnj509 13167  bnj510 13168  bnj4 13172  bnj8 13174  bnj11 13177  bnj13 13178  bnj16 13180  bnj24 13187  bnj26 13188  bnj33 13197  bnj34 13198  bnj37 13201  bnj40 13204  bnj41 13205  bnj45 13207  bnj47 13209  bnj51 13214  bnj55 13217  bnj58 13218  bnj77 13224  bnj78 13225  bnj80 13227  bnj89 13229  bnj88 13231  bnj132 13245  bnj140 13252  bnj141 13253  bnj142 13254  bnj156 13262  bnj220 13285  bnj512 13292  bnj537 13305  bnj538 13306  bnj856 13560  bnj912 13593  bnj922 13605  bnj946 13616  bnj947 13617  bnj971 13631  bnj980 13633  bnj979 13634  bnj988 13636  bnj989 13637  bnj990 13638  bnj991 13639  bnj1010 13645  bnj1035 13656  bnj1054 13662  bnj1058 13666  bnj1074 13674  bnj1135 13706  bnj1138 13707  bnj1144 13712  bnj1197 13744  bnj1208 13753  bnj1209 13754  bnj1215 13762  bnj1269 13798  bnj1305 13819  bnj1325 13829  bnj1330 13832  bnj1366 13862  bnj1370 13865  bnj1391 13876  bnj1438 13903  bnj1479 13926  bnj22 13962  bnj53 13964  bnj71 13977  bnj81 13980  bnj82 13981  bnj86 13984  bnj87 13985  bnj91 13986  bnj92 13987  bnj104 13995  bnj106 13996  bnj109 13997  bnj118 13999  bnj120 14001  bnj124 14005  bnj149 14012  bnj153 14018  bnj207 14019  bnj222 14022  bnj518 14031  bnj539 14037  bnj541 14039  bnj543 14040  bnj549 14046  bnj556 14051  bnj571 14060  bnj605 14063  bnj589 14068  bnj591 14070  bnj580 14072  bnj609 14077  bnj849 14089  bnj882 14091  bnj917 14104  bnj934 14105  bnj944 14111  bnj950 14113  bnj983 14128  bnj984 14129  bnj985 14130  bnj986 14131  bnj1021 14151  bnj1033 14155  bnj1040 14159  bnj1043 14162  bnj1045 14163  bnj1067 14170  bnj1069 14171  bnj1081 14178  bnj1083 14179  bnj1112 14189  bnj1134 14198  bnj1253 14241  bnj1313 14265  bnj1319 14266  bnj1373 14277  hashpwlem 14363  hashpw 14364  ghomgrpilem2 14366  cayleylem2 14379  cayleylem3 14380  axextprim 14420  axrepprim 14421  axunprim 14422  axpowprim 14423  axregprim 14424  axinfprim 14425  axacprim 14426  untangtr 14433  biimpexp 14445  r19.30OLD 14447  indifdiOLD 14453  dftr6 14460  coep 14461  coepr 14462  dffr5 14463  dfso2 14464  dfpo2 14465  elpotr 14481  dford3 14482  dfon2lem5 14487  dfon2lem6 14488  dfon2lem8 14490  dfon2lem9 14491  dfon2 14492  omopthlem1 14501  elpredim 14529  elpred 14530  elpredg 14531  tz6.26 14558  wfi 14560  eltrpred 14578  frind 14592  xporderlemOLD 14601  soxpOLD 14603  frxpOLD 14604  poseq 14607  soseq 14608  wfrlem4 14613  wfrlem5 14614  wfrlem9 14618  wfrlem11 14620  wfrlem12 14621  wfrlem13 14622  wfrlem14 14623  wfrlem15 14624  tfrALTlem 14629  tfr3ALT 14632  frrlem5 14638  frrlem5e 14642  frrlem11 14646  elno3 14661  nosgnn0 14664  sltres 14670  axdenselem5 14692  axfelem12 14710  axfelem15 14713  axfelem18 14716  axfelem22 14720  elsymdif 14727  brsset 14754  idsset 14755  dfon3 14757  brbigcup 14759  elfix 14764  dffix2 14766  ellimits 14771  elfuns 14774  snelsingles 14776  dfiota3 14777  altopthsn 14784  altopelaltxp 14799  altxpsspw 14800  FTBid 14822  19.41vvvvOLD 14971  eeeeanv 14972  r19.3rzvb 14973  altdftru 14983  cbvrex2v 15003  boxeq 15022  albineal 15031  evevifev 15036  fnoprvpop 15046  ficli 15063  ref4w 15080  cnvref 15081  restidsing 15101  cnvintcnvOLD 15194  repcpwti 15242  cbicplem 15247  dffprod 15409  bsi 15598  apnei 15623  hmeogrp 15649  rcfpfillem2 15695  limfillem1 15704  grphmlem1 15769  grphm 15774  altretoplem2 15787  altretop 15788  dualcat2lem 15923  dualded2lem 15924  dualcat2 15927  ishoma 15930  ismonc 15957  isepic 15967  issubcat 15987  tarval1 16024  settrcon 16057  bpmp 16061  isline1 16104  ecase13d 16174  dfiin2gOLD 16180  cnvresima 16183  dmsdtriordOLD 16184  trer 16185  finminlem 16191  elfiun 16193  fictblem 16194  fictb 16195  ordisoOLD 16198  ordtypelem6OLD 16204  ordtypelem7OLD 16205  hartog 16208  infenomsubOLD 16222  opncldf1 16226  opncldf3 16228  clsun 16237  subntr 16249  cnsubsp 16250  compsub 16255  cptclsscpt 16256  hscptsscld 16258  compfipin0lem 16259  compfipin0 16260  alexsublem2 16262  alexsublem3 16263  alexsublem4 16264  alexsub 16265  is1stc3 16293  is2ndc2 16297  isfne2 16305  topfneec 16325  fnessref 16327  locfincomp 16338  comppfsc 16341  neibastop2lem2 16344  neibastop2lem3 16345  neibastop2lem4 16346  ist0-2 16363  fbasfip 16380  neifg 16383  isufil2 16389  ufprim 16393  filssufillem 16394  fixufil 16400  ufinffr 16402  filcon 16404  cnpfillim 16413  rnelfmlem 16416  flimfcn 16427  isfclus 16430  fcluscf 16436  flimfnfcls 16439  fcluscn 16443  fclsfcn 16456  filnetlem1 16464  filnetlem2 16465  filnetlem3 16466  filnetlem4 16467  biadan2 16472  sbmoOLD 16478  2ralorOLD 16479  rexunOLD 16480  3reeanvOLD 16485  morexOLD 16486  ralabOLD 16493  rexrabOLD 16495  disjrOLD 16499  unpreimaOLD 16507  respreimaOLD 16508  opabex3OLD 16525  oprabrexex2 16533  f1opr 16538  eqfnfv3OLD 16545  inixp 16546  eroprlem 16556  eropreu 16557  eroprf 16559  fimaxOLD 16570  indexfiOLD 16579  zornn0 16588  frfiOLD 16595  fzsplit 16616  fzm1 16620  elnnr 16627  sdc 16635  fdc 16636  seq1eq2 16641  fsum00 16644  fsumltisumi 16647  lmclim2 16674  piececn 16718  txmet 16749  sstotbnd 16760  isbnd3 16765  heiborlem1 16779  heiborlem16 16794  heiborlem20 16798  heiborlem37 16815  bfp 16833  rrndstprj1 16841  rrntotbndlem1 16844  rrntotbnd 16846  phtpycolem5 16879  phtpyco 16880  pcocn 16900  pcohtpylem3 16906  pcohtpy 16907  isdivrng2 16935  isdivrng3 16936  iscring 16969  iscring2 16970  fldcrng 16976  pridlnr 17008  smprngpr 17024  isdmn 17026  isdmn2 17027  isfldidl2 17041  ispridlc 17042  isdmn3 17046  an43OLD 17060  prtlem70 17062  prtlem100 17068  prtlem5 17069  n0el 17072  prter2 17109  prter3 17110  blkssatm 17113  pm10.541 17138  pm10.542 17139  alrot3 17149  19.21vv 17152  19.36vv 17160  19.31vv 17161  19.37vv 17162  19.28vv 17163  2exanali 17167  pm11.53 17168  pm11.6 17173  pm11.62 17175  issetaOLD 17229  cbvralcsfOLD 17235  cbvrexcsfOLD 17236  cbvreucsfOLD 17237  cbviotafOLD 17256  dfvd2 17320  dfvd3 17325  undif3VD 17540  onfrALTlem5VD 17543  onfrALTlem4VD 17544  glb0 17587  isolat 17606  cvrnbtwn3 17667  atlrelat1 17718  iscvlat2 17721  ishlat2 17749  ishlat3 17750  hlrelat5 17796  hlrelat2 17798  3dim0 17853  2dim 17866  issrng 17888  issdrng 17891  isphil 17907  islpln5 17966  islvol5 18011  4atlem3 18028  dalem20 18125  ispsubsp2 18179  pmapglb 18202  elpadd 18231  paddasslem17 18268  dalawlem13 18315  polval2 18323  isltrn2 18473  cdleme0nex 18661  cdleme22b 18713

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7

This theorem depends on definitions:  df-bi 220

Copyright terms: Public domain