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  962  xorbin  1395  xordc1  1404  alinexa  1614  dfrex2dc  2485  ralinexa  2521  rabeq0  3477  disj  3496  minel  3509  disjsn  3681  sotricim  4355  poirr2  5059  funun  5299  imadiflem  5334  imadif  5335  brprcneu  5548  2omotaplemap  7319  prltlu  7549  caucvgprlemnbj  7729  caucvgprprlemnbj  7755  suplocexprlemmu  7780  xrltnsym2  9863  fzp1nel  10173  fsumsplit  11553  sumsplitdc  11578  phiprmpw  12363  odzdvds  12386  pcdvdsb  12461  lgsne0  15195  lgsquadlem3  15236  bj-nnor  15296