Theorem ianor 983

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395   ∨ wo 847

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 207  df-an 396  df-or 848

This theorem is referenced by:  anor  984  3ianor  1106  nanor  1496  cadnot  1616  19.33b  1886  neorian  3023  2nreu  4389  tpprceq3  4751  tppreqb  4752  prneimg  4801  prneimg2  4802  prnebg  4803  preq12nebg  4810  opthprneg  4812  opthneg  5416  fr2nr  5588  iresn0n0  5998  xpeq0  6102  difxp  6106  ordtri3or  6333  imadif  6560  ftpg  7084  nf1const  7233  nf1oconst  7234  0mpo0  7424  2mpo0  7590  bropopvvv  8015  bropfvvvv  8017  frxp  8051  soxp  8054  ressuppssdif  8110  mpoxneldm  8137  naddcllem  8586  dfsup2  9323  nelaneqOLD  9483  suc11reg  9504  rankxplim3  9769  kmlem3  10039  cdainflem  10074  isfin5-2  10277  mulge0b  11987  nn0n0n1ge2b  12445  rpneg  12919  mul2lt0bi  12993  xrrebnd  13062  xnn0xaddcl  13129  xmullem2  13159  difreicc  13379  fz0  13434  nelfzo  13559  injresinj  13686  hashunx  14288  swrdnd  14557  swrdnnn0nd  14559  swrdnd0  14560  repswswrd  14686  dfgcd2  16452  ncoprmlnprm  16634  firest  17331  xpcbas  18079  smndex2dnrinv  18818  symgfix2  19323  gsumdixp  20232  0ringnnzr  20435  mplsubrglem  21936  symgmatr01lem  22563  ppttop  22917  fin1aufil  23842  zclmncvs  25070  mbfmax  25572  mdegleb  25991  coemulhi  26181  noetasuplem4  27670  noetainflem4  27674  sltlpss  27848  numedglnl  29117  usgredg2v  29200  clwwlkn  29998  clwwlkneq0  30001  clwwlknon1nloop  30071  trlsegvdeg  30199  1to2vfriswmgr  30251  numclwwlk3lem2  30356  atcvati  32358  difrab2  32469  ofpreima2  32640  hashxpe  32781  fldextrspunlsplem  33678  ordtconnlem1  33929  aean  34249  sitgaddlemb  34353  ballotlemodife  34503  bnj1174  35007  erdszelem10  35236  satfv1  35399  fmla0disjsuc  35434  fmlasucdisj  35435  dfon2lem4  35820  nrmo  36444  poimirlem30  37690  poimirlem31  37691  itg2addnclem  37711  itg2addnclem2  37712  itg2addnclem3  37713  iblabsnclem  37723  ftc1anclem3  37735  areacirclem4  37751  lsatcvat  39089  lkreqN  39209  cvrat  39461  4atlem3  39635  paddasslem17  39875  llnexchb2  39908  dalawlem14  39923  cdleme0nex  40329  lclkrlem2o  41560  lcfrlem19  41600  dvrelog2b  42099  aks4d1p7  42116  aks6d1c2p2  42152  aks6d1c5  42172  sticksstones1  42179  aks6d1c6lem3  42205  ifpnot23  43511  ifpim123g  43533  sqrtcvallem1  43664  ntrneineine1lem  44117  mnringmulrcld  44261  stoweidlem14  46052  stoweidlem26  46064  dfatprc  47161  afvco2  47207  ndmafv2nrn  47253  nfunsnafv2  47256  afv2ndeffv0  47291  nltle2tri  47344  ichnreuop  47503  spr0nelg  47507  evennodd  47674  oddneven  47675  usgrexmpl2trifr  48068  pg4cyclnex  48158  lindslinindsimp1  48489  lindslinindsimp2  48495  line2ylem  48783  line2xlem  48785