Theorem trut 1492

Description: A proposition is equivalent to it being implied by T.. Closed form of trud 1493. Dual of dfnot 1502. It is to tbtru 1494 what a1bi 352 is to tbt 359. (Contributed by BJ, 26-Oct-2019.)

Assertion

Ref	Expression
trut	|- ( ph <-> ( T. -> ph ) )

Proof of Theorem trut

Step	Hyp	Ref	Expression
1		tru 1487	. 2 |- T.
2	1	a1bi 352	1 |- ( ph <-> ( T. -> ph ) )

Syntax hints:   -> wi 4   <-> wb 196   T. wtru 1484

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 197  df-tru 1486

This theorem is referenced by:  truimfal  1515