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

Theorem trud 1538
Description: Anything implies . Dual statement of falim 1545. Deduction form of tru 1532. Note on naming: in 2022, the theorem now known as mptru 1535 was renamed from trud so if you are reading documentation written before that time, references to trud refer to what is now mptru 1535. (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 1532 . 2
21a1i 11 1 (𝜑 → ⊤)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wtru 1529
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 1531
This theorem is referenced by:  falimtru  1553  emptyex  1899  disjprgw  5053  disjprg  5054  euotd  5395  mptexgf  6977  elabrex  6993  riota5f  7131  wl-nax6im  34641  ac6s6  35333  lhpexle1  37026  prjspvs  39140  cnvtrucl0  39864  rfovcnvf1od  40230  elabrexg  41183
  Copyright terms: Public domain W3C validator