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

Theorem iman 413
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 282 . . 3  |-  ( ps  <->  -. 
-.  ps )
21imbi2i 303 . 2  |-  ( (
ph  ->  ps )  <->  ( ph  ->  -.  -.  ps )
)
3 imnan 411 . 2  |-  ( (
ph  ->  -.  -.  ps )  <->  -.  ( ph  /\  -.  ps ) )
42, 3bitri 240 1  |-  ( (
ph  ->  ps )  <->  -.  ( ph  /\  -.  ps )
)
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 176    /\ wa 358
This theorem is referenced by:  annim  414  pm3.24  852  xor  861  nannan  1291  nic-mpALT  1427  nic-axALT  1429  difdif  3302  dfss4  3403  difin  3406  npss0  3493  ssdif0  3513  difin0ss  3520  inssdif0  3521  dfif2  3567  notzfaus  4185  tfinds  4650  dffv2  5592  domtriord  7007  inf3lem3  7331  nominpos  9948  isprm3  12767  vdwlem13  13040  vdwnn  13045  efgredlem  15056  efgred  15057  ufinffr  17624  ptcmplem5  17750  nmoleub2lem2  18597  ellogdm  19986  pntpbnd  20737  cvbr2  22863  cvnbtwn2  22867  cvnbtwn3  22868  cvnbtwn4  22869  chpssati  22943  chrelat2i  22945  chrelat3  22951  df3nandALT1  24835  imnand2  24838  fdc  26455  prtlem80  26724  psgnunilem4  27420  bnj1476  28879  bnj110  28890  bnj1388  29063  lpssat  29203  lssat  29206  lcvbr2  29212  lcvbr3  29213  lcvnbtwn2  29217  lcvnbtwn3  29218  cvrval2  29464  cvrnbtwn2  29465  cvrnbtwn3  29466  cvrnbtwn4  29469  atlrelat1  29511  hlrelat2  29592  dihglblem6  31530
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 177  df-an 360
  Copyright terms: Public domain W3C validator