Metamath Proof Explorer


Theorem nanim

Description: Implication in terms of alternative denial. (Contributed by Jeff Hoffman, 19-Nov-2007)

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

Proof

Step Hyp Ref Expression
1 nannan
 |-  ( ( ph -/\ ( ps -/\ ps ) ) <-> ( ph -> ( ps /\ ps ) ) )
2 anidmdbi
 |-  ( ( ph -> ( ps /\ ps ) ) <-> ( ph -> ps ) )
3 1 2 bitr2i
 |-  ( ( ph -> ps ) <-> ( ph -/\ ( ps -/\ ps ) ) )