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  1017  nic-mpALT  1674  nic-axALT  1676  rexanali  3092  difdif  4089  dfss4  4223  difin  4226  ssdif0  4320  difin0ss  4327  inssdif0  4328  dfif2  4483  dffv2  6937  tfinds  7812  sdom0  9049  domtriord  9063  sdom1  9162  inf3lem3  9551  nominpos  12390  isprm3  16622  vdwlem13  16933  vdwnn  16938  psgnunilem4  19438  efgredlem  19688  efgred  19689  ufinffr  23885  ptcmplem5  24012  nmoleub2lem2  25084  ellogdm  26616  pntpbnd  27567  cvbr2  32370  cvnbtwn2  32374  cvnbtwn3  32375  cvnbtwn4  32376  chpssati  32450  chrelat2i  32452  chrelat3  32458  bnj1476  35022  bnj110  35033  bnj1388  35208  dff15  35259  df3nandALT1  36612  imnand2  36615  bj-andnotim  36810  lindsenlbs  37863  poimirlem11  37879  poimirlem12  37880  fdc  37993  lpssat  39386  lssat  39389  lcvbr2  39395  lcvbr3  39396  lcvnbtwn2  39400  lcvnbtwn3  39401  cvrval2  39647  cvrnbtwn2  39648  cvrnbtwn3  39649  cvrnbtwn4  39652  atlrelat1  39694  hlrelat2  39776  dihglblem6  41713  hashnexinj  42495  naddgeoa  43748  faosnf0.11b  43780  dfsucon  43876  or3or  44376  uneqsn  44378  plvcofphax  47304  ichim  47814