![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > pm2.43d | GIF version |
Description: Deduction absorbing redundant antecedent. (Contributed by NM, 18-Aug-1993.) (Proof shortened by O'Cat, 28-Nov-2008.) |
Ref | Expression |
---|---|
pm2.43d.1 | ⊢ (𝜑 → (𝜓 → (𝜓 → 𝜒))) |
Ref | Expression |
---|---|
pm2.43d | ⊢ (𝜑 → (𝜓 → 𝜒)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | id 19 | . 2 ⊢ (𝜓 → 𝜓) | |
2 | pm2.43d.1 | . 2 ⊢ (𝜑 → (𝜓 → (𝜓 → 𝜒))) | |
3 | 1, 2 | mpdi 43 | 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: loolin 102 pm2.18dc 856 sbcof2 1820 rgen2a 2541 rspct 2846 po2nr 4321 ordsuc 4574 funssres 5270 2elresin 5339 f1imass 5788 smoel 6315 tfri3 6382 nnmass 6502 sbthlem1 6970 genpcdl 7532 genpcuu 7533 recexprlemss1l 7648 recexprlemss1u 7649 grpid 12936 uniopn 13797 elabgft1 14826 bj-rspgt 14834 |
Copyright terms: Public domain | W3C validator |