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

Theorem iman 415
Description: Express implication in terms of conjunction. Theorem 3.4(27) of [Stoll] p. 176. (Contributed by NM, 5-Aug-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 284 . . 3  |-  ( ps  <->  -. 
-.  ps )
21imbi2i 305 . 2  |-  ( (
ph  ->  ps )  <->  ( ph  ->  -.  -.  ps )
)
3 imnan 413 . 2  |-  ( (
ph  ->  -.  -.  ps )  <->  -.  ( ph  /\  -.  ps ) )
42, 3bitri 242 1  |-  ( (
ph  ->  ps )  <->  -.  ( ph  /\  -.  ps )
)
Colors of variables: wff set class
Syntax hints:   -. wn 5    -> wi 6    <-> wb 178    /\ wa 360
This theorem is referenced by:  annim  416  pm3.24  857  xor  866  nannan  1296  nic-mpALT  1432  nic-axALT  1434  difdif  3219  dfss4  3310  difin  3313  npss0  3400  ssdif0  3420  difin0ss  3426  inssdif0  3427  dfif2  3472  notzfaus  4079  tfinds  4541  dffv2  5444  domtriord  6892  inf3lem3  7215  nominpos  9827  isprm3  12641  vdwlem13  12914  vdwnn  12919  efgredlem  14891  efgred  14892  ufinffr  17456  ptcmplem5  17582  nmoleub2lem2  18429  ellogdm  19818  pntpbnd  20569  cvbr2  22693  cvnbtwn2  22697  cvnbtwn3  22698  cvnbtwn4  22699  chpssati  22773  chrelat2i  22775  chrelat3  22781  df3nandALT1  24009  imnand2  24012  fdc  25621  prtlem80  25890  psgnunilem4  26586  bnj1476  27568  bnj110  27579  bnj1388  27752  lpssat  27892  lssat  27895  lcvbr2  27901  lcvbr3  27902  lcvnbtwn2  27906  lcvnbtwn3  27907  cvrval2  28153  cvrnbtwn2  28154  cvrnbtwn3  28155  cvrnbtwn4  28158  atlrelat1  28200  hlrelat2  28281  dihglblem6  30219
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10
This theorem depends on definitions:  df-bi 179  df-an 362
  Copyright terms: Public domain W3C validator