Metamath Proof Explorer


Theorem anidms

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

Ref Expression
Hypothesis anidms.1 φ φ ψ
Assertion anidms φ ψ

Proof

Step Hyp Ref Expression
1 anidms.1 φ φ ψ
2 1 ex φ φ ψ
3 2 pm2.43i φ ψ