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  1673  nic-axALT  1675  rexanali  3087  difdif  4084  dfss4  4218  difin  4221  ssdif0  4315  difin0ss  4322  inssdif0  4323  dfif2  4478  dffv2  6926  tfinds  7799  sdom0  9033  domtriord  9047  sdom1  9145  inf3lem3  9531  nominpos  12369  isprm3  16601  vdwlem13  16912  vdwnn  16917  psgnunilem4  19417  efgredlem  19667  efgred  19668  ufinffr  23864  ptcmplem5  23991  nmoleub2lem2  25063  ellogdm  26595  pntpbnd  27546  cvbr2  32284  cvnbtwn2  32288  cvnbtwn3  32289  cvnbtwn4  32290  chpssati  32364  chrelat2i  32366  chrelat3  32372  bnj1476  34931  bnj110  34942  bnj1388  35117  dff15  35168  df3nandALT1  36515  imnand2  36518  bj-andnotim  36704  lindsenlbs  37728  poimirlem11  37744  poimirlem12  37745  fdc  37858  lpssat  39185  lssat  39188  lcvbr2  39194  lcvbr3  39195  lcvnbtwn2  39199  lcvnbtwn3  39200  cvrval2  39446  cvrnbtwn2  39447  cvrnbtwn3  39448  cvrnbtwn4  39451  atlrelat1  39493  hlrelat2  39575  dihglblem6  41512  hashnexinj  42294  naddgeoa  43551  faosnf0.11b  43584  dfsucon  43680  or3or  44180  uneqsn  44182  plvcofphax  47109  ichim  47619