Theorem trud 1557

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

Syntax hints:   → wi 4  ⊤wtru 1548

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 208  df-tru 1550

This theorem is referenced by:  falimtru  1572  emptyex  1914  disjprg  5075  euotd  5461  elabrex  7193  elabrexg  7194  riota5f  7348  bj-exextruan  36985  bj-cbvew  36989  bj-abv  37266  wl-2mintru1  37859  wl-nax6im  37896  ac6s6  38546  lhpexle1  40507  prjspvs  43067  cnvtrucl0  44075  rfovcnvf1od  44455  fsupdm  47292  thinciso  49967