Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > mptru | Unicode 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 1352 | . 2 | |
2 | mptru.1 | . 2 | |
3 | 1, 2 | ax-mp 5 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wtru 1349 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 |
This theorem depends on definitions: df-bi 116 df-tru 1351 |
This theorem is referenced by: xorbi12i 1378 nfbi 1582 spime 1734 eubii 2028 nfmo 2039 mobii 2056 dvelimc 2334 ralbii 2476 rexbii 2477 nfralw 2507 nfralxy 2508 nfrexxy 2509 nfralya 2510 nfrexya 2511 nfreuxy 2644 nfsbc1 2972 nfsbc 2975 sbcbii 3014 csbeq2i 3076 nfcsb1 3081 nfcsbw 3085 nfcsb 3086 nfif 3554 ssbri 4033 nfbr 4035 mpteq12i 4077 ralxfr 4451 rexxfr 4453 nfiotaw 5164 nfriota 5818 nfov 5883 mpoeq123i 5916 mpoeq3ia 5918 disjsnxp 6216 tfri1 6344 eqer 6545 0er 6547 ecopover 6611 ecopoverg 6614 nfixpxy 6695 en2i 6748 en3i 6749 ener 6757 ensymb 6758 entr 6762 djuf1olem 7030 omp1eomlem 7071 infnninf 7100 ltsopi 7282 ltsonq 7360 enq0er 7397 ltpopr 7557 ltposr 7725 axcnex 7821 axaddf 7830 axmulf 7831 ltso 7997 nfneg 8116 negiso 8871 sup3exmid 8873 xrltso 9753 frecfzennn 10382 frechashgf1o 10384 0tonninf 10395 1tonninf 10396 facnn 10661 fac0 10662 fac1 10663 cnrecnv 10874 cau3 11079 xrnegiso 11225 sum0 11351 trireciplem 11463 trirecip 11464 ege2le3 11634 oddpwdc 12128 ennnfonelem1 12362 ennnfonelemhf1o 12368 strnfvn 12437 strslss 12463 mndprop 12677 grpprop 12725 isgrpi 12730 txswaphmeolem 13114 divcnap 13349 elcncf1ii 13361 cnrehmeocntop 13387 dvid 13456 dveflem 13481 dvef 13482 sincn 13484 coscn 13485 cosz12 13495 sincos6thpi 13557 lgsdir2lem5 13727 bj-sttru 13775 bj-dctru 13788 bj-sbimeh 13807 bdnthALT 13870 012of 14028 2o01f 14029 isomninnlem 14062 iooref1o 14066 iswomninnlem 14081 ismkvnnlem 14084 dceqnconst 14091 dcapnconst 14092 taupi 14102 |
Copyright terms: Public domain | W3C validator |