Theorem iman 405

Description: Implication in terms of conjunction and negation. Theorem 3.4(27) of [Stoll] p. 176. (Contributed by NM, 12-Mar-1993.) (Proof shortened by Wolf Lammen, 30-Oct-2012.)

Assertion

Ref	Expression
iman	⊢ ((𝜑 → 𝜓) ↔ ¬ (𝜑 ∧ ¬ 𝜓))

Proof of Theorem iman

Step	Hyp	Ref	Expression
1		notnotb 318	. . 3 ⊢ (𝜓 ↔ ¬ ¬ 𝜓)
2	1	imbi2i 339	. 2 ⊢ ((𝜑 → 𝜓) ↔ (𝜑 → ¬ ¬ 𝜓))
3		imnan 403	. 2 ⊢ ((𝜑 → ¬ ¬ 𝜓) ↔ ¬ (𝜑 ∧ ¬ 𝜓))
4	2, 3	bitri 278	1 ⊢ ((𝜑 → 𝜓) ↔ ¬ (𝜑 ∧ ¬ 𝜓))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 399

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 210  df-an 400

This theorem is referenced by:  pm3.24  406  annim  407  xor  1012  nic-mpALT  1674  nic-axALT  1676  rexanali  3224  difdif  4058  dfss4  4185  difin  4188  ssdif0  4277  difin0ss  4282  inssdif0  4283  dfif2  4427  notzfausOLD  5228  dffv2  6733  tfinds  7554  domtriord  8647  inf3lem3  9077  nominpos  11862  isprm3  16017  vdwlem13  16319  vdwnn  16324  psgnunilem4  18617  efgredlem  18865  efgred  18866  ufinffr  22534  ptcmplem5  22661  nmoleub2lem2  23721  ellogdm  25230  pntpbnd  26172  cvbr2  30066  cvnbtwn2  30070  cvnbtwn3  30071  cvnbtwn4  30072  chpssati  30146  chrelat2i  30148  chrelat3  30154  bnj1476  32229  bnj110  32240  bnj1388  32415  dff15  32463  df3nandALT1  33860  imnand2  33863  bj-andnotim  34035  lindsenlbs  35052  poimirlem11  35068  poimirlem12  35069  fdc  35183  lpssat  36309  lssat  36312  lcvbr2  36318  lcvbr3  36319  lcvnbtwn2  36323  lcvnbtwn3  36324  cvrval2  36570  cvrnbtwn2  36571  cvrnbtwn3  36572  cvrnbtwn4  36575  atlrelat1  36617  hlrelat2  36699  dihglblem6  38636  dfsucon  40231  or3or  40724  uneqsn  40726  plvcofphax  43540  ichim  43974