Theorem annim 414

Description: Express conjunction in terms of implication. (Contributed by NM, 2-Aug-1994.)

Assertion

Ref	Expression
annim	⊢ ((φ ∧ ¬ ψ) ↔ ¬ (φ → ψ))

Proof of Theorem annim

Step	Hyp	Ref	Expression
1		iman 413	. 2 ⊢ ((φ → ψ) ↔ ¬ (φ ∧ ¬ ψ))
2	1	con2bii 322	1 ⊢ ((φ ∧ ¬ ψ) ↔ ¬ (φ → ψ))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 176   ∧ wa 358

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 177  df-an 360

This theorem is referenced by:  pm4.61  415  pm4.52  477  xordi  865  exanali  1585  19.35  1600  rexanali  2661  r19.35  2759  difin0ss  3617  dfpw2  4328  nnsucelrlem1  4425  evenodddisjlem1  4516  nnadjoinlem1  4520  sfintfinlem1  4532  tfinnnlem1  4534  nchoicelem10  6299  nchoicelem11  6300