Theorem imnan 697

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 642	. . . 4 ⊢ (𝜑 → (𝜓 → ¬ (𝜑 → ¬ 𝜓)))
2	1	imp 124	. . 3 ⊢ ((𝜑 ∧ 𝜓) → ¬ (𝜑 → ¬ 𝜓))
3	2	con2i 632	. 2 ⊢ ((𝜑 → ¬ 𝜓) → ¬ (𝜑 ∧ 𝜓))
4		pm3.2 139	. . 3 ⊢ (𝜑 → (𝜓 → (𝜑 ∧ 𝜓)))
5	4	con3rr3 638	. 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 619  ax-in2 620

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  imnani  698  nan  699  mpnanrd  700  pm3.24  701  imanst  896  ianordc  907  pm5.17dc  912  dn1dc  969  xorbin  1429  xordc1  1438  alinexa  1652  dfrex2dc  2535  ralinexa  2571  rabeq0  3540  disj  3559  minel  3572  disjsn  3753  sotricim  4446  poirr2  5157  funun  5399  imadiflem  5437  imadif  5438  brprcneu  5665  2omotaplemap  7573  prltlu  7804  caucvgprlemnbj  7984  caucvgprprlemnbj  8010  suplocexprlemmu  8035  xrltnsym2  10130  fzp1nel  10442  fsumsplit  12097  sumsplitdc  12122  phiprmpw  12923  odzdvds  12947  pcdvdsb  13022  lgsne0  15928  lgsquadlem3  15969  bj-nnor  16523