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 ⊢ (𝜑 → ⊤)

Syntax hints:   → wi 4  ⊤wtru 1571

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 210  df-tru 1573

This theorem is referenced by:  falimtru  1595  emptyex  1937  disjprg  5106  euotd  5498  elabrex  7242  elabrexg  7243  riota5f  7397  bj-exextruan  37241  bj-cbvew  37245  bj-abv  37522  wl-2mintru1  38117  wl-nax6im  38154  ac6s6  38802  lhpexle1  40763  prjspvs  43325  cnvtrucl0  44333  rfovcnvf1od  44713  fsupdm  47539  thinciso  50231