Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Jarvin Udandy
atbiffatnnb
Next ⟩
bisaiaisb
Metamath Proof Explorer
Ascii
Unicode
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
⊢
φ
→
ψ
→
φ
→
¬
¬
ψ