Theorem trud 1549

Description: Anything implies ⊤. Dual statement of falim 1556. Deduction form of tru 1543. Note on naming: in 2022, the theorem now known as mptru 1546 was renamed from trud so if you are reading documentation written before that time, references to trud refer to what is now mptru 1546. (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 1543	. 2 ⊢ ⊤
2	1	a1i 11	1 ⊢ (𝜑 → ⊤)

Syntax hints:   → wi 4  ⊤wtru 1540

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 206  df-tru 1542

This theorem is referenced by:  falimtru  1564  emptyex  1908  disjprgw  5076  disjprg  5077  euotd  5440  elabrex  7148  riota5f  7293  bj-abv  35139  wl-2mintru1  35709  wl-nax6im  35725  ac6s6  36378  lhpexle1  38222  prjspvs  40644  cnvtrucl0  41445  rfovcnvf1od  41825  elabrexg  42802  thinciso  46585