Theorem imnan 662

Description: Express implication in terms of conjunction. (Contributed by NM, 9-Apr-1994.) (Revised by Mario Carneiro, 1-Feb-2015.)

Assertion

Ref	Expression
imnan	⊢ ((𝜑 → ¬ 𝜓) ↔ ¬ (𝜑 ∧ 𝜓))

Proof of Theorem imnan

Step	Hyp	Ref	Expression
1		pm3.2im 609	. . . 4 ⊢ (𝜑 → (𝜓 → ¬ (𝜑 → ¬ 𝜓)))
2	1	imp 123	. . 3 ⊢ ((𝜑 ∧ 𝜓) → ¬ (𝜑 → ¬ 𝜓))
3	2	con2i 599	. 2 ⊢ ((𝜑 → ¬ 𝜓) → ¬ (𝜑 ∧ 𝜓))
4		pm3.2 138	. . 3 ⊢ (𝜑 → (𝜓 → (𝜑 ∧ 𝜓)))
5	4	con3rr3 605	. 2 ⊢ (¬ (𝜑 ∧ 𝜓) → (𝜑 → ¬ 𝜓))
6	3, 5	impbii 125	1 ⊢ ((𝜑 → ¬ 𝜓) ↔ ¬ (𝜑 ∧ 𝜓))

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 103   ↔ wb 104

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 586  ax-in2 587

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  imnani  663  nan  664  pm3.24  665  imanst  856  ianordc  867  pm5.17dc  872  dn1dc  927  xorbin  1345  xordc1  1354  alinexa  1565  dfrex2dc  2402  ralinexa  2436  rabeq0  3358  disj  3377  minel  3390  disjsn  3551  sotricim  4205  poirr2  4889  funun  5125  imadiflem  5160  imadif  5161  brprcneu  5368  prltlu  7240  caucvgprlemnbj  7420  caucvgprprlemnbj  7446  xrltnsym2  9470  fzp1nel  9774  fsumsplit  11065  sumsplitdc  11090  phiprmpw  11740  bj-nnor  12633