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

Theorem iman 391
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 307 . . 3 (𝜓 ↔ ¬ ¬ 𝜓)
21imbi2i 328 . 2 ((𝜑𝜓) ↔ (𝜑 → ¬ ¬ 𝜓))
3 imnan 389 . 2 ((𝜑 → ¬ ¬ 𝜓) ↔ ¬ (𝜑 ∧ ¬ 𝜓))
42, 3bitri 267 1 ((𝜑𝜓) ↔ ¬ (𝜑 ∧ ¬ 𝜓))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 198  wa 385
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 199  df-an 386
This theorem is referenced by:  pm3.24  392  annim  393  xor  1039  nic-mpALT  1768  nic-axALT  1770  rexanali  3178  difdif  3934  dfss4  4059  difin  4062  ssdif0  4142  difin0ss  4147  inssdif0  4148  dfif2  4279  notzfaus  5032  dffv2  6496  tfinds  7293  domtriord  8348  inf3lem3  8777  nominpos  11557  isprm3  15730  vdwlem13  16030  vdwnn  16035  psgnunilem4  18230  efgredlem  18474  efgredlemOLD  18475  efgred  18476  ufinffr  22061  ptcmplem5  22188  nmoleub2lem2  23243  ellogdm  24726  pntpbnd  25629  cvbr2  29667  cvnbtwn2  29671  cvnbtwn3  29672  cvnbtwn4  29673  chpssati  29747  chrelat2i  29749  chrelat3  29755  bnj1476  31434  bnj110  31445  bnj1388  31618  df3nandALT1  32906  imnand2  32909  bj-andnotim  33078  lindsenlbs  33893  poimirlem11  33909  poimirlem12  33910  fdc  34028  lpssat  35034  lssat  35037  lcvbr2  35043  lcvbr3  35044  lcvnbtwn2  35048  lcvnbtwn3  35049  cvrval2  35295  cvrnbtwn2  35296  cvrnbtwn3  35297  cvrnbtwn4  35300  atlrelat1  35342  hlrelat2  35424  dihglblem6  37361  or3or  39097  uneqsn  39099  plvcofphax  41856
  Copyright terms: Public domain W3C validator