Theorem dfnot 1217

Description: One definition of negation in logics that take ⊥ as axiomatic is via "implies contradiction", i.e. φ → ⊥. (Contributed by Mario Carneiro, 2-Feb-2015.)

Assertion

Ref	Expression
dfnot	⊢ (¬ φ ↔ (φ → ⊥ ))

Proof of Theorem dfnot

Step	Hyp	Ref	Expression
1		fal 1207	. 2 ⊢ ¬ ⊥
2		mtt 592	. 2 ⊢ (¬ ⊥ → (¬ φ ↔ (φ → ⊥ )))
3	1, 2	ax-mp 7	1 ⊢ (¬ φ ↔ (φ → ⊥ ))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 96   ⊥ wfal 1202

This theorem is referenced by:  inegd  1218  pclem6  1219  alnex  1335  alexim  1480  difin  3059  indifdir  3078

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 97  ax-ia2 98  ax-ia3 99  ax-in1 528  ax-in2 529

This theorem depends on definitions:  df-bi 108  df-tru 1204  df-fal 1205