Theorem imnan 701

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 646	. . . 4 ⊢ (𝜑 → (𝜓 → ¬ (𝜑 → ¬ 𝜓)))
2	1	imp 124	. . 3 ⊢ ((𝜑 ∧ 𝜓) → ¬ (𝜑 → ¬ 𝜓))
3	2	con2i 636	. 2 ⊢ ((𝜑 → ¬ 𝜓) → ¬ (𝜑 ∧ 𝜓))
4		pm3.2 139	. . 3 ⊢ (𝜑 → (𝜓 → (𝜑 ∧ 𝜓)))
5	4	con3rr3 642	. 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 623  ax-in2 624

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  imnani  702  nan  703  mpnanrd  704  pm3.24  705  imanst  900  ianordc  911  pm5.17dc  916  dn1dc  973  xorbin  1433  xordc1  1442  alinexa  1656  dfrex2dc  2541  ralinexa  2577  rabeq0  3552  disj  3572  minel  3585  disjsn  3767  sotricim  4463  poirr2  5175  funun  5417  imadiflem  5455  imadif  5456  brprcneu  5683  2omotaplemap  7613  prltlu  7844  caucvgprlemnbj  8024  caucvgprprlemnbj  8050  suplocexprlemmu  8075  xrltnsym2  10175  fzp1nel  10489  fsumsplit  12152  sumsplitdc  12177  phiprmpw  12978  odzdvds  13002  pcdvdsb  13077  lgsne0  16071  lgsquadlem3  16112  bj-nnor  16676