Theorem imnan 691

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  692  nan  693  pm3.24  694  imanst  889  ianordc  900  pm5.17dc  905  dn1dc  961  xorbin  1394  xordc1  1403  alinexa  1613  dfrex2dc  2478  ralinexa  2514  rabeq0  3464  disj  3483  minel  3496  disjsn  3666  sotricim  4335  poirr2  5033  funun  5272  imadiflem  5307  imadif  5308  brprcneu  5520  2omotaplemap  7270  prltlu  7500  caucvgprlemnbj  7680  caucvgprprlemnbj  7706  suplocexprlemmu  7731  xrltnsym2  9808  fzp1nel  10118  fsumsplit  11429  sumsplitdc  11454  phiprmpw  12236  odzdvds  12259  pcdvdsb  12333  lgsne0  14735  bj-nnor  14782