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

Theorem tru 1399
Description: The truth value is provable. (Contributed by Anthony Hart, 13-Oct-2010.)
Assertion
Ref Expression
tru

Proof of Theorem tru
StepHypRef Expression
1 id 22 . 2 No typesetting for: |- ( A. x x = x -> A. x x = x )
2 df-tru 1398 . 2 No typesetting for: |- ( T. <-> ( A. x x = x -> A. x x = x ) )
31, 2mpbir 209 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  A.wal 1393  =wceq 1395   wtru 1396
This theorem is referenced by:  fal  1402  dftru2  1403  trud  1404  tbtru  1405  bitru  1407  a1tru  1411  truan  1412  truorfal  1424  falortru  1425  truimfal  1428  cadtru  1469  nftru  1626  disjprg  4448  reusv2lem5  4657  rabxfr  4674  reuhyp  4680  euotd  4753  elabrex  6155  caovcl  6469  caovass  6475  caovdi  6494  ectocl  7398  fin1a2lem10  8810  riotaneg  10543  zriotaneg  11002  cshwsexa  12792  eflt  13852  efgi0  16738  efgi1  16739  0frgp  16797  iundisj2  21959  pige3  22910  tanord1  22924  tanord  22925  logtayl  23041  iundisj2f  27449  iundisj2fi  27602  ordtcon  27907  allt  29866  nextnt  29870  wl-impchain-mp-x  29956  wl-impchain-com-1.x  29960  wl-impchain-com-n.m  29965  ftc1anclem5  30094  mzpcompact2lem  30684  elabrexg  31430  uun0.1  33575  uunT1  33577  un10  33585  un01  33586  bj-trut  34171  bj-axd2d  34181  bj-rabtr  34497  bj-rabtrALT  34498  bj-df-v  34583  bj-finsumval0  34663  lhpexle1  35732  bj-ifid2  37711  bj-ifim1  37712  bj-ifim2  37713  bj-ifnot  37717  bj-ifdfor  37722
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 185  df-tru 1398
  Copyright terms: Public domain W3C validator