Theorem iman 402

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 205   ∧ wa 396

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 206  df-an 397

This theorem is referenced by:  pm3.24  403  annim  404  xor  1012  nic-mpALT  1675  nic-axALT  1677  rexanali  3192  difdif  4065  dfss4  4192  difin  4195  ssdif0  4297  difin0ss  4302  inssdif0  4303  dfif2  4461  dffv2  6863  tfinds  7706  sdom0  8895  domtriord  8910  inf3lem3  9388  nominpos  12210  isprm3  16388  vdwlem13  16694  vdwnn  16699  psgnunilem4  19105  efgredlem  19353  efgred  19354  ufinffr  23080  ptcmplem5  23207  nmoleub2lem2  24279  ellogdm  25794  pntpbnd  26736  cvbr2  30645  cvnbtwn2  30649  cvnbtwn3  30650  cvnbtwn4  30651  chpssati  30725  chrelat2i  30727  chrelat3  30733  bnj1476  32827  bnj110  32838  bnj1388  33013  dff15  33056  df3nandALT1  34588  imnand2  34591  bj-andnotim  34770  lindsenlbs  35772  poimirlem11  35788  poimirlem12  35789  fdc  35903  lpssat  37027  lssat  37030  lcvbr2  37036  lcvbr3  37037  lcvnbtwn2  37041  lcvnbtwn3  37042  cvrval2  37288  cvrnbtwn2  37289  cvrnbtwn3  37290  cvrnbtwn4  37293  atlrelat1  37335  hlrelat2  37417  dihglblem6  39354  dfsucon  41130  or3or  41631  uneqsn  41633  plvcofphax  44442  ichim  44909