Theorem trud 1550

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

Syntax hints:   → wi 4  ⊤wtru 1541

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 1543

This theorem is referenced by:  falimtru  1565  emptyex  1909  disjprgw  5087  disjprg  5088  euotd  5457  elabrex  7172  riota5f  7322  bj-abv  35186  wl-2mintru1  35766  wl-nax6im  35782  ac6s6  36435  lhpexle1  38276  prjspvs  40709  cnvtrucl0  41553  rfovcnvf1od  41933  elabrexg  42909  thinciso  46692