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 205   ∧ 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 206  df-an 396

This theorem is referenced by:  pm3.24  402  annim  403  xor  1013  nic-mpALT  1667  nic-axALT  1669  rexanali  3099  difdif  4129  dfss4  4259  difin  4262  ssdif0  4364  difin0ss  4369  inssdif0  4370  dfif2  4531  dffv2  6993  tfinds  7864  sdom0  9133  domtriord  9148  sdom1  9267  inf3lem3  9654  nominpos  12480  isprm3  16654  vdwlem13  16962  vdwnn  16967  psgnunilem4  19452  efgredlem  19702  efgred  19703  ufinffr  23846  ptcmplem5  23973  nmoleub2lem2  25056  ellogdm  26586  pntpbnd  27534  cvbr2  32106  cvnbtwn2  32110  cvnbtwn3  32111  cvnbtwn4  32112  chpssati  32186  chrelat2i  32188  chrelat3  32194  bnj1476  34478  bnj110  34489  bnj1388  34664  dff15  34707  df3nandALT1  35883  imnand2  35886  bj-andnotim  36065  lindsenlbs  37088  poimirlem11  37104  poimirlem12  37105  fdc  37218  lpssat  38485  lssat  38488  lcvbr2  38494  lcvbr3  38495  lcvnbtwn2  38499  lcvnbtwn3  38500  cvrval2  38746  cvrnbtwn2  38747  cvrnbtwn3  38748  cvrnbtwn4  38751  atlrelat1  38793  hlrelat2  38876  dihglblem6  40813  hashnexinj  41599  naddgeoa  42824  faosnf0.11b  42857  dfsucon  42953  or3or  43453  uneqsn  43455  plvcofphax  46329  ichim  46797