Theorem iman 403

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

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

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 398

This theorem is referenced by:  pm3.24  404  annim  405  xor  1014  nic-mpALT  1675  nic-axALT  1677  rexanali  3103  difdif  4131  dfss4  4259  difin  4262  ssdif0  4364  difin0ss  4369  inssdif0  4370  dfif2  4531  dffv2  6987  tfinds  7849  sdom0  9108  domtriord  9123  sdom1  9242  inf3lem3  9625  nominpos  12449  isprm3  16620  vdwlem13  16926  vdwnn  16931  psgnunilem4  19365  efgredlem  19615  efgred  19616  ufinffr  23433  ptcmplem5  23560  nmoleub2lem2  24632  ellogdm  26147  pntpbnd  27091  cvbr2  31536  cvnbtwn2  31540  cvnbtwn3  31541  cvnbtwn4  31542  chpssati  31616  chrelat2i  31618  chrelat3  31624  bnj1476  33858  bnj110  33869  bnj1388  34044  dff15  34087  df3nandALT1  35284  imnand2  35287  bj-andnotim  35466  lindsenlbs  36483  poimirlem11  36499  poimirlem12  36500  fdc  36613  lpssat  37883  lssat  37886  lcvbr2  37892  lcvbr3  37893  lcvnbtwn2  37897  lcvnbtwn3  37898  cvrval2  38144  cvrnbtwn2  38145  cvrnbtwn3  38146  cvrnbtwn4  38149  atlrelat1  38191  hlrelat2  38274  dihglblem6  40211  naddgeoa  42145  faosnf0.11b  42178  dfsucon  42274  or3or  42774  uneqsn  42776  plvcofphax  45657  ichim  46125