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

Theorem iman 413
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 282 . . 3  |-  ( ps  <->  -. 
-.  ps )
21imbi2i 303 . 2  |-  ( (
ph  ->  ps )  <->  ( ph  ->  -.  -.  ps )
)
3 imnan 411 . 2  |-  ( (
ph  ->  -.  -.  ps )  <->  -.  ( ph  /\  -.  ps ) )
42, 3bitri 240 1  |-  ( (
ph  ->  ps )  <->  -.  ( ph  /\  -.  ps )
)
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 176    /\ wa 358
This theorem is referenced by:  annim  414  pm3.24  852  xor  861  nannan  1291  nic-mpALT  1427  nic-axALT  1429  difdif  3315  dfss4  3416  difin  3419  npss0  3506  ssdif0  3526  difin0ss  3533  inssdif0  3534  dfif2  3580  notzfaus  4201  tfinds  4666  dffv2  5608  domtriord  7023  inf3lem3  7347  nominpos  9964  isprm3  12783  vdwlem13  13056  vdwnn  13061  efgredlem  15072  efgred  15073  ufinffr  17640  ptcmplem5  17766  nmoleub2lem2  18613  ellogdm  20002  pntpbnd  20753  cvbr2  22879  cvnbtwn2  22883  cvnbtwn3  22884  cvnbtwn4  22885  chpssati  22959  chrelat2i  22961  chrelat3  22967  df3nandALT1  24907  imnand2  24910  fdc  26558  prtlem80  26827  psgnunilem4  27523  bnj1476  29195  bnj110  29206  bnj1388  29379  lpssat  29825  lssat  29828  lcvbr2  29834  lcvbr3  29835  lcvnbtwn2  29839  lcvnbtwn3  29840  cvrval2  30086  cvrnbtwn2  30087  cvrnbtwn3  30088  cvrnbtwn4  30091  atlrelat1  30133  hlrelat2  30214  dihglblem6  32152
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 177  df-an 360
  Copyright terms: Public domain W3C validator