Description: Inference absorbing redundant antecedent. Inference associated with pm2.43 . (Contributed by NM, 10-Jan-1993) (Proof shortened by Mel L. O'Cat, 28-Nov-2008)
Ref | Expression | ||
---|---|---|---|
Hypothesis | pm2.43i.1 | ⊢ ( 𝜑 → ( 𝜑 → 𝜓 ) ) | |
Assertion | pm2.43i | ⊢ ( 𝜑 → 𝜓 ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | pm2.43i.1 | ⊢ ( 𝜑 → ( 𝜑 → 𝜓 ) ) | |
2 | id | ⊢ ( 𝜑 → 𝜑 ) | |
3 | 2 1 | mpd | ⊢ ( 𝜑 → 𝜓 ) |