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  1671  nic-axALT  1673  rexanali  3090  difdif  4117  dfss4  4251  difin  4254  ssdif0  4348  difin0ss  4355  inssdif0  4356  dfif2  4509  dffv2  6985  tfinds  7864  sdom0  9131  domtriord  9146  sdom1  9261  inf3lem3  9653  nominpos  12487  isprm3  16703  vdwlem13  17014  vdwnn  17019  psgnunilem4  19488  efgredlem  19738  efgred  19739  ufinffr  23902  ptcmplem5  24029  nmoleub2lem2  25104  ellogdm  26636  pntpbnd  27587  cvbr2  32249  cvnbtwn2  32253  cvnbtwn3  32254  cvnbtwn4  32255  chpssati  32329  chrelat2i  32331  chrelat3  32337  bnj1476  34802  bnj110  34813  bnj1388  34988  dff15  35039  df3nandALT1  36341  imnand2  36344  bj-andnotim  36530  lindsenlbs  37563  poimirlem11  37579  poimirlem12  37580  fdc  37693  lpssat  38955  lssat  38958  lcvbr2  38964  lcvbr3  38965  lcvnbtwn2  38969  lcvnbtwn3  38970  cvrval2  39216  cvrnbtwn2  39217  cvrnbtwn3  39218  cvrnbtwn4  39221  atlrelat1  39263  hlrelat2  39346  dihglblem6  41283  hashnexinj  42070  naddgeoa  43352  faosnf0.11b  43385  dfsucon  43481  or3or  43981  uneqsn  43983  plvcofphax  46905  ichim  47390