Theorem trud 1569

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

Syntax hints:   → wi 4  ⊤wtru 1560

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 209  df-tru 1562

This theorem is referenced by:  falimtru  1584  emptyex  1926  disjprg  5093  euotd  5479  elabrex  7220  elabrexg  7221  riota5f  7375  bj-exextruan  37070  bj-cbvew  37074  bj-abv  37351  wl-2mintru1  37944  wl-nax6im  37981  ac6s6  38631  lhpexle1  40592  prjspvs  43152  cnvtrucl0  44160  rfovcnvf1od  44540  fsupdm  47376  thinciso  50051