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  4414  poirr2  5121  funun  5362  imadiflem  5400  imadif  5401  brprcneu  5622  2omotaplemap  7454  prltlu  7685  caucvgprlemnbj  7865  caucvgprprlemnbj  7891  suplocexprlemmu  7916  xrltnsym2  10002  fzp1nel  10312  fsumsplit  11933  sumsplitdc  11958  phiprmpw  12759  odzdvds  12783  pcdvdsb  12858  lgsne0  15732  lgsquadlem3  15773  bj-nnor  16153