![]() |
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 1821 rgen2a 2544 rspct 2849 po2nr 4327 ordsuc 4580 funssres 5277 2elresin 5346 f1imass 5796 smoel 6325 tfri3 6392 nnmass 6512 sbthlem1 6986 genpcdl 7548 genpcuu 7549 recexprlemss1l 7664 recexprlemss1u 7665 grpid 12983 uniopn 13958 elabgft1 14988 bj-rspgt 14996 |
Copyright terms: Public domain | W3C validator |