Theorem iman 401

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 315	. . 3 ⊢ (𝜓 ↔ ¬ ¬ 𝜓)
2	1	imbi2i 336	. 2 ⊢ ((𝜑 → 𝜓) ↔ (𝜑 → ¬ ¬ 𝜓))
3		imnan 399	. 2 ⊢ ((𝜑 → ¬ ¬ 𝜓) ↔ ¬ (𝜑 ∧ ¬ 𝜓))
4	2, 3	bitri 275	1 ⊢ ((𝜑 → 𝜓) ↔ ¬ (𝜑 ∧ ¬ 𝜓))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  pm3.24  402  annim  403  xor  1016  nic-mpALT  1672  nic-axALT  1674  rexanali  3084  difdif  4094  dfss4  4228  difin  4231  ssdif0  4325  difin0ss  4332  inssdif0  4333  dfif2  4486  dffv2  6938  tfinds  7816  sdom0  9050  domtriord  9064  sdom1  9166  inf3lem3  9559  nominpos  12395  isprm3  16629  vdwlem13  16940  vdwnn  16945  psgnunilem4  19403  efgredlem  19653  efgred  19654  ufinffr  23792  ptcmplem5  23919  nmoleub2lem2  24992  ellogdm  26524  pntpbnd  27475  cvbr2  32185  cvnbtwn2  32189  cvnbtwn3  32190  cvnbtwn4  32191  chpssati  32265  chrelat2i  32267  chrelat3  32273  bnj1476  34810  bnj110  34821  bnj1388  34996  dff15  35047  df3nandALT1  36360  imnand2  36363  bj-andnotim  36549  lindsenlbs  37582  poimirlem11  37598  poimirlem12  37599  fdc  37712  lpssat  38979  lssat  38982  lcvbr2  38988  lcvbr3  38989  lcvnbtwn2  38993  lcvnbtwn3  38994  cvrval2  39240  cvrnbtwn2  39241  cvrnbtwn3  39242  cvrnbtwn4  39245  atlrelat1  39287  hlrelat2  39370  dihglblem6  41307  hashnexinj  42089  naddgeoa  43356  faosnf0.11b  43389  dfsucon  43485  or3or  43985  uneqsn  43987  plvcofphax  46921  ichim  47431