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  3116  difdif  4082  dfss4  4215  difin  4218  ssdif0  4314  difin0ss  4321  inssdif0OLD  4323  dfif2  4484  dffv2  6973  dff15  7269  tfinds  7856  sdom0  9107  domtriord  9121  sdom1  9220  inf3lem3  9609  nominpos  12505  isprm3  16773  vdwlem13  17085  vdwnn  17090  psgnunilem4  19624  efgredlem  19874  efgred  19875  lindsenlbs  22064  ufinffr  24155  ptcmplem5  24282  nmoleub2lem2  25344  ellogdm  26876  pntpbnd  27824  cvbr2  32764  cvnbtwn2  32768  cvnbtwn3  32769  cvnbtwn4  32770  chpssati  32844  chrelat2i  32846  chrelat3  32852  bnj1476  35356  bnj110  35367  bnj1388  35542  df3nandALT1  37018  imnand2  37021  bj-andnotim  37289  poimirlem11  38380  poimirlem12  38381  fdc  38495  lpssat  39886  lssat  39889  lcvbr2  39895  lcvbr3  39896  lcvnbtwn2  39900  lcvnbtwn3  39901  cvrval2  40147  cvrnbtwn2  40148  cvrnbtwn3  40149  cvrnbtwn4  40152  atlrelat1  40194  hlrelat2  40276  dihglblem6  42213  hashnexinj  42994  naddgeoa  44235  faosnf0.11b  44267  dfsucon  44363  or3or  44863  uneqsn  44865  plvcofphax  47835  ichim  48357