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 1339 | . 2 | |
2 | mptru.1 | . 2 | |
3 | 1, 2 | ax-mp 5 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wtru 1336 |
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 1338 |
This theorem is referenced by: xorbi12i 1365 nfbi 1569 spime 1721 eubii 2015 nfmo 2026 mobii 2043 dvelimc 2321 ralbii 2463 rexbii 2464 nfralw 2494 nfralxy 2495 nfrexxy 2496 nfralya 2497 nfrexya 2498 nfreuxy 2631 nfsbc1 2954 nfsbc 2957 sbcbii 2996 csbeq2i 3058 nfcsb1 3063 nfcsbw 3067 nfcsb 3068 nfif 3534 ssbri 4010 nfbr 4012 mpteq12i 4054 ralxfr 4428 rexxfr 4430 nfiotaw 5141 nfriota 5791 nfov 5853 mpoeq123i 5886 mpoeq3ia 5888 disjsnxp 6186 tfri1 6314 eqer 6514 0er 6516 ecopover 6580 ecopoverg 6583 nfixpxy 6664 en2i 6717 en3i 6718 ener 6726 ensymb 6727 entr 6731 djuf1olem 6999 omp1eomlem 7040 infnninf 7069 ltsopi 7242 ltsonq 7320 enq0er 7357 ltpopr 7517 ltposr 7685 axcnex 7781 axaddf 7790 axmulf 7791 ltso 7957 nfneg 8076 negiso 8831 sup3exmid 8833 xrltso 9709 frecfzennn 10334 frechashgf1o 10336 0tonninf 10347 1tonninf 10348 facnn 10612 fac0 10613 fac1 10614 cnrecnv 10821 cau3 11026 xrnegiso 11170 sum0 11296 trireciplem 11408 trirecip 11409 ege2le3 11579 oddpwdc 12064 ennnfonelem1 12206 ennnfonelemhf1o 12212 strnfvn 12281 strslss 12307 txswaphmeolem 12790 divcnap 13025 elcncf1ii 13037 cnrehmeocntop 13063 dvid 13132 dveflem 13157 dvef 13158 sincn 13160 coscn 13161 cosz12 13171 sincos6thpi 13233 bj-sttru 13386 bj-dctru 13396 bj-sbimeh 13417 bdnthALT 13481 012of 13638 2o01f 13639 isomninnlem 13672 iooref1o 13676 iswomninnlem 13691 ismkvnnlem 13694 dceqnconst 13701 dcapnconst 13702 taupi 13712 |
Copyright terms: Public domain | W3C validator |