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  880  xor  889  nannan  1347  nic-mpALT  1489  nic-axALT  1491  rexanali  2917  difdif  3630  dfss4  3732  difin  3735  npss0  3865  ssdif0  3885  difin0ss  3893  inssdif0  3894  dfif2  3941  notzfaus  4622  dffv2  5938  tfinds  6672  domtriord  7660  inf3lem3  8043  nominpos  10771  isprm3  14081  vdwlem13  14366  vdwnn  14371  psgnunilem4  16318  efgredlem  16561  efgred  16562  ufinffr  20165  ptcmplem5  20291  nmoleub2lem2  21334  ellogdm  22748  pntpbnd  23501  cvbr2  26878  cvnbtwn2  26882  cvnbtwn3  26883  cvnbtwn4  26884  chpssati  26958  chrelat2i  26960  chrelat3  26966  df3nandALT1  29439  imnand2  29442  fdc  29841  bnj1476  32984  bnj110  32995  bnj1388  33168  bj-andnotim  33258  lpssat  33810  lssat  33813  lcvbr2  33819  lcvbr3  33820  lcvnbtwn2  33824  lcvnbtwn3  33825  cvrval2  34071  cvrnbtwn2  34072  cvrnbtwn3  34073  cvrnbtwn4  34076  atlrelat1  34118  hlrelat2  34199  dihglblem6  36137
  Copyright terms: Public domain W3C validator