Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > pm2.43i | Unicode version |
Description: Inference absorbing redundant antecedent. (Contributed by NM, 5-Aug-1993.) (Proof shortened by O'Cat, 28-Nov-2008.) |
Ref | Expression |
---|---|
pm2.43i.1 |
Ref | Expression |
---|---|
pm2.43i |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | id 19 | . 2 | |
2 | pm2.43i.1 | . 2 | |
3 | 1, 2 | mpd 13 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 |
This theorem is referenced by: sylc 62 impbid 128 ibi 175 anidms 394 pm2.13dc 855 hbequid 1478 equidqe 1497 equid 1662 ax10 1680 hbae 1681 vtoclgaf 2725 vtocl2gaf 2727 vtocl3gaf 2729 ifmdc 3479 elinti 3750 copsexg 4136 nlimsucg 4451 tfisi 4471 vtoclr 4557 issref 4891 relresfld 5038 f1o2ndf1 6093 tfrlem9 6184 nndi 6350 mulcanpig 7111 lediv2a 8617 seq3id3 10235 resqrexlemdecn 10739 ndvdssub 11539 nn0seqcvgd 11634 fiinopn 12082 xmetunirn 12438 mopnval 12522 ax1hfs 13135 |
Copyright terms: Public domain | W3C validator |