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  3277  dfss4  3378  difin  3381  npss0  3468  ssdif0  3488  difin0ss  3495  inssdif0  3496  dfif2  3541  notzfaus  4157  tfinds  4622  dffv2  5526  domtriord  6975  inf3lem3  7299  nominpos  9915  isprm3  12729  vdwlem13  13002  vdwnn  13007  efgredlem  15018  efgred  15019  ufinffr  17586  ptcmplem5  17712  nmoleub2lem2  18559  ellogdm  19948  pntpbnd  20699  cvbr2  22823  cvnbtwn2  22827  cvnbtwn3  22828  cvnbtwn4  22829  chpssati  22903  chrelat2i  22905  chrelat3  22911  df3nandALT1  24210  imnand2  24213  fdc  25822  prtlem80  26091  psgnunilem4  26787  bnj1476  27928  bnj110  27939  bnj1388  28112  equextvK  28240  lpssat  28370  lssat  28373  lcvbr2  28379  lcvbr3  28380  lcvnbtwn2  28384  lcvnbtwn3  28385  cvrval2  28631  cvrnbtwn2  28632  cvrnbtwn3  28633  cvrnbtwn4  28636  atlrelat1  28678  hlrelat2  28759  dihglblem6  30697
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