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  1673  nic-axALT  1675  rexanali  3090  difdif  4087  dfss4  4221  difin  4224  ssdif0  4318  difin0ss  4325  inssdif0  4326  dfif2  4481  dffv2  6929  tfinds  7802  sdom0  9037  domtriord  9051  sdom1  9150  inf3lem3  9539  nominpos  12378  isprm3  16610  vdwlem13  16921  vdwnn  16926  psgnunilem4  19426  efgredlem  19676  efgred  19677  ufinffr  23873  ptcmplem5  24000  nmoleub2lem2  25072  ellogdm  26604  pntpbnd  27555  cvbr2  32358  cvnbtwn2  32362  cvnbtwn3  32363  cvnbtwn4  32364  chpssati  32438  chrelat2i  32440  chrelat3  32446  bnj1476  35003  bnj110  35014  bnj1388  35189  dff15  35240  df3nandALT1  36593  imnand2  36596  bj-andnotim  36788  lindsenlbs  37816  poimirlem11  37832  poimirlem12  37833  fdc  37946  lpssat  39273  lssat  39276  lcvbr2  39282  lcvbr3  39283  lcvnbtwn2  39287  lcvnbtwn3  39288  cvrval2  39534  cvrnbtwn2  39535  cvrnbtwn3  39536  cvrnbtwn4  39539  atlrelat1  39581  hlrelat2  39663  dihglblem6  41600  hashnexinj  42382  naddgeoa  43636  faosnf0.11b  43668  dfsucon  43764  or3or  44264  uneqsn  44266  plvcofphax  47193  ichim  47703