Theorem iman 404

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

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

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 399

This theorem is referenced by:  pm3.24  405  annim  406  xor  1011  nic-mpALT  1673  nic-axALT  1675  rexanali  3265  difdif  4107  dfss4  4235  difin  4238  ssdif0  4323  difin0ss  4328  inssdif0  4329  dfif2  4469  notzfausOLD  5263  dffv2  6756  tfinds  7574  domtriord  8663  inf3lem3  9093  nominpos  11875  isprm3  16027  vdwlem13  16329  vdwnn  16334  psgnunilem4  18625  efgredlem  18873  efgred  18874  ufinffr  22537  ptcmplem5  22664  nmoleub2lem2  23720  ellogdm  25222  pntpbnd  26164  cvbr2  30060  cvnbtwn2  30064  cvnbtwn3  30065  cvnbtwn4  30066  chpssati  30140  chrelat2i  30142  chrelat3  30148  bnj1476  32119  bnj110  32130  bnj1388  32305  dff15  32353  df3nandALT1  33747  imnand2  33750  bj-andnotim  33922  lindsenlbs  34902  poimirlem11  34918  poimirlem12  34919  fdc  35035  lpssat  36164  lssat  36167  lcvbr2  36173  lcvbr3  36174  lcvnbtwn2  36178  lcvnbtwn3  36179  cvrval2  36425  cvrnbtwn2  36426  cvrnbtwn3  36427  cvrnbtwn4  36430  atlrelat1  36472  hlrelat2  36554  dihglblem6  38491  dfsucon  39909  or3or  40391  uneqsn  40393  plvcofphax  43203