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

Theorem ianor 488
Description: Negated conjunction in terms of disjunction (De Morgan's law). Theorem *4.51 of [WhiteheadRussell] p. 120. (Contributed by NM, 14-May-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 422 . 2  |-  ( (
ph  ->  -.  ps )  <->  -.  ( ph  /\  ps ) )
2 pm4.62 419 . 2  |-  ( (
ph  ->  -.  ps )  <->  ( -.  ph  \/  -.  ps ) )
31, 2bitr3i 251 1  |-  ( -.  ( ph  /\  ps ) 
<->  ( -.  ph  \/  -.  ps ) )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 184    \/ wo 368    /\ wa 369
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371
This theorem is referenced by:  anor  489  3anor  981  cadnot  1436  thema1a  1579  19.33b  1663  neorian  2694  indifdir  3601  tpprceq3  4008  tppreqb  4009  prneimg  4048  prnebg  4049  opthneg  4566  fr2nr  4693  ordtri3or  4746  suc11  4817  xpeq0  5253  difxp  5257  imadif  5488  fvfundmfvn0  5717  ftpg  5887  bropopvvv  6648  frxp  6677  soxp  6680  ressuppssdif  6705  dfsup2  7684  suc11reg  7817  rankxplim3  8080  kmlem3  8313  cdainflem  8352  isfin5-2  8552  mulge0b  10191  nn0n0n1ge2b  10636  rpneg  11012  xrrebnd  11132  xmullem2  11220  difreicc  11409  fz0  11457  injresinj  11631  hashunx  12141  wrdsymb0  12251  repswswrd  12414  firest  14363  xpcbas  14980  symgfix2  15912  gsumdixpOLD  16688  gsumdixp  16689  mplsubrglem  17494  mplsubrglemOLD  17495  symgmatr01lem  18434  ppttop  18586  fin1aufil  19480  mbfmax  21102  mdegleb  21510  coemulhi  21696  usgraedgprv  23246  usgraedgrnv  23247  usgraidx2v  23262  cusgrares  23331  cusgrasizeindslem2  23333  2pthlem2  23446  vdgrf  23519  atcvati  25741  ofpreima2  25936  mul2lt0bi  25993  ordtconlem1  26306  aean  26612  ballotlemodife  26832  erdszelem10  27040  dfon2lem4  27550  nodenselem4  27776  dvtanlem  28394  itg2addnclem  28396  itg2addnclem2  28397  itg2addnclem3  28398  iblabsnclem  28408  ftc1anclem3  28422  areacirclem4  28440  stoweidlem14  29762  stoweidlem26  29774  afvco2  30035  2wlkonot3v  30347  2spthonot3v  30348  clwwlknprop  30388  clwlknclwlkdifs  30531  1to2vfriswmgra  30551  frgrawopreglem3  30592  2spotiundisj  30608  numclwwlk3lem  30654  0rngnnzr  30729  lindslinindsimp1  30880  lindslinindsimp2  30886  bnj1174  31881  lsatcvat  32535  lkreqN  32655  cvrat  32906  4atlem3  33080  paddasslem17  33320  llnexchb2  33353  dalawlem14  33368  cdleme0nex  33774  lclkrlem2o  35006  lcfrlem19  35046
  Copyright terms: Public domain W3C validator