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  1016  nic-mpALT  1672  nic-axALT  1674  rexanali  3086  difdif  4106  dfss4  4240  difin  4243  ssdif0  4337  difin0ss  4344  inssdif0  4345  dfif2  4498  dffv2  6963  tfinds  7844  sdom0  9085  domtriord  9100  sdom1  9207  inf3lem3  9601  nominpos  12435  isprm3  16659  vdwlem13  16970  vdwnn  16975  psgnunilem4  19433  efgredlem  19683  efgred  19684  ufinffr  23822  ptcmplem5  23949  nmoleub2lem2  25022  ellogdm  26555  pntpbnd  27506  cvbr2  32219  cvnbtwn2  32223  cvnbtwn3  32224  cvnbtwn4  32225  chpssati  32299  chrelat2i  32301  chrelat3  32307  bnj1476  34845  bnj110  34856  bnj1388  35031  dff15  35082  df3nandALT1  36384  imnand2  36387  bj-andnotim  36573  lindsenlbs  37606  poimirlem11  37622  poimirlem12  37623  fdc  37736  lpssat  38998  lssat  39001  lcvbr2  39007  lcvbr3  39008  lcvnbtwn2  39012  lcvnbtwn3  39013  cvrval2  39259  cvrnbtwn2  39260  cvrnbtwn3  39261  cvrnbtwn4  39264  atlrelat1  39306  hlrelat2  39389  dihglblem6  41326  hashnexinj  42108  naddgeoa  43355  faosnf0.11b  43388  dfsucon  43484  or3or  43984  uneqsn  43986  plvcofphax  46918  ichim  47413