Theorem iman 402

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 316	. . 3 ⊢ (𝜓 ↔ ¬ ¬ 𝜓)
2	1	imbi2i 337	. 2 ⊢ ((𝜑 → 𝜓) ↔ (𝜑 → ¬ ¬ 𝜓))
3		imnan 400	. 2 ⊢ ((𝜑 → ¬ ¬ 𝜓) ↔ ¬ (𝜑 ∧ ¬ 𝜓))
4	2, 3	bitri 276	1 ⊢ ((𝜑 → 𝜓) ↔ ¬ (𝜑 ∧ ¬ 𝜓))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 207   ∧ wa 396

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 208  df-an 397

This theorem is referenced by:  pm3.24  403  annim  404  xor  1022  nic-mpALT  1679  nic-axALT  1681  rexanali  3094  difdif  4072  dfss4  4204  difin  4207  ssdif0  4301  difin0ss  4308  inssdif0  4309  dfif2  4463  dffv2  6929  tfinds  7807  sdom0  9044  domtriord  9058  sdom1  9157  inf3lem3  9549  nominpos  12412  isprm3  16650  vdwlem13  16962  vdwnn  16967  psgnunilem4  19470  efgredlem  19720  efgred  19721  ufinffr  23919  ptcmplem5  24046  nmoleub2lem2  25108  ellogdm  26628  pntpbnd  27576  cvbr2  32379  cvnbtwn2  32383  cvnbtwn3  32384  cvnbtwn4  32385  chpssati  32459  chrelat2i  32461  chrelat3  32467  bnj1476  35036  bnj110  35047  bnj1388  35222  dff15  35272  df3nandALT1  36634  imnand2  36637  bj-andnotim  36906  lindsenlbs  37989  poimirlem11  38005  poimirlem12  38006  fdc  38119  lpssat  39512  lssat  39515  lcvbr2  39521  lcvbr3  39522  lcvnbtwn2  39526  lcvnbtwn3  39527  cvrval2  39773  cvrnbtwn2  39774  cvrnbtwn3  39775  cvrnbtwn4  39778  atlrelat1  39820  hlrelat2  39902  dihglblem6  41839  hashnexinj  42620  naddgeoa  43846  faosnf0.11b  43878  dfsucon  43974  or3or  44474  uneqsn  44476  plvcofphax  47417  ichim  47939