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  1300  nic-mpALT  1446  nic-axALT  1448  difdif  3465  dfss4  3567  difin  3570  npss0  3658  ssdif0  3678  difin0ss  3686  inssdif0  3687  dfif2  3733  notzfaus  4366  tfinds  4830  dffv2  5787  domtriord  7244  inf3lem3  7574  nominpos  10193  isprm3  13076  vdwlem13  13349  vdwnn  13354  efgredlem  15367  efgred  15368  ufinffr  17949  ptcmplem5  18075  nmoleub2lem2  19112  ellogdm  20518  pntpbnd  21270  cvbr2  23774  cvnbtwn2  23778  cvnbtwn3  23779  cvnbtwn4  23780  chpssati  23854  chrelat2i  23856  chrelat3  23862  df3nandALT1  26094  imnand2  26097  fdc  26386  psgnunilem4  27335  bnj1476  29072  bnj110  29083  bnj1388  29256  lpssat  29650  lssat  29653  lcvbr2  29659  lcvbr3  29660  lcvnbtwn2  29664  lcvnbtwn3  29665  cvrval2  29911  cvrnbtwn2  29912  cvrnbtwn3  29913  cvrnbtwn4  29916  atlrelat1  29958  hlrelat2  30039  dihglblem6  31977
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