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  3083  difdif  4088  dfss4  4222  difin  4225  ssdif0  4319  difin0ss  4326  inssdif0  4327  dfif2  4480  dffv2  6922  tfinds  7800  sdom0  9033  domtriord  9047  sdom1  9149  inf3lem3  9545  nominpos  12379  isprm3  16612  vdwlem13  16923  vdwnn  16928  psgnunilem4  19394  efgredlem  19644  efgred  19645  ufinffr  23832  ptcmplem5  23959  nmoleub2lem2  25032  ellogdm  26564  pntpbnd  27515  cvbr2  32245  cvnbtwn2  32249  cvnbtwn3  32250  cvnbtwn4  32251  chpssati  32325  chrelat2i  32327  chrelat3  32333  bnj1476  34816  bnj110  34827  bnj1388  35002  dff15  35053  df3nandALT1  36375  imnand2  36378  bj-andnotim  36564  lindsenlbs  37597  poimirlem11  37613  poimirlem12  37614  fdc  37727  lpssat  38994  lssat  38997  lcvbr2  39003  lcvbr3  39004  lcvnbtwn2  39008  lcvnbtwn3  39009  cvrval2  39255  cvrnbtwn2  39256  cvrnbtwn3  39257  cvrnbtwn4  39260  atlrelat1  39302  hlrelat2  39385  dihglblem6  41322  hashnexinj  42104  naddgeoa  43370  faosnf0.11b  43403  dfsucon  43499  or3or  43999  uneqsn  44001  plvcofphax  46935  ichim  47445