![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > mptru | GIF version |
Description: Eliminate ⊤ as an antecedent. A proposition implied by ⊤ is true. (Contributed by Mario Carneiro, 13-Mar-2014.) |
Ref | Expression |
---|---|
mptru.1 | ⊢ (⊤ → 𝜑) |
Ref | Expression |
---|---|
mptru | ⊢ 𝜑 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | tru 1357 | . 2 ⊢ ⊤ | |
2 | mptru.1 | . 2 ⊢ (⊤ → 𝜑) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ 𝜑 |
Colors of variables: wff set class |
Syntax hints: → wi 4 ⊤wtru 1354 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 |
This theorem depends on definitions: df-bi 117 df-tru 1356 |
This theorem is referenced by: xorbi12i 1383 nfbi 1589 spime 1741 eubii 2035 nfmo 2046 mobii 2063 dvelimc 2341 ralbii 2483 rexbii 2484 nfralw 2514 nfralxy 2515 nfrexxy 2516 nfralya 2517 nfrexya 2518 nfreuxy 2651 nfsbc1 2980 nfsbc 2983 sbcbii 3022 csbeq2i 3084 nfcsb1 3089 nfcsbw 3093 nfcsb 3094 nfif 3562 ssbri 4047 nfbr 4049 mpteq12i 4091 ralxfr 4466 rexxfr 4468 nfiotaw 5182 nfriota 5839 nfov 5904 mpoeq123i 5937 mpoeq3ia 5939 disjsnxp 6237 tfri1 6365 eqer 6566 0er 6568 ecopover 6632 ecopoverg 6635 nfixpxy 6716 en2i 6769 en3i 6770 ener 6778 ensymb 6779 entr 6783 djuf1olem 7051 omp1eomlem 7092 infnninf 7121 ltsopi 7318 ltsonq 7396 enq0er 7433 ltpopr 7593 ltposr 7761 axcnex 7857 axaddf 7866 axmulf 7867 ltso 8033 nfneg 8152 negiso 8910 sup3exmid 8912 xrltso 9794 frecfzennn 10423 frechashgf1o 10425 0tonninf 10436 1tonninf 10437 facnn 10702 fac0 10703 fac1 10704 cnrecnv 10914 cau3 11119 xrnegiso 11265 sum0 11391 trireciplem 11503 trirecip 11504 ege2le3 11674 oddpwdc 12168 ennnfonelem1 12402 ennnfonelemhf1o 12408 strnfvn 12477 strslss 12504 mndprop 12796 grpprop 12848 isgrpi 12854 ablprop 13053 ringprop 13172 cnfldstr 13348 cncrng 13354 zringbas 13377 zringplusg 13378 dvdsrzring 13384 txswaphmeolem 13713 divcnap 13948 elcncf1ii 13960 cnrehmeocntop 13986 dvid 14055 dveflem 14080 dvef 14081 sincn 14083 coscn 14084 cosz12 14094 sincos6thpi 14156 lgsdir2lem5 14326 bj-sttru 14374 bj-dctru 14387 bj-sbimeh 14406 bdnthALT 14469 012of 14627 2o01f 14628 isomninnlem 14660 iooref1o 14664 iswomninnlem 14679 ismkvnnlem 14682 dceqnconst 14689 dcapnconst 14690 taupi 14702 |
Copyright terms: Public domain | W3C validator |