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  1015  nic-mpALT  1670  nic-axALT  1672  rexanali  3108  difdif  4158  dfss4  4288  difin  4291  ssdif0  4389  difin0ss  4396  inssdif0  4397  dfif2  4550  dffv2  7017  tfinds  7897  sdom0  9174  domtriord  9189  sdom1  9305  inf3lem3  9699  nominpos  12530  isprm3  16730  vdwlem13  17040  vdwnn  17045  psgnunilem4  19539  efgredlem  19789  efgred  19790  ufinffr  23958  ptcmplem5  24085  nmoleub2lem2  25168  ellogdm  26699  pntpbnd  27650  cvbr2  32315  cvnbtwn2  32319  cvnbtwn3  32320  cvnbtwn4  32321  chpssati  32395  chrelat2i  32397  chrelat3  32403  bnj1476  34823  bnj110  34834  bnj1388  35009  dff15  35060  df3nandALT1  36365  imnand2  36368  bj-andnotim  36554  lindsenlbs  37575  poimirlem11  37591  poimirlem12  37592  fdc  37705  lpssat  38969  lssat  38972  lcvbr2  38978  lcvbr3  38979  lcvnbtwn2  38983  lcvnbtwn3  38984  cvrval2  39230  cvrnbtwn2  39231  cvrnbtwn3  39232  cvrnbtwn4  39235  atlrelat1  39277  hlrelat2  39360  dihglblem6  41297  hashnexinj  42085  naddgeoa  43356  faosnf0.11b  43389  dfsucon  43485  or3or  43985  uneqsn  43987  plvcofphax  46862  ichim  47331