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 φ ψ φ ¬ ¬ ψ