Theorem imnan 694

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 640	. . . 4 ⊢ (𝜑 → (𝜓 → ¬ (𝜑 → ¬ 𝜓)))
2	1	imp 124	. . 3 ⊢ ((𝜑 ∧ 𝜓) → ¬ (𝜑 → ¬ 𝜓))
3	2	con2i 630	. 2 ⊢ ((𝜑 → ¬ 𝜓) → ¬ (𝜑 ∧ 𝜓))
4		pm3.2 139	. . 3 ⊢ (𝜑 → (𝜓 → (𝜑 ∧ 𝜓)))
5	4	con3rr3 636	. 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 617  ax-in2 618

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  imnani  695  nan  696  mpnanrd  697  pm3.24  698  imanst  893  ianordc  904  pm5.17dc  909  dn1dc  966  xorbin  1426  xordc1  1435  alinexa  1649  dfrex2dc  2521  ralinexa  2557  rabeq0  3521  disj  3540  minel  3553  disjsn  3728  sotricim  4413  poirr2  5120  funun  5361  imadiflem  5399  imadif  5400  brprcneu  5619  2omotaplemap  7439  prltlu  7670  caucvgprlemnbj  7850  caucvgprprlemnbj  7876  suplocexprlemmu  7901  xrltnsym2  9986  fzp1nel  10296  fsumsplit  11913  sumsplitdc  11938  phiprmpw  12739  odzdvds  12763  pcdvdsb  12838  lgsne0  15711  lgsquadlem3  15752  bj-nnor  16056