Theorem iman 439

Description: Express implication in terms of conjunction. 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 304	. . 3 ⊢ (𝜓 ↔ ¬ ¬ 𝜓)
2	1	imbi2i 325	. 2 ⊢ ((𝜑 → 𝜓) ↔ (𝜑 → ¬ ¬ 𝜓))
3		imnan 437	. 2 ⊢ ((𝜑 → ¬ ¬ 𝜓) ↔ ¬ (𝜑 ∧ ¬ 𝜓))
4	2, 3	bitri 264	1 ⊢ ((𝜑 → 𝜓) ↔ ¬ (𝜑 ∧ ¬ 𝜓))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 196   ∧ wa 383

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 197  df-an 385

This theorem is referenced by:  annim  440  pm3.24  944  xor  953  nic-mpALT  1637  nic-axALT  1639  rexanali  3027  difdif  3769  dfss4  3891  difin  3894  ssdif0  3975  difin0ss  3979  inssdif0  3980  npss0OLD  4048  dfif2  4121  notzfaus  4870  dffv2  6310  tfinds  7101  domtriord  8147  inf3lem3  8565  nominpos  11307  isprm3  15443  vdwlem13  15744  vdwnn  15749  psgnunilem4  17963  efgredlem  18206  efgred  18207  ufinffr  21780  ptcmplem5  21907  nmoleub2lem2  22962  ellogdm  24430  pntpbnd  25322  cvbr2  29270  cvnbtwn2  29274  cvnbtwn3  29275  cvnbtwn4  29276  chpssati  29350  chrelat2i  29352  chrelat3  29358  bnj1476  31043  bnj110  31054  bnj1388  31227  df3nandALT1  32521  imnand2  32524  bj-andnotim  32698  lindsenlbs  33534  poimirlem11  33550  poimirlem12  33551  fdc  33671  lpssat  34618  lssat  34621  lcvbr2  34627  lcvbr3  34628  lcvnbtwn2  34632  lcvnbtwn3  34633  cvrval2  34879  cvrnbtwn2  34880  cvrnbtwn3  34881  cvrnbtwn4  34884  atlrelat1  34926  hlrelat2  35007  dihglblem6  36946  or3or  38636  uneqsn  38638  plvcofphax  41435