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  874  ianordc  885  pm5.17dc  890  dn1dc  945  xorbin  1366  xordc1  1375  alinexa  1583  dfrex2dc  2448  ralinexa  2484  rabeq0  3423  disj  3442  minel  3455  disjsn  3621  sotricim  4282  poirr2  4975  funun  5211  imadiflem  5246  imadif  5247  brprcneu  5458  prltlu  7390  caucvgprlemnbj  7570  caucvgprprlemnbj  7596  suplocexprlemmu  7621  xrltnsym2  9683  fzp1nel  9988  fsumsplit  11286  sumsplitdc  11311  phiprmpw  12074  bj-nnor  13270