Theorem trud 1546

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

Assertion

Ref	Expression
trud	⊢ (𝜑 → ⊤)

Proof of Theorem trud

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

Syntax hints:   → wi 4  ⊤wtru 1537

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 209  df-tru 1539

This theorem is referenced by:  falimtru  1561  emptyex  1907  disjprgw  5064  disjprg  5065  euotd  5406  mptexgf  6988  elabrex  7005  riota5f  7145  wl-nax6im  34762  ac6s6  35454  lhpexle1  37148  prjspvs  39266  cnvtrucl0  39990  rfovcnvf1od  40356  elabrexg  41309