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  1403  xordc1  1412  alinexa  1625  dfrex2dc  2496  ralinexa  2532  rabeq0  3489  disj  3508  minel  3521  disjsn  3694  sotricim  4369  poirr2  5074  funun  5314  imadiflem  5352  imadif  5353  brprcneu  5568  2omotaplemap  7368  prltlu  7599  caucvgprlemnbj  7779  caucvgprprlemnbj  7805  suplocexprlemmu  7830  xrltnsym2  9915  fzp1nel  10225  fsumsplit  11689  sumsplitdc  11714  phiprmpw  12515  odzdvds  12539  pcdvdsb  12614  lgsne0  15486  lgsquadlem3  15527  bj-nnor  15632