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-mp 5 ax-1 6 ax-2 7 |
This theorem is referenced by: sylc 62 impbid 128 ibi 175 anidms 395 pm2.13dc 880 hbequid 1506 equidqe 1525 equid 1694 ax10 1710 hbae 1711 vtoclgaf 2795 vtocl2gaf 2797 vtocl3gaf 2799 ifmdc 3565 elinti 3840 copsexg 4229 nlimsucg 4550 tfisi 4571 vtoclr 4659 issref 4993 relresfld 5140 f1o2ndf1 6207 tfrlem9 6298 nndi 6465 mulcanpig 7297 lediv2a 8811 seq3id3 10463 resqrexlemdecn 10976 ndvdssub 11889 nn0seqcvgd 11995 modprm0 12208 fiinopn 12796 xmetunirn 13152 mopnval 13236 ax1hfs 14103 |
Copyright terms: Public domain | W3C validator |