Theorem iman 407

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 318	. . 3 ⊢ (𝜓 ↔ ¬ ¬ 𝜓)
2	1	imbi2i 339	. 2 ⊢ ((𝜑 → 𝜓) ↔ (𝜑 → ¬ ¬ 𝜓))
3		imnan 405	. 2 ⊢ ((𝜑 → ¬ ¬ 𝜓) ↔ ¬ (𝜑 ∧ ¬ 𝜓))
4	2, 3	bitri 278	1 ⊢ ((𝜑 → 𝜓) ↔ ¬ (𝜑 ∧ ¬ 𝜓))

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  pm3.24  408  annim  409  xor  1032  nic-mpALT  1705  nic-axALT  1707  rexanali  3117  difdif  4082  dfss4  4215  difin  4218  ssdif0  4314  difin0ss  4321  inssdif0OLD  4323  dfif2  4484  dffv2  6978  dff15  7274  tfinds  7869  sdom0  9121  domtriord  9135  sdom1  9234  inf3lem3  9624  nominpos  12576  isprm3  16851  vdwlem13  17164  vdwnn  17169  psgnunilem4  19704  efgredlem  19954  efgred  19955  lindsenlbs  22150  ufinffr  24241  ptcmplem5  24368  nmoleub2lem2  25430  ellogdm  26960  pntpbnd  27908  cvbr2  32878  cvnbtwn2  32882  cvnbtwn3  32883  cvnbtwn4  32884  chpssati  32958  chrelat2i  32960  chrelat3  32966  bnj1476  35470  bnj110  35481  bnj1388  35656  df3nandALT1  37167  imnand2  37170  bj-andnotim  37438  poimirlem11  38529  poimirlem12  38530  fdc  38659  lpssat  40050  lssat  40053  lcvbr2  40059  lcvbr3  40060  lcvnbtwn2  40064  lcvnbtwn3  40065  cvrval2  40311  cvrnbtwn2  40312  cvrnbtwn3  40313  cvrnbtwn4  40316  atlrelat1  40358  hlrelat2  40440  dihglblem6  42377  hashnexinj  43158  naddgeoa  44380  faosnf0.11b  44412  dfsucon  44508  or3or  45008  uneqsn  45010  plvcofphax  47986  ichim  48508