Theorem tru 1321

Description: ⊤ is provable. (Contributed by Anthony Hart, 13-Oct-2010.)

Assertion

Ref	Expression
tru	⊢ ⊤

Proof of Theorem tru

Step	Hyp	Ref	Expression
1		biid 227	. 2 ⊢ (φ ↔ φ)
2		df-tru 1319	. 2 ⊢ ( ⊤ ↔ (φ ↔ φ))
3	1, 2	mpbir 200	1 ⊢ ⊤

Syntax hints:   ↔ wb 176   ⊤ wtru 1316

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 177  df-tru 1319

This theorem is referenced by:  fal  1322  trud  1323  tbtru  1324  bitru  1326  a1tru  1330  truorfal  1341  falortru  1342  truimfal  1345  cadtru  1401  nftru  1554  cbv3  1982  finds  4412  caovcl  5624  caovass  5628  caovdi  5635  ectocl  5993