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  1673  nic-axALT  1675  rexanali  3086  difdif  4080  dfss4  4214  difin  4217  ssdif0  4311  difin0ss  4318  inssdif0  4319  dfif2  4472  dffv2  6912  tfinds  7785  sdom0  9017  domtriord  9031  sdom1  9129  inf3lem3  9515  nominpos  12353  isprm3  16589  vdwlem13  16900  vdwnn  16905  psgnunilem4  19404  efgredlem  19654  efgred  19655  ufinffr  23839  ptcmplem5  23966  nmoleub2lem2  25038  ellogdm  26570  pntpbnd  27521  cvbr2  32255  cvnbtwn2  32259  cvnbtwn3  32260  cvnbtwn4  32261  chpssati  32335  chrelat2i  32337  chrelat3  32343  bnj1476  34851  bnj110  34862  bnj1388  35037  dff15  35088  df3nandALT1  36433  imnand2  36436  bj-andnotim  36622  lindsenlbs  37655  poimirlem11  37671  poimirlem12  37672  fdc  37785  lpssat  39052  lssat  39055  lcvbr2  39061  lcvbr3  39062  lcvnbtwn2  39066  lcvnbtwn3  39067  cvrval2  39313  cvrnbtwn2  39314  cvrnbtwn3  39315  cvrnbtwn4  39318  atlrelat1  39360  hlrelat2  39442  dihglblem6  41379  hashnexinj  42161  naddgeoa  43427  faosnf0.11b  43460  dfsucon  43556  or3or  44056  uneqsn  44058  plvcofphax  46978  ichim  47488