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 101 pm2.18dc 825 sbcof2 1766 rgen2a 2463 rspct 2756 po2nr 4201 ordsuc 4448 funssres 5135 2elresin 5204 f1imass 5643 smoel 6165 tfri3 6232 nnmass 6351 sbthlem1 6813 genpcdl 7295 genpcuu 7296 recexprlemss1l 7411 recexprlemss1u 7412 uniopn 12095 elabgft1 12912 bj-rspgt 12920 |
Copyright terms: Public domain | W3C validator |