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  1670  nic-axALT  1672  rexanali  3101  difdif  4146  dfss4  4276  difin  4279  ssdif0  4373  difin0ss  4380  inssdif0  4381  dfif2  4534  dffv2  7008  tfinds  7885  sdom0  9153  domtriord  9168  sdom1  9282  inf3lem3  9674  nominpos  12507  isprm3  16723  vdwlem13  17033  vdwnn  17038  psgnunilem4  19536  efgredlem  19786  efgred  19787  ufinffr  23959  ptcmplem5  24086  nmoleub2lem2  25171  ellogdm  26704  pntpbnd  27655  cvbr2  32325  cvnbtwn2  32329  cvnbtwn3  32330  cvnbtwn4  32331  chpssati  32405  chrelat2i  32407  chrelat3  32413  bnj1476  34853  bnj110  34864  bnj1388  35039  dff15  35090  df3nandALT1  36394  imnand2  36397  bj-andnotim  36583  lindsenlbs  37614  poimirlem11  37630  poimirlem12  37631  fdc  37744  lpssat  39007  lssat  39010  lcvbr2  39016  lcvbr3  39017  lcvnbtwn2  39021  lcvnbtwn3  39022  cvrval2  39268  cvrnbtwn2  39269  cvrnbtwn3  39270  cvrnbtwn4  39273  atlrelat1  39315  hlrelat2  39398  dihglblem6  41335  hashnexinj  42122  naddgeoa  43398  faosnf0.11b  43431  dfsucon  43527  or3or  44027  uneqsn  44029  plvcofphax  46908  ichim  47393