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  2534  indifdir  3426  fr2nr  4370  ordtri3or  4423  suc11  4495  xpeq0  5099  imadif  5293  difxp  6115  frxp  6187  soxp  6190  dfsup2  7191  suc11reg  7316  rankxplim3  7547  kmlem3  7774  cdainflem  7813  isfin5-2  8013  rpneg  10379  xrrebnd  10493  xmullem2  10581  difreicc  10763  firest  13333  xpcbas  13948  gsumdixp  15388  mplsubrglem  16179  ppttop  16740  fin1aufil  17623  mbfmax  19000  mdegleb  19446  coemulhi  19631  atcvati  22962  ballotlem2  23043  ballotlemodife  23052  erdszelem10  23138  mulge0b  23492  dfon2lem4  23546  axdenselem4  23742  areacirclem5  24339  nelioo5  24922  stoweidlem14  27174  stoweidlem26  27186  notatnand  27255  fvfundmfvn0  27377  afvco2  27428  bnj1174  28312  lsatcvat  28519  lkreqN  28639  cvrat  28890  4atlem3  29064  paddasslem17  29304  llnexchb2  29337  dalawlem14  29352  cdleme0nex  29758  lclkrlem2o  30990  lcfrlem19  31030
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