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  1017  nic-mpALT  1674  nic-axALT  1676  rexanali  3091  difdif  4075  dfss4  4209  difin  4212  ssdif0  4306  difin0ss  4313  inssdif0  4314  dfif2  4468  dffv2  6935  tfinds  7811  sdom0  9047  domtriord  9061  sdom1  9160  inf3lem3  9551  nominpos  12414  isprm3  16652  vdwlem13  16964  vdwnn  16969  psgnunilem4  19472  efgredlem  19722  efgred  19723  ufinffr  23894  ptcmplem5  24021  nmoleub2lem2  25083  ellogdm  26603  pntpbnd  27551  cvbr2  32354  cvnbtwn2  32358  cvnbtwn3  32359  cvnbtwn4  32360  chpssati  32434  chrelat2i  32436  chrelat3  32442  bnj1476  34989  bnj110  35000  bnj1388  35175  dff15  35227  df3nandALT1  36581  imnand2  36584  bj-andnotim  36853  lindsenlbs  37936  poimirlem11  37952  poimirlem12  37953  fdc  38066  lpssat  39459  lssat  39462  lcvbr2  39468  lcvbr3  39469  lcvnbtwn2  39473  lcvnbtwn3  39474  cvrval2  39720  cvrnbtwn2  39721  cvrnbtwn3  39722  cvrnbtwn4  39725  atlrelat1  39767  hlrelat2  39849  dihglblem6  41786  hashnexinj  42567  naddgeoa  43822  faosnf0.11b  43854  dfsucon  43950  or3or  44450  uneqsn  44452  plvcofphax  47395  ichim  47917