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

Theorem iman 440
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
StepHypRef Expression
1 notnotb 304 . . 3 (𝜓 ↔ ¬ ¬ 𝜓)
21imbi2i 326 . 2 ((𝜑𝜓) ↔ (𝜑 → ¬ ¬ 𝜓))
3 imnan 438 . 2 ((𝜑 → ¬ ¬ 𝜓) ↔ ¬ (𝜑 ∧ ¬ 𝜓))
42, 3bitri 264 1 ((𝜑𝜓) ↔ ¬ (𝜑 ∧ ¬ 𝜓))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wa 384
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 197  df-an 386
This theorem is referenced by:  annim  441  pm3.24  925  xor  934  nic-mpALT  1594  nic-axALT  1596  rexanali  2992  difdif  3716  dfss4  3838  difin  3841  ssdif0  3918  difin0ss  3922  inssdif0  3923  npss0OLD  3989  dfif2  4062  notzfaus  4802  dffv2  6230  tfinds  7009  domtriord  8053  inf3lem3  8474  nominpos  11216  isprm3  15323  vdwlem13  15624  vdwnn  15629  psgnunilem4  17841  efgredlem  18084  efgred  18085  ufinffr  21646  ptcmplem5  21773  nmoleub2lem2  22829  ellogdm  24292  pntpbnd  25184  cvbr2  29003  cvnbtwn2  29007  cvnbtwn3  29008  cvnbtwn4  29009  chpssati  29083  chrelat2i  29085  chrelat3  29091  bnj1476  30646  bnj110  30657  bnj1388  30830  df3nandALT1  32059  imnand2  32062  bj-andnotim  32236  lindsenlbs  33057  poimirlem11  33073  poimirlem12  33074  fdc  33194  lpssat  33801  lssat  33804  lcvbr2  33810  lcvbr3  33811  lcvnbtwn2  33815  lcvnbtwn3  33816  cvrval2  34062  cvrnbtwn2  34063  cvrnbtwn3  34064  cvrnbtwn4  34067  atlrelat1  34109  hlrelat2  34190  dihglblem6  36130  or3or  37822  uneqsn  37824  plvcofphax  40434
  Copyright terms: Public domain W3C validator