![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > pm2.43i | GIF 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 813 hbequid 1447 equidqe 1466 equid 1630 ax10 1647 hbae 1648 vtoclgaf 2672 vtocl2gaf 2674 vtocl3gaf 2676 elinti 3665 copsexg 4027 nlimsucg 4337 tfisi 4356 vtoclr 4434 issref 4757 relresfld 4897 f1o2ndf1 5901 tfrlem9 5989 nndi 6151 mulcanpig 6657 lediv2a 8110 iseqid3s 9632 resqrexlemdecn 10117 ndvdssub 10555 nn0seqcvgd 10648 ax1hfs 11071 |
Copyright terms: Public domain | W3C validator |