Theorem imnan 697

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 642	. . . 4 ⊢ (𝜑 → (𝜓 → ¬ (𝜑 → ¬ 𝜓)))
2	1	imp 124	. . 3 ⊢ ((𝜑 ∧ 𝜓) → ¬ (𝜑 → ¬ 𝜓))
3	2	con2i 632	. 2 ⊢ ((𝜑 → ¬ 𝜓) → ¬ (𝜑 ∧ 𝜓))
4		pm3.2 139	. . 3 ⊢ (𝜑 → (𝜓 → (𝜑 ∧ 𝜓)))
5	4	con3rr3 638	. 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 619  ax-in2 620

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  imnani  698  nan  699  mpnanrd  700  pm3.24  701  imanst  896  ianordc  907  pm5.17dc  912  dn1dc  969  xorbin  1429  xordc1  1438  alinexa  1652  dfrex2dc  2524  ralinexa  2560  rabeq0  3526  disj  3545  minel  3558  disjsn  3735  sotricim  4426  poirr2  5136  funun  5378  imadiflem  5416  imadif  5417  brprcneu  5641  2omotaplemap  7519  prltlu  7750  caucvgprlemnbj  7930  caucvgprprlemnbj  7956  suplocexprlemmu  7981  xrltnsym2  10073  fzp1nel  10384  fsumsplit  12031  sumsplitdc  12056  phiprmpw  12857  odzdvds  12881  pcdvdsb  12956  lgsne0  15840  lgsquadlem3  15881  bj-nnor  16435