Theorem trud 1544

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

Syntax hints:   → wi 4  ⊤wtru 1535

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 1537

This theorem is referenced by:  falimtru  1559  emptyex  1903  disjprgw  5148  disjprg  5149  euotd  5519  elabrex  7257  elabrexg  7258  riota5f  7409  bj-abv  36612  wl-2mintru1  37197  wl-nax6im  37213  ac6s6  37873  lhpexle1  39707  prjspvs  42264  cnvtrucl0  43291  rfovcnvf1od  43671  fsupdm  46463  thinciso  48381