Metamath Proof Explorer

Theorem atbiffatnnb

Description: If a implies b, then a implies not not b. (Contributed by Jarvin Udandy, 28-Aug-2016)

Ref Expression
Assertion atbiffatnnb 
|- ( ( ph -> ps ) -> ( ph -> -. -. ps ) )

Proof

Step Hyp Ref Expression
1 idd 
 |-  ( ph -> ( ps -> ps ) )
2 notnotb 
 |-  ( ps <-> -. -. ps )
3 1 2 imbitrdi 
 |-  ( ph -> ( ps -> -. -. ps ) )
4 3 a2i 
 |-  ( ( ph -> ps ) -> ( ph -> -. -. ps ) )