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 | ⊢ ( 𝜑 → 𝜓 ) |