Metamath Proof Explorer

Theorem anidmdbi

Description: Conjunction idempotence with antecedent. (Contributed by Roy F. Longton, 8-Aug-2005)

Ref Expression
Assertion anidmdbi 
|- ( ( ph -> ( ps /\ ps ) ) <-> ( ph -> ps ) )

Proof

Step Hyp Ref Expression
1 anidm 
 |-  ( ( ps /\ ps ) <-> ps )
2 1 imbi2i 
 |-  ( ( ph -> ( ps /\ ps ) ) <-> ( ph -> ps ) )