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 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.) |
Ref | Expression |
---|---|
trud | ⊢ (𝜑 → ⊤) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | tru 1532 | . 2 ⊢ ⊤ | |
2 | 1 | a1i 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 |