![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > trud | Structured version Visualization version GIF version |
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.) |
Ref | Expression |
---|---|
trud | ⊢ (𝜑 → ⊤) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | tru 1526 | . 2 ⊢ ⊤ | |
2 | 1 | a1i 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 |