Description: Implication in terms of alternative denial. (Contributed by Jeff Hoffman, 19-Nov-2007)
Ref | Expression | ||
---|---|---|---|
Assertion | nanim | |- ( ( ph -> ps ) <-> ( ph -/\ ( ps -/\ ps ) ) ) |
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 ) ) ) |