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-1 5 ax-2 6 ax-mp 7 |
This theorem is referenced by: sylc 61 impbid 127 ibi 174 anidms 389 pm2.13dc 812 hbequid 1446 equidqe 1465 equid 1629 ax10 1645 hbae 1646 vtoclgaf 2663 vtocl2gaf 2665 vtocl3gaf 2667 elinti 3645 copsexg 3999 nlimsucg 4309 tfisi 4328 vtoclr 4406 issref 4727 relresfld 4867 f1o2ndf1 5869 tfrlem9 5958 nndi 6088 mulcanpig 6525 lediv2a 7973 iseqid3s 9466 resqrexlemdecn 9898 ndvdssub 10330 nn0seqcvgd 10423 ax1hfs 10786 |
Copyright terms: Public domain | W3C validator |