| 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 1557. Deduction form of tru 1544. Note on naming: in 2022, the theorem now known as mptru 1547 was renamed from trud so if you are reading documentation written before that time, references to trud refer to what is now mptru 1547. (Contributed by FL, 20-Mar-2011.) (Proof shortened by Anthony Hart, 1-Aug-2011.) |
| Ref | Expression |
|---|---|
| trud | ⊢ (𝜑 → ⊤) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | tru 1544 | . 2 ⊢ ⊤ | |
| 2 | 1 | a1i 11 | 1 ⊢ (𝜑 → ⊤) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ⊤wtru 1541 |
| 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 207 df-tru 1543 |
| This theorem is referenced by: falimtru 1565 emptyex 1907 disjprg 5139 euotd 5518 elabrex 7262 elabrexg 7263 riota5f 7416 bj-abv 36907 wl-2mintru1 37491 wl-nax6im 37519 ac6s6 38179 lhpexle1 40010 prjspvs 42620 cnvtrucl0 43637 rfovcnvf1od 44017 fsupdm 46857 thinciso 49117 |
| Copyright terms: Public domain | W3C validator |