Theorem trud 1551

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

Syntax hints:   → wi 4  ⊤wtru 1542

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 1544

This theorem is referenced by:  falimtru  1566  emptyex  1913  disjprgw  5073  disjprg  5074  euotd  5429  mptexgf  7092  elabrex  7110  riota5f  7254  bj-abv  35070  wl-2mintru1  35640  wl-nax6im  35656  ac6s6  36309  lhpexle1  38001  prjspvs  40429  cnvtrucl0  41185  rfovcnvf1od  41565  elabrexg  42542  thinciso  46293