MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  iman Structured version   Visualization version   GIF version

Theorem iman 402
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
StepHypRef Expression
1 notnotb 316 . . 3 (𝜓 ↔ ¬ ¬ 𝜓)
21imbi2i 337 . 2 ((𝜑𝜓) ↔ (𝜑 → ¬ ¬ 𝜓))
3 imnan 400 . 2 ((𝜑 → ¬ ¬ 𝜓) ↔ ¬ (𝜑 ∧ ¬ 𝜓))
42, 3bitri 276 1 ((𝜑𝜓) ↔ ¬ (𝜑 ∧ ¬ 𝜓))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 207  wa 396
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 208  df-an 397
This theorem is referenced by:  pm3.24  403  annim  404  xor  1010  nic-mpALT  1666  nic-axALT  1668  rexanali  3269  difdif  4110  dfss4  4238  difin  4241  ssdif0  4326  difin0ss  4331  inssdif0  4332  dfif2  4471  notzfausOLD  5259  dffv2  6752  tfinds  7565  domtriord  8655  inf3lem3  9085  nominpos  11866  isprm3  16020  vdwlem13  16322  vdwnn  16327  psgnunilem4  18548  efgredlem  18796  efgred  18797  ufinffr  22456  ptcmplem5  22583  nmoleub2lem2  23638  ellogdm  25138  pntpbnd  26081  cvbr2  29977  cvnbtwn2  29981  cvnbtwn3  29982  cvnbtwn4  29983  chpssati  30057  chrelat2i  30059  chrelat3  30065  bnj1476  32008  bnj110  32019  bnj1388  32192  dff15  32240  df3nandALT1  33634  imnand2  33637  bj-andnotim  33809  lindsenlbs  34757  poimirlem11  34773  poimirlem12  34774  fdc  34891  lpssat  36019  lssat  36022  lcvbr2  36028  lcvbr3  36029  lcvnbtwn2  36033  lcvnbtwn3  36034  cvrval2  36280  cvrnbtwn2  36281  cvrnbtwn3  36282  cvrnbtwn4  36285  atlrelat1  36327  hlrelat2  36409  dihglblem6  38346  dfsucon  39757  or3or  40239  uneqsn  40241  plvcofphax  43052
  Copyright terms: Public domain W3C validator