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  3121  difdif  4089  dfss4  4222  difin  4225  ssdif0  4321  difin0ss  4328  inssdif0OLD  4330  dfif2  4491  dffv2  6980  dff15  7272  tfinds  7858  sdom0  9100  domtriord  9114  sdom1  9213  inf3lem3  9602  nominpos  12492  isprm3  16758  vdwlem13  17070  vdwnn  17075  psgnunilem4  19590  efgredlem  19840  efgred  19841  ufinffr  24115  ptcmplem5  24242  nmoleub2lem2  25304  ellogdm  26833  pntpbnd  27781  cvbr2  32664  cvnbtwn2  32668  cvnbtwn3  32669  cvnbtwn4  32670  chpssati  32744  chrelat2i  32746  chrelat3  32752  bnj1476  35259  bnj110  35270  bnj1388  35445  df3nandALT1  36943  imnand2  36946  bj-andnotim  37214  lindsenlbs  38299  poimirlem11  38315  poimirlem12  38316  fdc  38429  lpssat  39820  lssat  39823  lcvbr2  39829  lcvbr3  39830  lcvnbtwn2  39834  lcvnbtwn3  39835  cvrval2  40081  cvrnbtwn2  40082  cvrnbtwn3  40083  cvrnbtwn4  40086  atlrelat1  40128  hlrelat2  40210  dihglblem6  42147  hashnexinj  42928  naddgeoa  44154  faosnf0.11b  44186  dfsucon  44282  or3or  44782  uneqsn  44784  plvcofphax  47717  ichim  48239