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  4098  dfss4  4232  difin  4235  ssdif0  4329  difin0ss  4336  inssdif0  4337  dfif2  4490  dffv2  6956  tfinds  7836  sdom0  9073  domtriord  9087  sdom1  9189  inf3lem3  9583  nominpos  12419  isprm3  16653  vdwlem13  16964  vdwnn  16969  psgnunilem4  19427  efgredlem  19677  efgred  19678  ufinffr  23816  ptcmplem5  23943  nmoleub2lem2  25016  ellogdm  26548  pntpbnd  27499  cvbr2  32212  cvnbtwn2  32216  cvnbtwn3  32217  cvnbtwn4  32218  chpssati  32292  chrelat2i  32294  chrelat3  32300  bnj1476  34837  bnj110  34848  bnj1388  35023  dff15  35074  df3nandALT1  36387  imnand2  36390  bj-andnotim  36576  lindsenlbs  37609  poimirlem11  37625  poimirlem12  37626  fdc  37739  lpssat  39006  lssat  39009  lcvbr2  39015  lcvbr3  39016  lcvnbtwn2  39020  lcvnbtwn3  39021  cvrval2  39267  cvrnbtwn2  39268  cvrnbtwn3  39269  cvrnbtwn4  39272  atlrelat1  39314  hlrelat2  39397  dihglblem6  41334  hashnexinj  42116  naddgeoa  43383  faosnf0.11b  43416  dfsucon  43512  or3or  44012  uneqsn  44014  plvcofphax  46948  ichim  47458