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 (De Morgan'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  1394  19.33b  1608  neorian  2608  indifdir  3501  fr2nr  4453  ordtri3or  4506  suc11  4578  xpeq0  5182  imadif  5409  difxp  6240  frxp  6312  soxp  6315  dfsup2  7285  suc11reg  7410  rankxplim3  7641  kmlem3  7868  cdainflem  7907  isfin5-2  8107  rpneg  10475  xrrebnd  10589  xmullem2  10677  difreicc  10859  firest  13436  xpcbas  14051  gsumdixp  15491  mplsubrglem  16282  ppttop  16850  fin1aufil  17729  mbfmax  19108  mdegleb  19554  coemulhi  19739  atcvati  23080  aean  23859  ballotlem2  23995  ballotlemodife  24004  erdszelem10  24135  mulge0b  24492  dfon2lem4  24700  nodenselem4  24896  itg2addnclem  25492  itg2addnclem2  25493  itg2addnc  25494  iblabsnclem  25503  areacirclem5  25521  stoweidlem14  27086  stoweidlem26  27098  notatnand  27187  fvfundmfvn0  27311  afvco2  27364  tpprceq3  27407  tppreqb  27408  prneimg  27409  prnebg  27410  ftpg  27417  bropopvvv  27435  nn0n0n1ge2b  27453  injresinj  27465  hashunx  27487  usgraedgprv  27551  usgraedgrnv  27552  usgraidx2v  27566  nbusgra  27594  cusgrares  27635  cusgrasizeindslem2  27637  2pthonlem2  27736  vdgref  27805  1to2vfriswmgra  27839  frgrawopreglem3  27879  bnj1174  28795  lsatcvat  29309  lkreqN  29429  cvrat  29680  4atlem3  29854  paddasslem17  30094  llnexchb2  30127  dalawlem14  30142  cdleme0nex  30548  lclkrlem2o  31780  lcfrlem19  31820
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