Theorem iman 401

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  pm3.24  402  annim  403  xor  1017  nic-mpALT  1674  nic-axALT  1676  rexanali  3092  difdif  4076  dfss4  4210  difin  4213  ssdif0  4307  difin0ss  4314  inssdif0  4315  dfif2  4469  dffv2  6929  tfinds  7804  sdom0  9040  domtriord  9054  sdom1  9153  inf3lem3  9542  nominpos  12405  isprm3  16643  vdwlem13  16955  vdwnn  16960  psgnunilem4  19463  efgredlem  19713  efgred  19714  ufinffr  23904  ptcmplem5  24031  nmoleub2lem2  25093  ellogdm  26616  pntpbnd  27565  cvbr2  32369  cvnbtwn2  32373  cvnbtwn3  32374  cvnbtwn4  32375  chpssati  32449  chrelat2i  32451  chrelat3  32457  bnj1476  35005  bnj110  35016  bnj1388  35191  dff15  35243  df3nandALT1  36597  imnand2  36600  bj-andnotim  36869  lindsenlbs  37950  poimirlem11  37966  poimirlem12  37967  fdc  38080  lpssat  39473  lssat  39476  lcvbr2  39482  lcvbr3  39483  lcvnbtwn2  39487  lcvnbtwn3  39488  cvrval2  39734  cvrnbtwn2  39735  cvrnbtwn3  39736  cvrnbtwn4  39739  atlrelat1  39781  hlrelat2  39863  dihglblem6  41800  hashnexinj  42581  naddgeoa  43840  faosnf0.11b  43872  dfsucon  43968  or3or  44468  uneqsn  44470  plvcofphax  47407  ichim  47929