Theorem iman 407

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

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  pm3.24  408  annim  409  xor  1032  nic-mpALT  1705  nic-axALT  1707  rexanali  3120  difdif  4074  dfss4  4217  difin  4220  ssdif0  4317  difin0ss  4324  inssdif0OLD  4326  dfif2  4487  dffv2  7011  dff15  7307  tfinds  7905  sdom0  9166  domtriord  9180  sdom1  9279  inf3lem3  9668  nominpos  12623  isprm3  16902  vdwlem13  17215  vdwnn  17220  psgnunilem4  19762  efgredlem  20012  efgred  20013  lindsenlbs  22212  ufinffr  24303  ptcmplem5  24430  nmoleub2lem2  25492  ellogdm  27024  pntpbnd  27972  cvbr2  32942  cvnbtwn2  32946  cvnbtwn3  32947  cvnbtwn4  32948  chpssati  33022  chrelat2i  33024  chrelat3  33030  bnj1476  35588  bnj110  35599  bnj1388  35774  df3nandALT1  37402  imnand2  37405  bj-andnotim  37673  poimirlem11  38817  poimirlem12  38818  fdc  38945  lpssat  40336  lssat  40339  lcvbr2  40345  lcvbr3  40346  lcvnbtwn2  40350  lcvnbtwn3  40351  cvrval2  40597  cvrnbtwn2  40598  cvrnbtwn3  40599  cvrnbtwn4  40602  atlrelat1  40644  hlrelat2  40726  dihglblem6  42663  hashnexinj  43444  naddgeoa  44657  faosnf0.11b  44689  dfsucon  44785  or3or  45284  uneqsn  45286  plvcofphax  48290  ichim  48812