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 ) ) )