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  4115  dfss4  4249  difin  4252  ssdif0  4346  difin0ss  4353  inssdif0  4354  dfif2  4507  dffv2  6984  tfinds  7863  sdom0  9130  domtriord  9145  sdom1  9260  inf3lem3  9652  nominpos  12486  isprm3  16702  vdwlem13  17013  vdwnn  17018  psgnunilem4  19483  efgredlem  19733  efgred  19734  ufinffr  23883  ptcmplem5  24010  nmoleub2lem2  25085  ellogdm  26617  pntpbnd  27568  cvbr2  32230  cvnbtwn2  32234  cvnbtwn3  32235  cvnbtwn4  32236  chpssati  32310  chrelat2i  32312  chrelat3  32318  bnj1476  34820  bnj110  34831  bnj1388  35006  dff15  35057  df3nandALT1  36359  imnand2  36362  bj-andnotim  36548  lindsenlbs  37581  poimirlem11  37597  poimirlem12  37598  fdc  37711  lpssat  38973  lssat  38976  lcvbr2  38982  lcvbr3  38983  lcvnbtwn2  38987  lcvnbtwn3  38988  cvrval2  39234  cvrnbtwn2  39235  cvrnbtwn3  39236  cvrnbtwn4  39239  atlrelat1  39281  hlrelat2  39364  dihglblem6  41301  hashnexinj  42088  naddgeoa  43369  faosnf0.11b  43402  dfsucon  43498  or3or  43998  uneqsn  44000  plvcofphax  46917  ichim  47402