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

Theorem iman 415
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 284 . . 3  |-  ( ps  <->  -. 
-.  ps )
21imbi2i 305 . 2  |-  ( (
ph  ->  ps )  <->  ( ph  ->  -.  -.  ps )
)
3 imnan 413 . 2  |-  ( (
ph  ->  -.  -.  ps )  <->  -.  ( ph  /\  -.  ps ) )
42, 3bitri 242 1  |-  ( (
ph  ->  ps )  <->  -.  ( ph  /\  -.  ps )
)
Colors of variables: wff set class
Syntax hints:   -. wn 5    -> wi 6    <-> wb 178    /\ wa 360
This theorem is referenced by:  annim  416  pm3.24  857  xor  866  nannan  1296  nic-mpALT  1432  nic-axALT  1434  difdif  3303  dfss4  3404  difin  3407  npss0  3494  ssdif0  3514  difin0ss  3521  inssdif0  3522  dfif2  3568  notzfaus  4184  tfinds  4649  dffv2  5553  domtriord  7002  inf3lem3  7326  nominpos  9943  isprm3  12761  vdwlem13  13034  vdwnn  13039  efgredlem  15050  efgred  15051  ufinffr  17618  ptcmplem5  17744  nmoleub2lem2  18591  ellogdm  19980  pntpbnd  20731  cvbr2  22855  cvnbtwn2  22859  cvnbtwn3  22860  cvnbtwn4  22861  chpssati  22935  chrelat2i  22937  chrelat3  22943  df3nandALT1  24242  imnand2  24245  fdc  25854  prtlem80  26123  psgnunilem4  26819  bnj1476  28146  bnj110  28157  bnj1388  28330  lpssat  28470  lssat  28473  lcvbr2  28479  lcvbr3  28480  lcvnbtwn2  28484  lcvnbtwn3  28485  cvrval2  28731  cvrnbtwn2  28732  cvrnbtwn3  28733  cvrnbtwn4  28736  atlrelat1  28778  hlrelat2  28859  dihglblem6  30797
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10
This theorem depends on definitions:  df-bi 179  df-an 362
  Copyright terms: Public domain W3C validator