MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ianor Unicode version

Theorem ianor 475
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 412 . 2  |-  ( (
ph  ->  -.  ps )  <->  -.  ( ph  /\  ps ) )
2 pm4.62 409 . 2  |-  ( (
ph  ->  -.  ps )  <->  ( -.  ph  \/  -.  ps ) )
31, 2bitr3i 243 1  |-  ( -.  ( ph  /\  ps ) 
<->  ( -.  ph  \/  -.  ps ) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 177    \/ wo 358    /\ wa 359
This theorem is referenced by:  anor  476  3anor  950  cadnot  1400  19.33b  1615  neorian  2654  indifdir  3557  tpprceq3  3898  tppreqb  3899  prneimg  3938  prnebg  3939  fr2nr  4520  ordtri3or  4573  suc11  4644  xpeq0  5252  imadif  5487  fvfundmfvn0  5721  ftpg  5875  difxp  6339  bropopvvv  6385  frxp  6415  soxp  6418  dfsup2  7405  suc11reg  7530  rankxplim3  7761  kmlem3  7988  cdainflem  8027  isfin5-2  8227  nn0n0n1ge2b  10237  rpneg  10597  xrrebnd  10712  xmullem2  10800  difreicc  10984  injresinj  11155  hashunx  11615  firest  13615  xpcbas  14230  gsumdixp  15670  mplsubrglem  16457  ppttop  17026  fin1aufil  17917  mbfmax  19494  mdegleb  19940  coemulhi  20125  usgraedgprv  21349  usgraedgrnv  21350  usgraidx2v  21365  cusgrares  21434  cusgrasizeindslem2  21436  2pthlem2  21549  vdgrf  21622  atcvati  23842  aean  24548  sibfof  24607  ballotlemodife  24708  erdszelem10  24839  mulge0b  25144  dfon2lem4  25356  nodenselem4  25552  itg2addnclem  26155  itg2addnclem2  26156  itg2addnclem3  26157  iblabsnclem  26167  areacirclem5  26185  stoweidlem14  27630  stoweidlem26  27642  afvco2  27907  2wlkonot3v  28072  2spthonot3v  28073  1to2vfriswmgra  28110  frgrawopreglem3  28149  2spotiundisj  28165  bnj1174  29078  lsatcvat  29533  lkreqN  29653  cvrat  29904  4atlem3  30078  paddasslem17  30318  llnexchb2  30351  dalawlem14  30366  cdleme0nex  30772  lclkrlem2o  32004  lcfrlem19  32044
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 178  df-or 360  df-an 361
  Copyright terms: Public domain W3C validator