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

Theorem iman 426
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  |-  ( (
ph  ->  ps )  <->  -.  ( ph  /\  -.  ps )
)

Proof of Theorem iman
StepHypRef Expression
1 notnot 293 . . 3  |-  ( ps  <->  -. 
-.  ps )
21imbi2i 314 . 2  |-  ( (
ph  ->  ps )  <->  ( ph  ->  -.  -.  ps )
)
3 imnan 424 . 2  |-  ( (
ph  ->  -.  -.  ps )  <->  -.  ( ph  /\  -.  ps ) )
42, 3bitri 253 1  |-  ( (
ph  ->  ps )  <->  -.  ( ph  /\  -.  ps )
)
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 188    /\ wa 371
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 189  df-an 373
This theorem is referenced by:  annim  427  pm3.24  893  xor  902  nannanOLD  1390  nic-mpALT  1555  nic-axALT  1557  rexanali  2840  difdif  3559  dfss4  3677  difin  3680  npss0  3803  ssdif0  3823  difin0ss  3833  inssdif0  3834  dfif2  3883  notzfaus  4578  dffv2  5938  tfinds  6686  domtriord  7718  inf3lem3  8135  nominpos  10849  isprm3  14633  vdwlem13  14943  vdwnn  14948  psgnunilem4  17138  efgredlem  17397  efgred  17398  ufinffr  20944  ptcmplem5  21071  nmoleub2lem2  22130  ellogdm  23584  pntpbnd  24426  cvbr2  27936  cvnbtwn2  27940  cvnbtwn3  27941  cvnbtwn4  27942  chpssati  28016  chrelat2i  28018  chrelat3  28024  bnj1476  29658  bnj110  29669  bnj1388  29842  df3nandALT1  31057  imnand2  31060  bj-andnotim  31172  poimirlem11  31951  poimirlem12  31952  fdc  32074  lpssat  32579  lssat  32582  lcvbr2  32588  lcvbr3  32589  lcvnbtwn2  32593  lcvnbtwn3  32594  cvrval2  32840  cvrnbtwn2  32841  cvrnbtwn3  32842  cvrnbtwn4  32845  atlrelat1  32887  hlrelat2  32968  dihglblem6  34908  plvcofphax  38535
  Copyright terms: Public domain W3C validator