Theorem imnan 680

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 627	. . . 4 ⊢ (𝜑 → (𝜓 → ¬ (𝜑 → ¬ 𝜓)))
2	1	imp 123	. . 3 ⊢ ((𝜑 ∧ 𝜓) → ¬ (𝜑 → ¬ 𝜓))
3	2	con2i 617	. 2 ⊢ ((𝜑 → ¬ 𝜓) → ¬ (𝜑 ∧ 𝜓))
4		pm3.2 138	. . 3 ⊢ (𝜑 → (𝜓 → (𝜑 ∧ 𝜓)))
5	4	con3rr3 623	. 2 ⊢ (¬ (𝜑 ∧ 𝜓) → (𝜑 → ¬ 𝜓))
6	3, 5	impbii 125	1 ⊢ ((𝜑 → ¬ 𝜓) ↔ ¬ (𝜑 ∧ 𝜓))

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 103   ↔ wb 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 604  ax-in2 605

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  imnani  681  nan  682  pm3.24  683  imanst  878  ianordc  889  pm5.17dc  894  dn1dc  950  xorbin  1374  xordc1  1383  alinexa  1591  dfrex2dc  2456  ralinexa  2492  rabeq0  3437  disj  3456  minel  3469  disjsn  3637  sotricim  4300  poirr2  4995  funun  5231  imadiflem  5266  imadif  5267  brprcneu  5478  prltlu  7424  caucvgprlemnbj  7604  caucvgprprlemnbj  7630  suplocexprlemmu  7655  xrltnsym2  9726  fzp1nel  10035  fsumsplit  11344  sumsplitdc  11369  phiprmpw  12150  odzdvds  12173  pcdvdsb  12247  lgsne0  13539  bj-nnor  13575