MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  iman Structured version   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 3    -> wi 4    <-> wb 178    /\ wa 360
This theorem is referenced by:  annim  416  pm3.24  854  xor  863  nannan  1301  nic-mpALT  1447  nic-axALT  1449  difdif  3475  dfss4  3577  difin  3580  npss0  3668  ssdif0  3688  difin0ss  3696  inssdif0  3697  dfif2  3743  notzfaus  4377  tfinds  4842  dffv2  5799  domtriord  7256  inf3lem3  7588  nominpos  10209  isprm3  13093  vdwlem13  13366  vdwnn  13371  efgredlem  15384  efgred  15385  ufinffr  17966  ptcmplem5  18092  nmoleub2lem2  19129  ellogdm  20535  pntpbnd  21287  cvbr2  23791  cvnbtwn2  23795  cvnbtwn3  23796  cvnbtwn4  23797  chpssati  23871  chrelat2i  23873  chrelat3  23879  df3nandALT1  26151  imnand2  26154  fdc  26463  psgnunilem4  27411  bnj1476  29292  bnj110  29303  bnj1388  29476  lpssat  29885  lssat  29888  lcvbr2  29894  lcvbr3  29895  lcvnbtwn2  29899  lcvnbtwn3  29900  cvrval2  30146  cvrnbtwn2  30147  cvrnbtwn3  30148  cvrnbtwn4  30151  atlrelat1  30193  hlrelat2  30274  dihglblem6  32212
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 179  df-an 362
  Copyright terms: Public domain W3C validator