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  1008  nic-mpALT  1664  nic-axALT  1666  rexanali  3265  difdif  4106  dfss4  4234  difin  4237  ssdif0  4322  difin0ss  4327  inssdif0  4328  dfif2  4467  notzfausOLD  5255  dffv2  6750  tfinds  7562  domtriord  8652  inf3lem3  9082  nominpos  11863  isprm3  16017  vdwlem13  16319  vdwnn  16324  psgnunilem4  18556  efgredlem  18804  efgred  18805  ufinffr  22467  ptcmplem5  22594  nmoleub2lem2  23649  ellogdm  25149  pntpbnd  26092  cvbr2  29988  cvnbtwn2  29992  cvnbtwn3  29993  cvnbtwn4  29994  chpssati  30068  chrelat2i  30070  chrelat3  30076  bnj1476  32019  bnj110  32030  bnj1388  32203  dff15  32251  df3nandALT1  33645  imnand2  33648  bj-andnotim  33820  lindsenlbs  34769  poimirlem11  34785  poimirlem12  34786  fdc  34903  lpssat  36031  lssat  36034  lcvbr2  36040  lcvbr3  36041  lcvnbtwn2  36045  lcvnbtwn3  36046  cvrval2  36292  cvrnbtwn2  36293  cvrnbtwn3  36294  cvrnbtwn4  36297  atlrelat1  36339  hlrelat2  36421  dihglblem6  38358  dfsucon  39769  or3or  40251  uneqsn  40253  plvcofphax  43064
  Copyright terms: Public domain W3C validator