Metamath Proof Explorer


Theorem pm2.43i

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
|- ( ph -> ( ph -> ps ) )
Assertion pm2.43i
|- ( ph -> ps )

Proof

Step Hyp Ref Expression
1 pm2.43i.1
 |-  ( ph -> ( ph -> ps ) )
2 id
 |-  ( ph -> ph )
3 2 1 mpd
 |-  ( ph -> ps )