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  3118  difdif  4085  dfss4  4218  difin  4221  ssdif0  4317  difin0ss  4324  inssdif0OLD  4326  dfif2  4487  dffv2  6977  dff15  7273  tfinds  7860  sdom0  9111  domtriord  9125  sdom1  9224  inf3lem3  9613  nominpos  12509  isprm3  16779  vdwlem13  17091  vdwnn  17096  psgnunilem4  19630  efgredlem  19880  efgred  19881  lindsenlbs  22070  ufinffr  24161  ptcmplem5  24288  nmoleub2lem2  25350  ellogdm  26884  pntpbnd  27832  cvbr2  32772  cvnbtwn2  32776  cvnbtwn3  32777  cvnbtwn4  32778  chpssati  32852  chrelat2i  32854  chrelat3  32860  bnj1476  35364  bnj110  35375  bnj1388  35550  df3nandALT1  37026  imnand2  37029  bj-andnotim  37297  poimirlem11  38388  poimirlem12  38389  fdc  38503  lpssat  39894  lssat  39897  lcvbr2  39903  lcvbr3  39904  lcvnbtwn2  39908  lcvnbtwn3  39909  cvrval2  40155  cvrnbtwn2  40156  cvrnbtwn3  40157  cvrnbtwn4  40160  atlrelat1  40202  hlrelat2  40284  dihglblem6  42221  hashnexinj  43002  naddgeoa  44243  faosnf0.11b  44275  dfsucon  44371  or3or  44871  uneqsn  44873  plvcofphax  47843  ichim  48365