Theorem imnan 694

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 640	. . . 4 ⊢ (𝜑 → (𝜓 → ¬ (𝜑 → ¬ 𝜓)))
2	1	imp 124	. . 3 ⊢ ((𝜑 ∧ 𝜓) → ¬ (𝜑 → ¬ 𝜓))
3	2	con2i 630	. 2 ⊢ ((𝜑 → ¬ 𝜓) → ¬ (𝜑 ∧ 𝜓))
4		pm3.2 139	. . 3 ⊢ (𝜑 → (𝜓 → (𝜑 ∧ 𝜓)))
5	4	con3rr3 636	. 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 617  ax-in2 618

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  imnani  695  nan  696  mpnanrd  697  pm3.24  698  imanst  893  ianordc  904  pm5.17dc  909  dn1dc  966  xorbin  1426  xordc1  1435  alinexa  1649  dfrex2dc  2521  ralinexa  2557  rabeq0  3522  disj  3541  minel  3554  disjsn  3729  sotricim  4418  poirr2  5127  funun  5368  imadiflem  5406  imadif  5407  brprcneu  5628  2omotaplemap  7466  prltlu  7697  caucvgprlemnbj  7877  caucvgprprlemnbj  7903  suplocexprlemmu  7928  xrltnsym2  10019  fzp1nel  10329  fsumsplit  11958  sumsplitdc  11983  phiprmpw  12784  odzdvds  12808  pcdvdsb  12883  lgsne0  15757  lgsquadlem3  15798  bj-nnor  16266