Theorem trud 1580

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

This proof depends on syntax axioms:   → wi 4  ⊤wtru 1571

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-tru 1573

This theorem is used by:  falimtru  1595  emptyex  1940  disjprg  5107  euotd  5498  elabrex  7242  elabrexg  7243  riota5f  7401  bj-exextruan  37293  bj-cbvew  37297  bj-abv  37574  wl-2mintru1  38169  wl-nax6im  38206  ac6s6  38854  lhpexle1  40815  prjspvs  43375  cnvtrucl0  44383  rfovcnvf1od  44763  fsupdm  47589  thinciso  50281