Theorem iman 439

Description: Express implication in terms of conjunction. 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 303	. . 3 ⊢ (𝜓 ↔ ¬ ¬ 𝜓)
2	1	imbi2i 325	. 2 ⊢ ((𝜑 → 𝜓) ↔ (𝜑 → ¬ ¬ 𝜓))
3		imnan 437	. 2 ⊢ ((𝜑 → ¬ ¬ 𝜓) ↔ ¬ (𝜑 ∧ ¬ 𝜓))
4	2, 3	bitri 263	1 ⊢ ((𝜑 → 𝜓) ↔ ¬ (𝜑 ∧ ¬ 𝜓))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 195   ∧ wa 383

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 196  df-an 385

This theorem is referenced by:  annim  440  pm3.24  922  xor  931  nic-mpALT  1588  nic-axALT  1590  rexanali  2981  difdif  3698  dfss4  3820  difin  3823  ssdif0  3896  difin0ss  3900  inssdif0  3901  npss0OLD  3967  dfif2  4038  notzfaus  4766  dffv2  6181  tfinds  6951  domtriord  7991  inf3lem3  8410  nominpos  11146  isprm3  15234  vdwlem13  15535  vdwnn  15540  psgnunilem4  17740  efgredlem  17983  efgred  17984  ufinffr  21543  ptcmplem5  21670  nmoleub2lem2  22724  ellogdm  24185  pntpbnd  25077  cvbr2  28526  cvnbtwn2  28530  cvnbtwn3  28531  cvnbtwn4  28532  chpssati  28606  chrelat2i  28608  chrelat3  28614  bnj1476  30171  bnj110  30182  bnj1388  30355  df3nandALT1  31566  imnand2  31569  bj-andnotim  31746  lindsenlbs  32574  poimirlem11  32590  poimirlem12  32591  fdc  32711  lpssat  33318  lssat  33321  lcvbr2  33327  lcvbr3  33328  lcvnbtwn2  33332  lcvnbtwn3  33333  cvrval2  33579  cvrnbtwn2  33580  cvrnbtwn3  33581  cvrnbtwn4  33584  atlrelat1  33626  hlrelat2  33707  dihglblem6  35647  or3or  37339  uneqsn  37341  plvcofphax  39763