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, 12-Mar-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  882  xor  891  nannanOLD  1350  nic-mpALT  1492  nic-axALT  1494  rexanali  2896  difdif  3615  dfss4  3717  difin  3720  npss0  3851  ssdif0  3871  difin0ss  3880  inssdif0  3881  dfif2  3928  notzfaus  4612  dffv2  5931  tfinds  6679  domtriord  7665  inf3lem3  8050  nominpos  10781  isprm3  14103  vdwlem13  14388  vdwnn  14393  psgnunilem4  16396  efgredlem  16639  efgred  16640  ufinffr  20303  ptcmplem5  20429  nmoleub2lem2  21472  ellogdm  22892  pntpbnd  23645  cvbr2  27074  cvnbtwn2  27078  cvnbtwn3  27079  cvnbtwn4  27080  chpssati  27154  chrelat2i  27156  chrelat3  27162  df3nandALT1  29837  imnand2  29840  fdc  30213  bnj1476  33638  bnj110  33649  bnj1388  33822  bj-andnotim  33925  lpssat  34478  lssat  34481  lcvbr2  34487  lcvbr3  34488  lcvnbtwn2  34492  lcvnbtwn3  34493  cvrval2  34739  cvrnbtwn2  34740  cvrnbtwn3  34741  cvrnbtwn4  34744  atlrelat1  34786  hlrelat2  34867  dihglblem6  36807
  Copyright terms: Public domain W3C validator