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  27665  bnj110  27676  bnj1388  27849  equextvK  27977  lpssat  28107  lssat  28110  lcvbr2  28116  lcvbr3  28117  lcvnbtwn2  28121  lcvnbtwn3  28122  cvrval2  28368  cvrnbtwn2  28369  cvrnbtwn3  28370  cvrnbtwn4  28373  atlrelat1  28415  hlrelat2  28496  dihglblem6  30434
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