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 56 impbid 120 ibi 165 anidms 377 pm2.13dc 779 hbequid 1406 equidqe 1425 equid 1589 ax10 1605 hbae 1606 vtoclgaf 2618 vtocl2gaf 2620 vtocl3gaf 2622 elinti 3624 copsexg 3981 nlimsucg 4290 tfisi 4310 vtoclr 4388 issref 4707 relresfld 4847 f1o2ndf1 5849 tfrlem9 5935 nndi 6065 mulcanpig 6433 lediv2a 7861 iseqid3s 9246 resqrexlemdecn 9610 nn0seqcvgd 9880 ax1hfs 9898 |
Copyright terms: Public domain | W3C validator |