Theorem ianor 509

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

Step	Hyp	Ref	Expression
1		imnan 438	. 2 |- ( ( ph -> -. ps ) <-> -. ( ph /\ ps ) )
2		pm4.62 435	. 2 |- ( ( ph -> -. ps ) <-> ( -. ph \/ -. ps ) )
3	1, 2	bitr3i 266	1 |- ( -. ( ph /\ ps ) <-> ( -. ph \/ -. ps ) )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 196   \/ wo 383   /\ wa 384

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 197  df-or 385  df-an 386

This theorem is referenced by:  anor  510  3anor  1054  cadnot  1554  19.33b  1813  neorian  2888  indifdir  3883  tpprceq3  4335  tppreqb  4336  prneimg  4388  prnebg  4389  opthneg  4950  fr2nr  5092  xpeq0  5554  difxp  5558  ordtri3or  5755  imadif  5973  fvfundmfvn0  6226  ftpg  6423  2mpt20  6882  bropopvvv  7255  bropfvvvv  7257  frxp  7287  soxp  7290  ressuppssdif  7316  mpt2xneldm  7338  dfsup2  8350  suc11reg  8516  rankxplim3  8744  kmlem3  8974  cdainflem  9013  isfin5-2  9213  mulge0b  10893  nn0n0n1ge2b  11359  rpneg  11863  mul2lt0bi  11936  xrrebnd  11999  xnn0xaddcl  12066  xmullem2  12095  difreicc  12304  fz0  12356  nelfzo  12475  injresinj  12589  hashunx  13175  swrdnd  13432  repswswrd  13531  dfgcd2  15263  ncoprmlnprm  15436  firest  16093  xpcbas  16818  symgfix2  17836  gsumdixp  18609  0ringnnzr  19269  mplsubrglem  19439  symgmatr01lem  20459  ppttop  20811  fin1aufil  21736  zclmncvs  22948  mbfmax  23416  mdegleb  23824  coemulhi  24010  numedglnl  26039  usgredg2v  26119  clwwlknclwwlkdifs  26873  trlsegvdeg  27087  1to2vfriswmgr  27143  numclwwlk3lem  27241  atcvati  29245  difrab2  29339  ofpreima2  29466  ordtconnlem1  29970  aean  30307  sitgaddlemb  30410  ballotlemodife  30559  bnj1174  31071  erdszelem10  31182  dfon2lem4  31691  noetalem3  31865  poimirlem30  33439  poimirlem31  33440  itg2addnclem  33461  itg2addnclem2  33462  itg2addnclem3  33463  iblabsnclem  33473  ftc1anclem3  33487  areacirclem4  33503  lsatcvat  34337  lkreqN  34457  cvrat  34708  4atlem3  34882  paddasslem17  35122  llnexchb2  35155  dalawlem14  35170  cdleme0nex  35577  lclkrlem2o  36810  lcfrlem19  36850  ifpnot23  37823  ifpim123g  37845  rp-fakenanass  37860  ntrneineine1lem  38382  stoweidlem14  40231  stoweidlem26  40243  afvco2  41256  nltle2tri  41323  evennodd  41556  oddneven  41557  spr0nelg  41726  lindslinindsimp1  42246  lindslinindsimp2  42252