Theorem iman 405

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 318	. . 3 ⊢ (𝜓 ↔ ¬ ¬ 𝜓)
2	1	imbi2i 339	. 2 ⊢ ((𝜑 → 𝜓) ↔ (𝜑 → ¬ ¬ 𝜓))
3		imnan 403	. 2 ⊢ ((𝜑 → ¬ ¬ 𝜓) ↔ ¬ (𝜑 ∧ ¬ 𝜓))
4	2, 3	bitri 278	1 ⊢ ((𝜑 → 𝜓) ↔ ¬ (𝜑 ∧ ¬ 𝜓))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 399

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 210  df-an 400

This theorem is referenced by:  pm3.24  406  annim  407  xor  1014  nic-mpALT  1679  nic-axALT  1681  rexanali  3176  difdif  4031  dfss4  4159  difin  4162  ssdif0  4262  difin0ss  4267  inssdif0  4268  dfif2  4426  notzfausOLD  5239  dffv2  6775  tfinds  7605  domtriord  8725  inf3lem3  9178  nominpos  11965  isprm3  16136  vdwlem13  16441  vdwnn  16446  psgnunilem4  18755  efgredlem  19003  efgred  19004  ufinffr  22692  ptcmplem5  22819  nmoleub2lem2  23880  ellogdm  25394  pntpbnd  26336  cvbr2  30230  cvnbtwn2  30234  cvnbtwn3  30235  cvnbtwn4  30236  chpssati  30310  chrelat2i  30312  chrelat3  30318  bnj1476  32410  bnj110  32421  bnj1388  32596  dff15  32639  df3nandALT1  34243  imnand2  34246  bj-andnotim  34425  lindsenlbs  35427  poimirlem11  35443  poimirlem12  35444  fdc  35558  lpssat  36682  lssat  36685  lcvbr2  36691  lcvbr3  36692  lcvnbtwn2  36696  lcvnbtwn3  36697  cvrval2  36943  cvrnbtwn2  36944  cvrnbtwn3  36945  cvrnbtwn4  36948  atlrelat1  36990  hlrelat2  37072  dihglblem6  39009  dfsucon  40724  or3or  41217  uneqsn  41219  plvcofphax  44021  ichim  44490