Theorem imnan 685

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 632	. . . 4 ⊢ (𝜑 → (𝜓 → ¬ (𝜑 → ¬ 𝜓)))
2	1	imp 123	. . 3 ⊢ ((𝜑 ∧ 𝜓) → ¬ (𝜑 → ¬ 𝜓))
3	2	con2i 622	. 2 ⊢ ((𝜑 → ¬ 𝜓) → ¬ (𝜑 ∧ 𝜓))
4		pm3.2 138	. . 3 ⊢ (𝜑 → (𝜓 → (𝜑 ∧ 𝜓)))
5	4	con3rr3 628	. 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 609  ax-in2 610

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  imnani  686  nan  687  pm3.24  688  imanst  883  ianordc  894  pm5.17dc  899  dn1dc  955  xorbin  1379  xordc1  1388  alinexa  1596  dfrex2dc  2461  ralinexa  2497  rabeq0  3444  disj  3463  minel  3476  disjsn  3645  sotricim  4308  poirr2  5003  funun  5242  imadiflem  5277  imadif  5278  brprcneu  5489  prltlu  7449  caucvgprlemnbj  7629  caucvgprprlemnbj  7655  suplocexprlemmu  7680  xrltnsym2  9751  fzp1nel  10060  fsumsplit  11370  sumsplitdc  11395  phiprmpw  12176  odzdvds  12199  pcdvdsb  12273  lgsne0  13733  bj-nnor  13769