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  2506  indifdir  3367  fr2nr  4308  ordtri3or  4361  suc11  4433  xpeq0  5053  imadif  5230  difxp  6052  frxp  6124  soxp  6127  dfsup2  7128  suc11reg  7253  rankxplim3  7484  kmlem3  7711  cdainflem  7750  isfin5-2  7950  rpneg  10315  xrrebnd  10429  xmullem2  10516  difreicc  10698  firest  13264  xpcbas  13879  gsumdixp  15319  mplsubrglem  16110  ppttop  16671  fin1aufil  17554  mbfmax  18931  mdegleb  19377  coemulhi  19562  atcvati  22891  ballotlem2  22973  ballotlemodife  22982  erdszelem10  23068  mulge0b  23422  dfon2lem4  23476  axdenselem4  23672  nelioo5  24843  stoweidlem14  27063  stoweidlem26  27075  notatnand  27118  bnj1174  28045  lsatcvat  28370  lkreqN  28490  cvrat  28741  4atlem3  28915  paddasslem17  29155  llnexchb2  29188  dalawlem14  29203  cdleme0nex  29609  lclkrlem2o  30841  lcfrlem19  30881
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