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  3092  difdif  4076  dfss4  4210  difin  4213  ssdif0  4307  difin0ss  4314  inssdif0  4315  dfif2  4469  dffv2  6927  tfinds  7802  sdom0  9038  domtriord  9052  sdom1  9151  inf3lem3  9540  nominpos  12379  isprm3  16611  vdwlem13  16922  vdwnn  16927  psgnunilem4  19430  efgredlem  19680  efgred  19681  ufinffr  23872  ptcmplem5  23999  nmoleub2lem2  25061  ellogdm  26588  pntpbnd  27539  cvbr2  32343  cvnbtwn2  32347  cvnbtwn3  32348  cvnbtwn4  32349  chpssati  32423  chrelat2i  32425  chrelat3  32431  bnj1476  34995  bnj110  35006  bnj1388  35181  dff15  35233  df3nandALT1  36587  imnand2  36590  bj-andnotim  36851  lindsenlbs  37927  poimirlem11  37943  poimirlem12  37944  fdc  38057  lpssat  39450  lssat  39453  lcvbr2  39459  lcvbr3  39460  lcvnbtwn2  39464  lcvnbtwn3  39465  cvrval2  39711  cvrnbtwn2  39712  cvrnbtwn3  39713  cvrnbtwn4  39716  atlrelat1  39758  hlrelat2  39840  dihglblem6  41777  hashnexinj  42559  naddgeoa  43825  faosnf0.11b  43857  dfsucon  43953  or3or  44453  uneqsn  44455  plvcofphax  47381  ichim  47891