Theorem imnan 692

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 638	. . . 4 ⊢ (𝜑 → (𝜓 → ¬ (𝜑 → ¬ 𝜓)))
2	1	imp 124	. . 3 ⊢ ((𝜑 ∧ 𝜓) → ¬ (𝜑 → ¬ 𝜓))
3	2	con2i 628	. 2 ⊢ ((𝜑 → ¬ 𝜓) → ¬ (𝜑 ∧ 𝜓))
4		pm3.2 139	. . 3 ⊢ (𝜑 → (𝜓 → (𝜑 ∧ 𝜓)))
5	4	con3rr3 634	. 2 ⊢ (¬ (𝜑 ∧ 𝜓) → (𝜑 → ¬ 𝜓))
6	3, 5	impbii 126	1 ⊢ ((𝜑 → ¬ 𝜓) ↔ ¬ (𝜑 ∧ 𝜓))

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 615  ax-in2 616

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  imnani  693  nan  694  pm3.24  695  imanst  890  ianordc  901  pm5.17dc  906  dn1dc  963  xorbin  1404  xordc1  1413  alinexa  1627  dfrex2dc  2499  ralinexa  2535  rabeq0  3498  disj  3517  minel  3530  disjsn  3705  sotricim  4388  poirr2  5094  funun  5334  imadiflem  5372  imadif  5373  brprcneu  5592  2omotaplemap  7404  prltlu  7635  caucvgprlemnbj  7815  caucvgprprlemnbj  7841  suplocexprlemmu  7866  xrltnsym2  9951  fzp1nel  10261  fsumsplit  11833  sumsplitdc  11858  phiprmpw  12659  odzdvds  12683  pcdvdsb  12758  lgsne0  15630  lgsquadlem3  15671  bj-nnor  15870