Theorem imnan 696

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  697  nan  698  mpnanrd  699  pm3.24  700  imanst  895  ianordc  906  pm5.17dc  911  dn1dc  968  xorbin  1428  xordc1  1437  alinexa  1651  dfrex2dc  2523  ralinexa  2559  rabeq0  3524  disj  3543  minel  3556  disjsn  3731  sotricim  4420  poirr2  5129  funun  5371  imadiflem  5409  imadif  5410  brprcneu  5632  2omotaplemap  7476  prltlu  7707  caucvgprlemnbj  7887  caucvgprprlemnbj  7913  suplocexprlemmu  7938  xrltnsym2  10029  fzp1nel  10339  fsumsplit  11973  sumsplitdc  11998  phiprmpw  12799  odzdvds  12823  pcdvdsb  12898  lgsne0  15773  lgsquadlem3  15814  bj-nnor  16356