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

Proof of Theorem ianor

Step	Hyp	Ref	Expression
1		imnan 422	. 2
2		pm4.62 419	. 2
3	1, 2	bitr3i 251	1

Syntax hints:  -.wn 3  ->wi 4  <->wb 184  \/wo 368  /\wa 369

This theorem is referenced by:  anor  489  3anor  989  cadnot  1461  stoic1a  1605  19.33b  1696  neorian  2784  indifdir  3753  tpprceq3  4170  tppreqb  4171  prneimg  4211  prnebg  4212  opthneg  4731  fr2nr  4862  ordtri3or  4915  suc11  4986  xpeq0  5432  difxp  5436  imadif  5668  fvfundmfvn0  5903  ftpg  6081  bropopvvv  6880  frxp  6910  soxp  6913  ressuppssdif  6940  dfsup2  7922  suc11reg  8057  rankxplim3  8320  kmlem3  8553  cdainflem  8592  isfin5-2  8792  mulge0b  10437  nn0n0n1ge2b  10885  rpneg  11278  xrrebnd  11398  xmullem2  11486  difreicc  11681  fz0  11730  injresinj  11926  hashunx  12454  wrdsymb0  12575  repswswrd  12756  firest  14830  xpcbas  15447  symgfix2  16441  gsumdixpOLD  17257  gsumdixp  17258  0ringnnzr  17917  mplsubrglem  18100  mplsubrglemOLD  18101  symgmatr01lem  19155  ppttop  19508  fin1aufil  20433  mbfmax  22056  mdegleb  22464  coemulhi  22651  usgraedgprv  24376  usgraedgrnv  24377  usgraidx2v  24393  cusgrares  24472  cusgrasizeindslem2  24474  2pthlem2  24598  clwwlknprop  24772  2wlkonot3v  24875  2spthonot3v  24876  vdgrf  24898  clwlknclwlkdifs  24960  1to2vfriswmgra  25006  frgrawopreglem3  25046  2spotiundisj  25062  numclwwlk3lem  25108  atcvati  27305  ofpreima2  27508  mul2lt0bi  27569  ordtconlem1  27906  aean  28216  ballotlemodife  28436  erdszelem10  28644  dfon2lem4  29218  nodenselem4  29444  dvtanlem  30064  itg2addnclem  30066  itg2addnclem2  30067  itg2addnclem3  30068  iblabsnclem  30078  ftc1anclem3  30092  areacirclem4  30110  stoweidlem14  31796  stoweidlem26  31808  afvco2  32261  usgedgvadf1  32415  usgedgvadf1ALT  32418  lindslinindsimp1  33058  lindslinindsimp2  33064  bnj1174  34059  lsatcvat  34775  lkreqN  34895  cvrat  35146  4atlem3  35320  paddasslem17  35560  llnexchb2  35593  dalawlem14  35608  cdleme0nex  36015  lclkrlem2o  37248  lcfrlem19  37288  bj-ifim123g  37706  bj-ifnot23  37718  rp-fakenanass  37739

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