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  949  cadnot  1399  19.33b  1613  neorian  2616  indifdir  3513  tpprceq3  3853  tppreqb  3854  prneimg  3892  prnebg  3893  fr2nr  4474  ordtri3or  4527  suc11  4599  xpeq0  5203  imadif  5432  ftpg  5817  difxp  6280  bropopvvv  6326  frxp  6353  soxp  6356  dfsup2  7342  suc11reg  7467  rankxplim3  7698  kmlem3  7925  cdainflem  7964  isfin5-2  8164  nn0n0n1ge2b  10174  rpneg  10534  xrrebnd  10649  xmullem2  10737  difreicc  10920  injresinj  11087  hashunx  11547  firest  13547  xpcbas  14162  gsumdixp  15602  mplsubrglem  16393  ppttop  16961  fin1aufil  17840  mbfmax  19219  mdegleb  19665  coemulhi  19850  usgraedgprv  21074  usgraedgrnv  21075  usgraidx2v  21089  atcvati  23279  aean  24058  ballotlem2  24194  ballotlemodife  24203  erdszelem10  24334  mulge0b  24675  dfon2lem4  24883  nodenselem4  25079  itg2addnclem  25675  itg2addnclem2  25676  itg2addnc  25677  iblabsnclem  25686  areacirclem5  25704  stoweidlem14  27269  stoweidlem26  27281  notatnand  27370  fvfundmfvn0  27494  afvco2  27547  nbusgra  27596  cusgrares  27637  cusgrasizeindslem2  27639  2pthonlem2  27738  vdgref  27807  1to2vfriswmgra  27841  frgrawopreglem3  27881  bnj1174  28797  lsatcvat  29311  lkreqN  29431  cvrat  29682  4atlem3  29856  paddasslem17  30096  llnexchb2  30129  dalawlem14  30144  cdleme0nex  30550  lclkrlem2o  31782  lcfrlem19  31822
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