Theorem iman 406

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 400

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 210  df-an 401

This theorem is referenced by:  pm3.24  407  annim  408  xor  1032  nic-mpALT  1702  nic-axALT  1704  rexanali  3119  difdif  4090  dfss4  4223  difin  4226  ssdif0  4322  difin0ss  4329  inssdif0OLD  4331  dfif2  4490  dffv2  6978  tfinds  7857  sdom0  9098  domtriord  9112  sdom1  9211  inf3lem3  9600  nominpos  12482  isprm3  16742  vdwlem13  17054  vdwnn  17059  psgnunilem4  19568  efgredlem  19818  efgred  19819  ufinffr  24067  ptcmplem5  24194  nmoleub2lem2  25256  ellogdm  26785  pntpbnd  27733  cvbr2  32616  cvnbtwn2  32620  cvnbtwn3  32621  cvnbtwn4  32622  chpssati  32696  chrelat2i  32698  chrelat3  32704  bnj1476  35216  bnj110  35227  bnj1388  35402  dff15  35453  df3nandALT1  36891  imnand2  36894  bj-andnotim  37162  lindsenlbs  38247  poimirlem11  38263  poimirlem12  38264  fdc  38377  lpssat  39768  lssat  39771  lcvbr2  39777  lcvbr3  39778  lcvnbtwn2  39782  lcvnbtwn3  39783  cvrval2  40029  cvrnbtwn2  40030  cvrnbtwn3  40031  cvrnbtwn4  40034  atlrelat1  40076  hlrelat2  40158  dihglblem6  42095  hashnexinj  42876  naddgeoa  44104  faosnf0.11b  44136  dfsucon  44232  or3or  44732  uneqsn  44734  plvcofphax  47667  ichim  48189