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  2508  indifdir  3400  fr2nr  4343  ordtri3or  4396  suc11  4468  xpeq0  5088  imadif  5265  difxp  6087  frxp  6159  soxp  6162  dfsup2  7163  suc11reg  7288  rankxplim3  7519  kmlem3  7746  cdainflem  7785  isfin5-2  7985  rpneg  10351  xrrebnd  10465  xmullem2  10552  difreicc  10734  firest  13300  xpcbas  13915  gsumdixp  15355  mplsubrglem  16146  ppttop  16707  fin1aufil  17590  mbfmax  18967  mdegleb  19413  coemulhi  19598  atcvati  22927  ballotlem2  23009  ballotlemodife  23018  erdszelem10  23104  mulge0b  23458  dfon2lem4  23512  axdenselem4  23708  nelioo5  24879  stoweidlem14  27132  stoweidlem26  27144  notatnand  27213  bnj1174  28165  lsatcvat  28490  lkreqN  28610  cvrat  28861  4atlem3  29035  paddasslem17  29275  llnexchb2  29308  dalawlem14  29323  cdleme0nex  29729  lclkrlem2o  30961  lcfrlem19  31001
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