Theorem imnan 690

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 637	. . . 4 ⊢ (𝜑 → (𝜓 → ¬ (𝜑 → ¬ 𝜓)))
2	1	imp 124	. . 3 ⊢ ((𝜑 ∧ 𝜓) → ¬ (𝜑 → ¬ 𝜓))
3	2	con2i 627	. 2 ⊢ ((𝜑 → ¬ 𝜓) → ¬ (𝜑 ∧ 𝜓))
4		pm3.2 139	. . 3 ⊢ (𝜑 → (𝜓 → (𝜑 ∧ 𝜓)))
5	4	con3rr3 633	. 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 614  ax-in2 615

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  imnani  691  nan  692  pm3.24  693  imanst  888  ianordc  899  pm5.17dc  904  dn1dc  960  xorbin  1384  xordc1  1393  alinexa  1603  dfrex2dc  2468  ralinexa  2504  rabeq0  3452  disj  3471  minel  3484  disjsn  3654  sotricim  4321  poirr2  5018  funun  5257  imadiflem  5292  imadif  5293  brprcneu  5505  2omotaplemap  7251  prltlu  7481  caucvgprlemnbj  7661  caucvgprprlemnbj  7687  suplocexprlemmu  7712  xrltnsym2  9788  fzp1nel  10097  fsumsplit  11406  sumsplitdc  11431  phiprmpw  12212  odzdvds  12235  pcdvdsb  12309  lgsne0  14221  bj-nnor  14257