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

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
StepHypRef Expression
1 notnotb 304 . . 3 (𝜓 ↔ ¬ ¬ 𝜓)
21imbi2i 325 . 2 ((𝜑𝜓) ↔ (𝜑 → ¬ ¬ 𝜓))
3 imnan 437 . 2 ((𝜑 → ¬ ¬ 𝜓) ↔ ¬ (𝜑 ∧ ¬ 𝜓))
42, 3bitri 264 1 ((𝜑𝜓) ↔ ¬ (𝜑 ∧ ¬ 𝜓))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  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 197  df-an 385
This theorem is referenced by:  annim  440  pm3.24  944  xor  953  nic-mpALT  1637  nic-axALT  1639  rexanali  3027  difdif  3769  dfss4  3891  difin  3894  ssdif0  3975  difin0ss  3979  inssdif0  3980  npss0OLD  4048  dfif2  4121  notzfaus  4870  dffv2  6310  tfinds  7101  domtriord  8147  inf3lem3  8565  nominpos  11307  isprm3  15443  vdwlem13  15744  vdwnn  15749  psgnunilem4  17963  efgredlem  18206  efgred  18207  ufinffr  21780  ptcmplem5  21907  nmoleub2lem2  22962  ellogdm  24430  pntpbnd  25322  cvbr2  29270  cvnbtwn2  29274  cvnbtwn3  29275  cvnbtwn4  29276  chpssati  29350  chrelat2i  29352  chrelat3  29358  bnj1476  31043  bnj110  31054  bnj1388  31227  df3nandALT1  32521  imnand2  32524  bj-andnotim  32698  lindsenlbs  33534  poimirlem11  33550  poimirlem12  33551  fdc  33671  lpssat  34618  lssat  34621  lcvbr2  34627  lcvbr3  34628  lcvnbtwn2  34632  lcvnbtwn3  34633  cvrval2  34879  cvrnbtwn2  34880  cvrnbtwn3  34881  cvrnbtwn4  34884  atlrelat1  34926  hlrelat2  35007  dihglblem6  36946  or3or  38636  uneqsn  38638  plvcofphax  41435
  Copyright terms: Public domain W3C validator