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  877  xor  886  nannan  1338  nic-mpALT  1480  nic-axALT  1482  difdif  3585  dfss4  3687  difin  3690  npss0  3820  ssdif0  3840  difin0ss  3848  inssdif0  3849  dfif2  3896  notzfaus  4570  dffv2  5868  tfinds  6575  domtriord  7562  inf3lem3  7942  nominpos  10667  isprm3  13885  vdwlem13  14167  vdwnn  14172  psgnunilem4  16117  efgredlem  16360  efgred  16361  ufinffr  19629  ptcmplem5  19755  nmoleub2lem2  20798  ellogdm  22212  pntpbnd  22965  cvbr2  25834  cvnbtwn2  25838  cvnbtwn3  25839  cvnbtwn4  25840  chpssati  25914  chrelat2i  25916  chrelat3  25922  df3nandALT1  28382  imnand2  28385  fdc  28784  bnj1476  32153  bnj110  32164  bnj1388  32337  bj-andnotim  32427  lpssat  32977  lssat  32980  lcvbr2  32986  lcvbr3  32987  lcvnbtwn2  32991  lcvnbtwn3  32992  cvrval2  33238  cvrnbtwn2  33239  cvrnbtwn3  33240  cvrnbtwn4  33243  atlrelat1  33285  hlrelat2  33366  dihglblem6  35304
  Copyright terms: Public domain W3C validator