Theorem iman 405

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 317	. . 3 ⊢ (𝜓 ↔ ¬ ¬ 𝜓)
2	1	imbi2i 338	. 2 ⊢ ((𝜑 → 𝜓) ↔ (𝜑 → ¬ ¬ 𝜓))
3		imnan 403	. 2 ⊢ ((𝜑 → ¬ ¬ 𝜓) ↔ ¬ (𝜑 ∧ ¬ 𝜓))
4	2, 3	bitri 277	1 ⊢ ((𝜑 → 𝜓) ↔ ¬ (𝜑 ∧ ¬ 𝜓))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 208   ∧ wa 399

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 209  df-an 400

This theorem is referenced by:  pm3.24  406  annim  407  xor  1027  nic-mpALT  1691  nic-axALT  1693  rexanali  3115  difdif  4086  dfss4  4219  difin  4222  ssdif0  4316  difin0ss  4323  inssdif0  4324  dfif2  4479  dffv2  6957  tfinds  7835  sdom0  9075  domtriord  9089  sdom1  9188  inf3lem3  9579  nominpos  12452  isprm3  16708  vdwlem13  17020  vdwnn  17025  psgnunilem4  19528  efgredlem  19778  efgred  19779  ufinffr  23977  ptcmplem5  24104  nmoleub2lem2  25166  ellogdm  26692  pntpbnd  27640  cvbr2  32443  cvnbtwn2  32447  cvnbtwn3  32448  cvnbtwn4  32449  chpssati  32523  chrelat2i  32525  chrelat3  32531  bnj1476  35103  bnj110  35114  bnj1388  35289  dff15  35339  df3nandALT1  36720  imnand2  36723  bj-andnotim  36992  lindsenlbs  38075  poimirlem11  38091  poimirlem12  38092  fdc  38205  lpssat  39598  lssat  39601  lcvbr2  39607  lcvbr3  39608  lcvnbtwn2  39612  lcvnbtwn3  39613  cvrval2  39859  cvrnbtwn2  39860  cvrnbtwn3  39861  cvrnbtwn4  39864  atlrelat1  39906  hlrelat2  39988  dihglblem6  41925  hashnexinj  42706  naddgeoa  43932  faosnf0.11b  43964  dfsucon  44060  or3or  44560  uneqsn  44562  plvcofphax  47502  ichim  48024