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

Theorem iman 414
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 283 . . 3  |-  ( ps  <->  -. 
-.  ps )
21imbi2i 304 . 2  |-  ( (
ph  ->  ps )  <->  ( ph  ->  -.  -.  ps )
)
3 imnan 412 . 2  |-  ( (
ph  ->  -.  -.  ps )  <->  -.  ( ph  /\  -.  ps ) )
42, 3bitri 241 1  |-  ( (
ph  ->  ps )  <->  -.  ( ph  /\  -.  ps )
)
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 177    /\ wa 359
This theorem is referenced by:  annim  415  pm3.24  853  xor  862  nannan  1297  nic-mpALT  1443  nic-axALT  1445  difdif  3433  dfss4  3535  difin  3538  npss0  3626  ssdif0  3646  difin0ss  3654  inssdif0  3655  dfif2  3701  notzfaus  4334  tfinds  4798  dffv2  5755  domtriord  7212  inf3lem3  7541  nominpos  10160  isprm3  13043  vdwlem13  13316  vdwnn  13321  efgredlem  15334  efgred  15335  ufinffr  17914  ptcmplem5  18040  nmoleub2lem2  19077  ellogdm  20483  pntpbnd  21235  cvbr2  23739  cvnbtwn2  23743  cvnbtwn3  23744  cvnbtwn4  23745  chpssati  23819  chrelat2i  23821  chrelat3  23827  df3nandALT1  26050  imnand2  26053  fdc  26339  psgnunilem4  27288  bnj1476  28924  bnj110  28935  bnj1388  29108  lpssat  29496  lssat  29499  lcvbr2  29505  lcvbr3  29506  lcvnbtwn2  29510  lcvnbtwn3  29511  cvrval2  29757  cvrnbtwn2  29758  cvrnbtwn3  29759  cvrnbtwn4  29762  atlrelat1  29804  hlrelat2  29885  dihglblem6  31823
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 178  df-an 361
  Copyright terms: Public domain W3C validator