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

Theorem iman 425
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 292 . . 3  |-  ( ps  <->  -. 
-.  ps )
21imbi2i 313 . 2  |-  ( (
ph  ->  ps )  <->  ( ph  ->  -.  -.  ps )
)
3 imnan 423 . 2  |-  ( (
ph  ->  -.  -.  ps )  <->  -.  ( ph  /\  -.  ps ) )
42, 3bitri 252 1  |-  ( (
ph  ->  ps )  <->  -.  ( ph  /\  -.  ps )
)
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 187    /\ wa 370
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 188  df-an 372
This theorem is referenced by:  annim  426  pm3.24  890  xor  899  nannanOLD  1385  nic-mpALT  1551  nic-axALT  1553  rexanali  2878  difdif  3591  dfss4  3707  difin  3710  npss0  3831  ssdif0  3851  difin0ss  3861  inssdif0  3862  dfif2  3911  notzfaus  4596  dffv2  5951  tfinds  6697  domtriord  7721  inf3lem3  8138  nominpos  10850  isprm3  14621  vdwlem13  14931  vdwnn  14936  psgnunilem4  17126  efgredlem  17385  efgred  17386  ufinffr  20931  ptcmplem5  21058  nmoleub2lem2  22117  ellogdm  23571  pntpbnd  24413  cvbr2  27922  cvnbtwn2  27926  cvnbtwn3  27927  cvnbtwn4  27928  chpssati  28002  chrelat2i  28004  chrelat3  28010  bnj1476  29654  bnj110  29665  bnj1388  29838  df3nandALT1  31050  imnand2  31053  bj-andnotim  31164  poimirlem11  31865  poimirlem12  31866  fdc  31988  lpssat  32498  lssat  32501  lcvbr2  32507  lcvbr3  32508  lcvnbtwn2  32512  lcvnbtwn3  32513  cvrval2  32759  cvrnbtwn2  32760  cvrnbtwn3  32761  cvrnbtwn4  32764  atlrelat1  32806  hlrelat2  32887  dihglblem6  34827  plvcofphax  38248
  Copyright terms: Public domain W3C validator