![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > trud | GIF version |
Description: Eliminate ⊤ as an antecedent. A proposition implied by ⊤ is true. (Contributed by Mario Carneiro, 13-Mar-2014.) |
Ref | Expression |
---|---|
trud.1 | ⊢ (⊤ → 𝜑) |
Ref | Expression |
---|---|
trud | ⊢ 𝜑 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | tru 1289 | . 2 ⊢ ⊤ | |
2 | trud.1 | . 2 ⊢ (⊤ → 𝜑) | |
3 | 1, 2 | ax-mp 7 | 1 ⊢ 𝜑 |
Colors of variables: wff set class |
Syntax hints: → wi 4 ⊤wtru 1286 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 104 ax-ia2 105 ax-ia3 106 |
This theorem depends on definitions: df-bi 115 df-tru 1288 |
This theorem is referenced by: xorbi12i 1315 nfbi 1522 spime 1670 eubii 1951 nfmo 1962 mobii 1979 dvelimc 2240 ralbii 2373 rexbii 2374 nfralxy 2403 nfrexxy 2404 nfralya 2405 nfrexya 2406 nfreuxy 2529 nfsbc1 2833 nfsbc 2836 sbcbii 2874 csbeq2i 2933 nfcsb1 2938 nfcsb 2941 nfif 3385 ssbri 3835 nfbr 3837 mpteq12i 3874 ralxfr 4224 rexxfr 4226 nfiotaxy 4901 nfriota 5508 nfov 5566 mpt2eq123i 5599 mpt2eq3ia 5601 tfri1 6014 eqer 6204 0er 6206 ecopover 6270 ecopoverg 6273 en2i 6317 en3i 6318 ener 6326 ensymb 6327 entr 6331 ltsopi 6572 ltsonq 6650 enq0er 6687 ltpopr 6847 ltposr 7002 axcnex 7089 ltso 7256 nfneg 7372 negiso 8100 xrltso 8947 frecfzennn 9508 frechashgf1o 9510 facnn 9751 fac0 9752 fac1 9753 cnrecnv 9935 cau3 10139 oddpwdc 10696 bj-sbimeh 10734 bdnthALT 10784 |
Copyright terms: Public domain | W3C validator |