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

Theorem ianor 474
Description: Negated conjunction in terms of disjunction (De Morgan's law). Theorem *4.51 of [WhiteheadRussell] p. 120. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Andrew Salmon, 13-May-2011.)
Assertion
Ref Expression
ianor  |-  ( -.  ( ph  /\  ps ) 
<->  ( -.  ph  \/  -.  ps ) )

Proof of Theorem ianor
StepHypRef Expression
1 imnan 411 . 2  |-  ( (
ph  ->  -.  ps )  <->  -.  ( ph  /\  ps ) )
2 pm4.62 408 . 2  |-  ( (
ph  ->  -.  ps )  <->  ( -.  ph  \/  -.  ps ) )
31, 2bitr3i 242 1  |-  ( -.  ( ph  /\  ps ) 
<->  ( -.  ph  \/  -.  ps ) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 176    \/ wo 357    /\ wa 358
This theorem is referenced by:  anor  475  3anor  948  cadnot  1384  19.33b  1597  neorian  2535  indifdir  3427  fr2nr  4373  ordtri3or  4426  suc11  4498  xpeq0  5102  imadif  5329  difxp  6155  frxp  6227  soxp  6230  dfsup2  7197  suc11reg  7322  rankxplim3  7553  kmlem3  7780  cdainflem  7819  isfin5-2  8019  rpneg  10385  xrrebnd  10499  xmullem2  10587  difreicc  10769  firest  13339  xpcbas  13954  gsumdixp  15394  mplsubrglem  16185  ppttop  16746  fin1aufil  17629  mbfmax  19006  mdegleb  19452  coemulhi  19637  atcvati  22968  ballotlem2  23049  ballotlemodife  23058  erdszelem10  23733  mulge0b  24088  dfon2lem4  24144  nodenselem4  24340  itg2addnclem  24933  itg2addnclem2  24934  itg2addnc  24935  areacirclem5  24940  nelioo5  25522  stoweidlem14  27774  stoweidlem26  27786  notatnand  27875  fvfundmfvn0  27997  afvco2  28048  tpprceq3  28083  prneimg  28084  usgraedgprv  28133  usgraedgrnv  28134  nbusgra  28154  1to2vfriswmgra  28195  bnj1174  29106  lsatcvat  29313  lkreqN  29433  cvrat  29684  4atlem3  29858  paddasslem17  30098  llnexchb2  30131  dalawlem14  30146  cdleme0nex  30552  lclkrlem2o  31784  lcfrlem19  31824
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-or 359  df-an 360
  Copyright terms: Public domain W3C validator