Theorem trud

Description: Anything implies T. . Dual statement of falim . Deduction form of tru . Note on naming: in 2022, the theorem now known as mptru was renamed from trud so if you are reading documentation written before that time, references to trud refer to what is now mptru . (Contributed by FL, 20-Mar-2011) (Proof shortened by Anthony Hart, 1-Aug-2011)

	Ref	Expression
Assertion	trud	⊢ ( 𝜑 → ⊤ )

Proof

Step	Hyp	Ref	Expression
1		tru	⊢ ⊤
2	1	a1i	⊢ ( 𝜑 → ⊤ )