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 ( ( 𝜑 ⊼ ( 𝜓𝜒 ) ) ↔ ( 𝜑 → ( 𝜓𝜒 ) ) )

Proof

Step Hyp Ref Expression
1 dfnan2 ( ( 𝜑 ⊼ ( 𝜓𝜒 ) ) ↔ ( 𝜑 → ¬ ( 𝜓𝜒 ) ) )
2 nanan ( ( 𝜓𝜒 ) ↔ ¬ ( 𝜓𝜒 ) )
3 2 imbi2i ( ( 𝜑 → ( 𝜓𝜒 ) ) ↔ ( 𝜑 → ¬ ( 𝜓𝜒 ) ) )
4 1 3 bitr4i ( ( 𝜑 ⊼ ( 𝜓𝜒 ) ) ↔ ( 𝜑 → ( 𝜓𝜒 ) ) )