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 ( ( 𝜑𝜓 ) → ( 𝜑 → ¬ ¬ 𝜓 ) )

Proof

Step Hyp Ref Expression
1 idd ( 𝜑 → ( 𝜓𝜓 ) )
2 notnotb ( 𝜓 ↔ ¬ ¬ 𝜓 )
3 1 2 syl6ib ( 𝜑 → ( 𝜓 → ¬ ¬ 𝜓 ) )
4 3 a2i ( ( 𝜑𝜓 ) → ( 𝜑 → ¬ ¬ 𝜓 ) )