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