Metamath Proof Explorer

Theorem anidms

Description: Inference from idempotent law for conjunction. (Contributed by NM, 15-Jun-1994)

Ref Expression
Hypothesis anidms.1 
|- ( ( ph /\ ph ) -> ps )
Assertion anidms 
|- ( ph -> ps )

Proof

Step Hyp Ref Expression
1 anidms.1 
 |-  ( ( ph /\ ph ) -> ps )
2 1 ex 
 |-  ( ph -> ( ph -> ps ) )
3 2 pm2.43i 
 |-  ( ph -> ps )