![]() |
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 42 | 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: loolin 100 pm2.18dc 788 sbcof2 1738 rgen2a 2429 rspct 2715 po2nr 4136 ordsuc 4379 funssres 5056 2elresin 5125 f1imass 5553 smoel 6065 tfri3 6132 nnmass 6248 sbthlem1 6666 genpcdl 7078 genpcuu 7079 recexprlemss1l 7194 recexprlemss1u 7195 uniopn 11598 elabgft1 11678 bj-rspgt 11686 |
Copyright terms: Public domain | W3C validator |