Metamath Proof Explorer


Theorem nannan

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

Proof

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