Theorem iman 402

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 205   ∧ wa 396

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 397

This theorem is referenced by:  pm3.24  403  annim  404  xor  1013  nic-mpALT  1674  nic-axALT  1676  rexanali  3102  difdif  4129  dfss4  4257  difin  4260  ssdif0  4362  difin0ss  4367  inssdif0  4368  dfif2  4529  dffv2  6983  tfinds  7845  sdom0  9104  domtriord  9119  sdom1  9238  inf3lem3  9621  nominpos  12445  isprm3  16616  vdwlem13  16922  vdwnn  16927  psgnunilem4  19359  efgredlem  19609  efgred  19610  ufinffr  23424  ptcmplem5  23551  nmoleub2lem2  24623  ellogdm  26138  pntpbnd  27080  cvbr2  31523  cvnbtwn2  31527  cvnbtwn3  31528  cvnbtwn4  31529  chpssati  31603  chrelat2i  31605  chrelat3  31611  bnj1476  33846  bnj110  33857  bnj1388  34032  dff15  34075  df3nandALT1  35272  imnand2  35275  bj-andnotim  35454  lindsenlbs  36471  poimirlem11  36487  poimirlem12  36488  fdc  36601  lpssat  37871  lssat  37874  lcvbr2  37880  lcvbr3  37881  lcvnbtwn2  37885  lcvnbtwn3  37886  cvrval2  38132  cvrnbtwn2  38133  cvrnbtwn3  38134  cvrnbtwn4  38137  atlrelat1  38179  hlrelat2  38262  dihglblem6  40199  naddgeoa  42130  faosnf0.11b  42163  dfsucon  42259  or3or  42759  uneqsn  42761  plvcofphax  45643  ichim  46111