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

Theorem iman 414
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 283 . . 3  |-  ( ps  <->  -. 
-.  ps )
21imbi2i 304 . 2  |-  ( (
ph  ->  ps )  <->  ( ph  ->  -.  -.  ps )
)
3 imnan 412 . 2  |-  ( (
ph  ->  -.  -.  ps )  <->  -.  ( ph  /\  -.  ps ) )
42, 3bitri 241 1  |-  ( (
ph  ->  ps )  <->  -.  ( ph  /\  -.  ps )
)
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 177    /\ wa 359
This theorem is referenced by:  annim  415  pm3.24  853  xor  862  nannan  1297  nic-mpALT  1443  nic-axALT  1445  difdif  3409  dfss4  3511  difin  3514  npss0  3602  ssdif0  3622  difin0ss  3630  inssdif0  3631  dfif2  3677  notzfaus  4308  tfinds  4772  dffv2  5728  domtriord  7182  inf3lem3  7511  nominpos  10129  isprm3  13008  vdwlem13  13281  vdwnn  13286  efgredlem  15299  efgred  15300  ufinffr  17875  ptcmplem5  18001  nmoleub2lem2  18988  ellogdm  20390  pntpbnd  21142  cvbr2  23627  cvnbtwn2  23631  cvnbtwn3  23632  cvnbtwn4  23633  chpssati  23707  chrelat2i  23709  chrelat3  23715  df3nandALT1  25853  imnand2  25856  fdc  26133  psgnunilem4  27082  bnj1476  28549  bnj110  28560  bnj1388  28733  lpssat  29179  lssat  29182  lcvbr2  29188  lcvbr3  29189  lcvnbtwn2  29193  lcvnbtwn3  29194  cvrval2  29440  cvrnbtwn2  29441  cvrnbtwn3  29442  cvrnbtwn4  29445  atlrelat1  29487  hlrelat2  29568  dihglblem6  31506
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 178  df-an 361
  Copyright terms: Public domain W3C validator