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 (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 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  1595  neorian  2533  indifdir  3425  fr2nr  4371  ordtri3or  4424  suc11  4496  xpeq0  5100  imadif  5327  difxp  6153  frxp  6225  soxp  6228  dfsup2  7195  suc11reg  7320  rankxplim3  7551  kmlem3  7778  cdainflem  7817  isfin5-2  8017  rpneg  10383  xrrebnd  10497  xmullem2  10585  difreicc  10767  firest  13337  xpcbas  13952  gsumdixp  15392  mplsubrglem  16183  ppttop  16744  fin1aufil  17627  mbfmax  19004  mdegleb  19450  coemulhi  19635  atcvati  22966  ballotlem2  23047  ballotlemodife  23056  erdszelem10  23731  mulge0b  24086  dfon2lem4  24142  nodenselem4  24338  areacirclem5  24929  nelioo5  25511  stoweidlem14  27763  stoweidlem26  27775  notatnand  27864  fvfundmfvn0  27986  afvco2  28037  tpprceq3  28072  prneimg  28073  usgraedgprv  28122  usgraedgrnv  28123  nbusgra  28143  1to2vfriswmgra  28184  bnj1174  29033  lsatcvat  29240  lkreqN  29360  cvrat  29611  4atlem3  29785  paddasslem17  30025  llnexchb2  30058  dalawlem14  30073  cdleme0nex  30479  lclkrlem2o  31711  lcfrlem19  31751
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