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-1 5  ax-2 6  ax-3 7  ax-mp 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  2660  r19.35  2758  difin0ss  3616  dfpw2  4327  nnsucelrlem1  4424  evenodddisjlem1  4515  nnadjoinlem1  4519  sfintfinlem1  4531  tfinnnlem1  4533  nchoicelem10  6298  nchoicelem11  6299