Theorem ianor 979

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 403	. 2 ⊢ ((𝜑 → ¬ 𝜓) ↔ ¬ (𝜑 ∧ 𝜓))
2		pm4.62 853	. 2 ⊢ ((𝜑 → ¬ 𝜓) ↔ (¬ 𝜑 ∨ ¬ 𝜓))
3	1, 2	bitr3i 280	1 ⊢ (¬ (𝜑 ∧ 𝜓) ↔ (¬ 𝜑 ∨ ¬ 𝜓))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 399   ∨ wo 844

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 210  df-an 400  df-or 845

This theorem is referenced by:  anor  980  3ianor  1104  nanor  1486  noranOLD  1528  cadnot  1617  19.33b  1886  neorian  3081  indifdir  4210  2nreu  4349  tpprceq3  4697  tppreqb  4698  prneimg  4745  prnebg  4746  preq12nebg  4753  opthprneg  4755  opthneg  5338  fr2nr  5497  iresn0n0  5890  xpeq0  5984  difxp  5988  ordtri3or  6191  imadif  6408  ftpg  6895  nf1const  7038  nf1oconst  7039  0mpo0  7216  2mpo0  7374  bropopvvv  7768  bropfvvvv  7770  frxp  7803  soxp  7806  ressuppssdif  7834  mpoxneldm  7861  dfsup2  8892  nelaneq  9047  suc11reg  9066  rankxplim3  9294  kmlem3  9563  cdainflem  9598  isfin5-2  9802  mulge0b  11499  nn0n0n1ge2b  11951  rpneg  12409  mul2lt0bi  12483  xrrebnd  12549  xnn0xaddcl  12616  xmullem2  12646  difreicc  12862  fz0  12917  nelfzo  13038  injresinj  13153  hashunx  13743  swrdnd  14007  swrdnnn0nd  14009  swrdnd0  14010  repswswrd  14137  dfgcd2  15884  ncoprmlnprm  16058  firest  16698  xpcbas  17420  smndex2dnrinv  18072  symgfix2  18536  gsumdixp  19355  0ringnnzr  20035  mplsubrglem  20677  symgmatr01lem  21258  ppttop  21612  fin1aufil  22537  zclmncvs  23753  mbfmax  24253  mdegleb  24665  coemulhi  24851  numedglnl  26937  usgredg2v  27017  clwwlkn  27811  clwwlkneq0  27814  clwwlknon1nloop  27884  trlsegvdeg  28012  1to2vfriswmgr  28064  numclwwlk3lem2  28169  atcvati  30169  difrab2  30268  ofpreima2  30429  hashxpe  30555  ordtconnlem1  31277  aean  31613  sitgaddlemb  31716  ballotlemodife  31865  bnj1174  32385  erdszelem10  32560  satfv1  32723  fmla0disjsuc  32758  fmlasucdisj  32759  dfon2lem4  33144  noetalem3  33332  nrmo  33871  poimirlem30  35087  poimirlem31  35088  itg2addnclem  35108  itg2addnclem2  35109  itg2addnclem3  35110  iblabsnclem  35120  ftc1anclem3  35132  areacirclem4  35148  lsatcvat  36346  lkreqN  36466  cvrat  36718  4atlem3  36892  paddasslem17  37132  llnexchb2  37165  dalawlem14  37180  cdleme0nex  37586  lclkrlem2o  38817  lcfrlem19  38857  ifpnot23  40186  ifpim123g  40208  sqrtcvallem1  40331  ntrneineine1lem  40787  mnringmulrcld  40936  stoweidlem14  42656  stoweidlem26  42668  dfatprc  43686  afvco2  43732  ndmafv2nrn  43778  nfunsnafv2  43781  afv2ndeffv0  43816  nltle2tri  43870  ichnreuop  43989  spr0nelg  43993  evennodd  44161  oddneven  44162  lindslinindsimp1  44866  lindslinindsimp2  44872  line2ylem  45165  line2xlem  45167