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

Theorem trud 1532
Description: Anything implies . Dual statement of falim 1539. Deduction form of tru 1526. Note on naming: in 2022, the theorem now known as mptru 1529 was renamed from trud so if you are reading documentation written before that time, references to trud refer to what is now mptru 1529. (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 1526 . 2
21a1i 11 1 (𝜑 → ⊤)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wtru 1523
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 1525
This theorem is referenced by:  falimtru  1547  disjprg  4958  euotd  5294  mptexgf  6851  elabrex  6867  riota5f  7002  wl-nax6im  34308  wl-nax6al  34309  ac6s6  35001  lhpexle1  36694  prjspvs  38776  cnvtrucl0  39488  rfovcnvf1od  39854  elabrexg  40861
  Copyright terms: Public domain W3C validator