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

Theorem iman 424
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 291 . . 3  |-  ( ps  <->  -. 
-.  ps )
21imbi2i 312 . 2  |-  ( (
ph  ->  ps )  <->  ( ph  ->  -.  -.  ps )
)
3 imnan 422 . 2  |-  ( (
ph  ->  -.  -.  ps )  <->  -.  ( ph  /\  -.  ps ) )
42, 3bitri 249 1  |-  ( (
ph  ->  ps )  <->  -.  ( ph  /\  -.  ps )
)
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 184    /\ wa 369
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 185  df-an 371
This theorem is referenced by:  annim  425  pm3.24  870  xor  879  nannan  1330  nic-mpALT  1482  nic-axALT  1484  difdif  3470  dfss4  3572  difin  3575  npss0  3705  ssdif0  3725  difin0ss  3733  inssdif0  3734  dfif2  3781  notzfaus  4455  dffv2  5752  tfinds  6459  domtriord  7445  inf3lem3  7824  nominpos  10548  isprm3  13754  vdwlem13  14036  vdwnn  14041  psgnunilem4  15982  efgredlem  16223  efgred  16224  ufinffr  19343  ptcmplem5  19469  nmoleub2lem2  20512  ellogdm  21968  pntpbnd  22721  cvbr2  25509  cvnbtwn2  25513  cvnbtwn3  25514  cvnbtwn4  25515  chpssati  25589  chrelat2i  25591  chrelat3  25597  df3nandALT1  28089  imnand2  28092  fdc  28482  bnj1476  31539  bnj110  31550  bnj1388  31723  bj-andnotim  31773  lpssat  32228  lssat  32231  lcvbr2  32237  lcvbr3  32238  lcvnbtwn2  32242  lcvnbtwn3  32243  cvrval2  32489  cvrnbtwn2  32490  cvrnbtwn3  32491  cvrnbtwn4  32494  atlrelat1  32536  hlrelat2  32617  dihglblem6  34555
  Copyright terms: Public domain W3C validator