Description: Nested alternative denials. (Contributed by Jeff Hoffman, 19-Nov-2007) (Proof shortened by Wolf Lammen, 26-Jun-2020)
Ref | Expression | ||
---|---|---|---|
Assertion | nannan | |- ( ( ph -/\ ( ps -/\ ch ) ) <-> ( ph -> ( ps /\ ch ) ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | dfnan2 | |- ( ( ph -/\ ( ps -/\ ch ) ) <-> ( ph -> -. ( ps -/\ ch ) ) ) |
|
2 | nanan | |- ( ( ps /\ ch ) <-> -. ( ps -/\ ch ) ) |
|
3 | 2 | imbi2i | |- ( ( ph -> ( ps /\ ch ) ) <-> ( ph -> -. ( ps -/\ ch ) ) ) |
4 | 1 3 | bitr4i | |- ( ( ph -/\ ( ps -/\ ch ) ) <-> ( ph -> ( ps /\ ch ) ) ) |