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 314	. . 3 ⊢ (𝜓 ↔ ¬ ¬ 𝜓)
2	1	imbi2i 335	. 2 ⊢ ((𝜑 → 𝜓) ↔ (𝜑 → ¬ ¬ 𝜓))
3		imnan 399	. 2 ⊢ ((𝜑 → ¬ ¬ 𝜓) ↔ ¬ (𝜑 ∧ ¬ 𝜓))
4	2, 3	bitri 274	1 ⊢ ((𝜑 → 𝜓) ↔ ¬ (𝜑 ∧ ¬ 𝜓))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 205   ∧ 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 206  df-an 396

This theorem is referenced by:  pm3.24  402  annim  403  xor  1011  nic-mpALT  1676  nic-axALT  1678  rexanali  3191  difdif  4061  dfss4  4189  difin  4192  ssdif0  4294  difin0ss  4299  inssdif0  4300  dfif2  4458  dffv2  6845  tfinds  7681  domtriord  8859  inf3lem3  9318  nominpos  12140  isprm3  16316  vdwlem13  16622  vdwnn  16627  psgnunilem4  19020  efgredlem  19268  efgred  19269  ufinffr  22988  ptcmplem5  23115  nmoleub2lem2  24185  ellogdm  25699  pntpbnd  26641  cvbr2  30546  cvnbtwn2  30550  cvnbtwn3  30551  cvnbtwn4  30552  chpssati  30626  chrelat2i  30628  chrelat3  30634  bnj1476  32727  bnj110  32738  bnj1388  32913  dff15  32956  df3nandALT1  34515  imnand2  34518  bj-andnotim  34697  lindsenlbs  35699  poimirlem11  35715  poimirlem12  35716  fdc  35830  lpssat  36954  lssat  36957  lcvbr2  36963  lcvbr3  36964  lcvnbtwn2  36968  lcvnbtwn3  36969  cvrval2  37215  cvrnbtwn2  37216  cvrnbtwn3  37217  cvrnbtwn4  37220  atlrelat1  37262  hlrelat2  37344  dihglblem6  39281  dfsucon  41028  or3or  41520  uneqsn  41522  plvcofphax  44329  ichim  44797