Theorem tru 1401

Description: The truth value T. is provable. (Contributed by Anthony Hart, 13-Oct-2010.)

Assertion

Ref	Expression
tru	|- T.

Proof of Theorem tru

Step	Hyp	Ref	Expression
1		id 19	. 2 |- ( A. x x = x -> A. x x = x )
2		df-tru 1400	. 2 |- ( T. <-> ( A. x x = x -> A. x x = x ) )
3	1, 2	mpbir 146	1 |- T.

Syntax hints:   -> wi 4   A.wal 1395   = wceq 1397   T. wtru 1398

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem depends on definitions:  df-bi 117  df-tru 1400

This theorem is referenced by:  fal  1404  dftru2  1405  mptru  1406  tbtru  1407  bitru  1409  trud  1413  truan  1414  truorfal  1450  falortru  1451  truimfal  1454  nftru  1514  euotd  4347  rabxfr  4567  reuhyp  4569  elabrex  5897  elabrexg  5898  caovcl  6176  caovass  6182  caovdi  6201  ectocl  6770  reef11  12259  mpomulcn  15289  bj-sbimeh  16368  bdtru  16427  bj-nn0suc0  16545