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  1704  nic-axALT  1706  rexanali  3116  difdif  4071  dfss4  4214  difin  4217  ssdif0  4313  difin0ss  4320  inssdif0OLD  4322  dfif2  4483  dffv2  6981  dff15  7277  tfinds  7872  sdom0  9132  domtriord  9146  sdom1  9245  inf3lem3  9635  nominpos  12587  isprm3  16864  vdwlem13  17177  vdwnn  17182  psgnunilem4  19717  efgredlem  19967  efgred  19968  lindsenlbs  22163  ufinffr  24254  ptcmplem5  24381  nmoleub2lem2  25443  ellogdm  26973  pntpbnd  27921  cvbr2  32891  cvnbtwn2  32895  cvnbtwn3  32896  cvnbtwn4  32897  chpssati  32971  chrelat2i  32973  chrelat3  32979  bnj1476  35524  bnj110  35535  bnj1388  35710  df3nandALT1  37280  imnand2  37283  bj-andnotim  37551  poimirlem11  38643  poimirlem12  38644  fdc  38773  lpssat  40164  lssat  40167  lcvbr2  40173  lcvbr3  40174  lcvnbtwn2  40178  lcvnbtwn3  40179  cvrval2  40425  cvrnbtwn2  40426  cvrnbtwn3  40427  cvrnbtwn4  40430  atlrelat1  40472  hlrelat2  40554  dihglblem6  42491  hashnexinj  43272  naddgeoa  44490  faosnf0.11b  44522  dfsucon  44618  or3or  45117  uneqsn  45119  plvcofphax  48111  ichim  48633