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

Theorem ianor 476
Description: Negated conjunction in terms of disjunction (DeMorgan'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 413 . 2  |-  ( (
ph  ->  -.  ps )  <->  -.  ( ph  /\  ps ) )
2 pm4.62 410 . 2  |-  ( (
ph  ->  -.  ps )  <->  ( -.  ph  \/  -.  ps ) )
31, 2bitr3i 244 1  |-  ( -.  ( ph  /\  ps ) 
<->  ( -.  ph  \/  -.  ps ) )
Colors of variables: wff set class
Syntax hints:   -. wn 5    -> wi 6    <-> wb 178    \/ wo 359    /\ wa 360
This theorem is referenced by:  anor  477  3anor  953  cadnot  1390  19.33b  1607  neorian  2499  indifdir  3332  fr2nr  4264  ordtri3or  4317  suc11  4387  xpeq0  5007  imadif  5184  difxp  6005  frxp  6077  soxp  6080  dfsup2  7079  suc11reg  7204  rankxplim3  7435  kmlem3  7662  cdainflem  7701  isfin5-2  7901  rpneg  10262  xrrebnd  10376  xmullem2  10463  difreicc  10645  firest  13211  xpcbas  13796  gsumdixp  15227  mplsubrglem  16015  ppttop  16576  fin1aufil  17459  mbfmax  18836  mdegleb  19282  coemulhi  19467  atcvati  22796  erdszelem10  22902  mulge0b  23256  dfon2lem4  23310  axdenselem4  23506  nelioo5  24677  bnj1174  27722  lsatcvat  27929  lkreqN  28049  cvrat  28300  4atlem3  28474  paddasslem17  28714  llnexchb2  28747  dalawlem14  28762  cdleme0nex  29168  lclkrlem2o  30400  lcfrlem19  30440
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362
  Copyright terms: Public domain W3C validator