Theorem iman 205

Description: Express implication in terms of conjunction. Theorem 3.4(27) of [Stoll] p. 176.

Assertion

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

Proof of Theorem iman

Step	Hyp	Ref	Expression
1		pm4.13 142	. . 3 ⊢ (ψ ↔ ¬ ¬ ψ)
2	1	imbi2i 160	. 2 ⊢ ((φ → ψ) ↔ (φ → ¬ ¬ ψ))
3		df-an 198	. . 3 ⊢ ((φ ∧ ¬ ψ) ↔ ¬ (φ → ¬ ¬ ψ))
4	3	bicon2i 194	. 2 ⊢ ((φ → ¬ ¬ ψ) ↔ ¬ (φ ∧ ¬ ψ))
5	2, 4	bitr 151	1 ⊢ ((φ → ψ) ↔ ¬ (φ ∧ ¬ ψ))

Syntax hints:  ¬ wn 1   → wi 2   ↔ wb 127   ∧ wa 196

This theorem is referenced by:  annim 206  dfbi 499  exanali 725  dfpss3 1558  difdif 1595  dfss4 1667  ssdif0 1748  difin0ss 1753  inssdif0 1754  fr0 2179  inf3lem3 3466  kmlem4 3583  nominpos 4509  cvbr2t 5715  cvnbtwn2t 5719  cvnbtwn3t 5720  cvnbtwn4t 5721  chpssat 5756  chrelat2 5758  chrelat3t 5762

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

This theorem depends on definitions:  df-bi 128  df-an 198

metamath.org