Theorem ianor 508

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 195   ∨ wo 382   ∧ wa 383

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 196  df-or 384  df-an 385

This theorem is referenced by:  anor  509  3anor  1047  cadnot  1545  19.33b  1802  neorian  2876  indifdir  3842  tpprceq3  4276  tppreqb  4277  prneimg  4328  prnebg  4329  opthneg  4876  fr2nr  5016  xpeq0  5473  difxp  5477  ordtri3or  5672  imadif  5887  fvfundmfvn0  6136  ftpg  6328  2mpt20  6780  bropopvvv  7142  bropfvvvv  7144  frxp  7174  soxp  7177  ressuppssdif  7203  mpt2xneldm  7225  dfsup2  8233  suc11reg  8399  rankxplim3  8627  kmlem3  8857  cdainflem  8896  isfin5-2  9096  mulge0b  10772  nn0n0n1ge2b  11236  rpneg  11739  mul2lt0bi  11812  xrrebnd  11873  xnn0xaddcl  11940  xmullem2  11967  difreicc  12175  fz0  12227  nelfzo  12344  injresinj  12451  hashunx  13036  swrdnd  13284  repswswrd  13382  dfgcd2  15101  ncoprmlnprm  15274  firest  15916  xpcbas  16641  symgfix2  17659  gsumdixp  18432  0ringnnzr  19090  mplsubrglem  19260  symgmatr01lem  20278  ppttop  20621  fin1aufil  21546  zclmncvs  22756  mbfmax  23222  mdegleb  23628  coemulhi  23814  usgraedgprv  25905  usgraedgrnv  25906  usgraidx2v  25922  cusgrares  26001  cusgrasizeindslem1  26002  2pthlem2  26126  clwwlknprop  26300  2wlkonot3v  26402  2spthonot3v  26403  vdgrf  26425  clwlknclwlkdifs  26487  1to2vfriswmgra  26533  frgrawopreglem3  26573  2spotiundisj  26589  numclwwlk3lem  26635  atcvati  28629  ofpreima2  28849  ordtconlem1  29298  aean  29634  sitgaddlemb  29737  ballotlemodife  29886  bnj1174  30325  erdszelem10  30436  dfon2lem4  30935  nodenselem4  31083  poimirlem30  32609  poimirlem31  32610  itg2addnclem  32631  itg2addnclem2  32632  itg2addnclem3  32633  iblabsnclem  32643  ftc1anclem3  32657  areacirclem4  32673  lsatcvat  33355  lkreqN  33475  cvrat  33726  4atlem3  33900  paddasslem17  34140  llnexchb2  34173  dalawlem14  34188  cdleme0nex  34595  lclkrlem2o  35828  lcfrlem19  35868  ifpnot23  36842  ifpim123g  36864  rp-fakenanass  36879  ntrneineine1lem  37402  stoweidlem14  38907  stoweidlem26  38919  afvco2  39905  nltle2tri  39942  evennodd  40094  oddneven  40095  usgredg2v  40454  clwwlknclwwlkdifs  41181  trlsegvdeg  41395  1to2vfriswmgr  41449  frgrwopreglem3  41483  av-numclwwlk3lem  41538  lindslinindsimp1  42040  lindslinindsimp2  42046