NFE Home New Foundations Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  NFE Home  >  Th. List  >  tru GIF version

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

Proof of Theorem tru
StepHypRef Expression
1 biid 227 . 2 (φφ)
2 df-tru 1319 . 2 ( ⊤ ↔ (φφ))
31, 2mpbir 200 1
Colors of variables: wff setvar class
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  4411  caovcl  5623  caovass  5627  caovdi  5634  ectocl  5992
  Copyright terms: Public domain W3C validator