Theorem iman 406

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 318	. . 3 ⊢ (𝜓 ↔ ¬ ¬ 𝜓)
2	1	imbi2i 339	. 2 ⊢ ((𝜑 → 𝜓) ↔ (𝜑 → ¬ ¬ 𝜓))
3		imnan 404	. 2 ⊢ ((𝜑 → ¬ ¬ 𝜓) ↔ ¬ (𝜑 ∧ ¬ 𝜓))
4	2, 3	bitri 278	1 ⊢ ((𝜑 → 𝜓) ↔ ¬ (𝜑 ∧ ¬ 𝜓))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 400

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 210  df-an 401

This theorem is referenced by:  pm3.24  407  annim  408  xor  1030  nic-mpALT  1699  nic-axALT  1701  rexanali  3125  difdif  4097  dfss4  4230  difin  4233  ssdif0  4328  difin0ss  4335  inssdif0  4336  dfif2  4491  dffv2  6974  tfinds  7852  sdom0  9093  domtriord  9107  sdom1  9206  inf3lem3  9595  nominpos  12477  isprm3  16737  vdwlem13  17049  vdwnn  17054  psgnunilem4  19563  efgredlem  19813  efgred  19814  ufinffr  24051  ptcmplem5  24178  nmoleub2lem2  25240  ellogdm  26766  pntpbnd  27714  cvbr2  32572  cvnbtwn2  32576  cvnbtwn3  32577  cvnbtwn4  32578  chpssati  32652  chrelat2i  32654  chrelat3  32660  bnj1476  35176  bnj110  35187  bnj1388  35362  dff15  35412  df3nandALT1  36795  imnand2  36798  bj-andnotim  37066  lindsenlbs  38149  poimirlem11  38165  poimirlem12  38166  fdc  38279  lpssat  39672  lssat  39675  lcvbr2  39681  lcvbr3  39682  lcvnbtwn2  39686  lcvnbtwn3  39687  cvrval2  39933  cvrnbtwn2  39934  cvrnbtwn3  39935  cvrnbtwn4  39938  atlrelat1  39980  hlrelat2  40062  dihglblem6  41999  hashnexinj  42780  naddgeoa  44006  faosnf0.11b  44038  dfsucon  44134  or3or  44634  uneqsn  44636  plvcofphax  47566  ichim  48088