Metamath Proof Explorer

Theorem idd

Description: Principle of identity id with antecedent. (Contributed by NM, 26-Nov-1995)

Ref Expression
Assertion idd 
|- ( ph -> ( ps -> ps ) )

Proof

Step Hyp Ref Expression
1 id 
 |-  ( ps -> ps )
2 1 a1i 
 |-  ( ph -> ( ps -> ps ) )