This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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	$⊢ φ \to ⊤$

Proof

Step	Hyp	Ref	Expression
1		tru	$⊢ ⊤$
2	1	a1i	$⊢ φ \to ⊤$