Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  trud Structured version   Visualization version   GIF version

Theorem trud 1548
 Description: Anything implies ⊤. Dual statement of falim 1555. Deduction form of tru 1542. Note on naming: in 2022, the theorem now known as mptru 1545 was renamed from trud so if you are reading documentation written before that time, references to trud refer to what is now mptru 1545. (Contributed by FL, 20-Mar-2011.) (Proof shortened by Anthony Hart, 1-Aug-2011.)
Assertion
Ref Expression
trud (𝜑 → ⊤)

Proof of Theorem trud
StepHypRef Expression
1 tru 1542 . 2
21a1i 11 1 (𝜑 → ⊤)
 Colors of variables: wff setvar class Syntax hints:   → wi 4  ⊤wtru 1539 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 1541 This theorem is referenced by:  falimtru  1563  emptyex  1908  disjprgw  5027  disjprg  5028  euotd  5372  mptexgf  6976  elabrex  6994  riota5f  7136  bj-abv  34627  wl-2mintru1  35187  wl-nax6im  35203  ac6s6  35890  lhpexle1  37584  prjspvs  39946  cnvtrucl0  40697  rfovcnvf1od  41078  elabrexg  42048
 Copyright terms: Public domain W3C validator