Theorem ioran 981

Description: Negated disjunction in terms of conjunction (De Morgan's law). Compare Theorem *4.56 of [WhiteheadRussell] p. 120. (Contributed by NM, 3-Jan-1993.) (Proof shortened by Andrew Salmon, 7-May-2011.)

Assertion

Ref	Expression
ioran	⊢ (¬ (𝜑 ∨ 𝜓) ↔ (¬ 𝜑 ∧ ¬ 𝜓))

Proof of Theorem ioran

Step	Hyp	Ref	Expression
1		pm4.65 406	. 2 ⊢ (¬ (¬ 𝜑 → 𝜓) ↔ (¬ 𝜑 ∧ ¬ 𝜓))
2		pm4.64 846	. 2 ⊢ ((¬ 𝜑 → 𝜓) ↔ (𝜑 ∨ 𝜓))
3	1, 2	xchnxbi 331	1 ⊢ (¬ (𝜑 ∨ 𝜓) ↔ (¬ 𝜑 ∧ ¬ 𝜓))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 205   ∧ wa 396   ∨ 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 206  df-an 397  df-or 845

This theorem is referenced by:  pm4.56  986  xor  1012  3ioran  1105  3ori  1423  ecase23d  1472  19.43OLD  1885  2ralorOLD  3216  dfun2  4205  prnebg  4799  sotrieq2  5556  somo  5563  dflim3  7753  frxp  8026  poxp  8028  soxp  8029  suppofssd  8081  oalimcl  8454  omlimcl  8472  oeeulem  8495  fsetexb  8715  domunfican  9177  infsupprpr  9353  ordtypelem7  9373  cantnfp1lem2  9528  cantnfp1lem3  9529  cantnflem1  9538  cnfcom2lem  9550  ssfin4  10159  fin1a2lem7  10255  fin1a2lem12  10260  fpwwe2lem12  10491  fpwwe2  10492  r1wunlim  10586  1re  11068  recgt0  11914  elnnz  12422  xrltlen  12973  xaddf  13051  xmullem  13091  xmullem2  13092  ssfzoulel  13574  elfznelfzo  13585  elfznelfzob  13586  om2uzf1oi  13766  fsuppmapnn0fiubex  13805  bcval4  14114  sadcaddlem  16255  lcmcllem  16390  lcmgcdlem  16400  lcmftp  16430  lcmfunsnlem2lem1  16432  lcmfunsnlem2lem2  16433  lcmfunsnlem2  16434  isprm3  16477  prm23ge5  16605  pcpremul  16633  subgmulg  18857  isnirred  20029  isdomn2  20668  cnfldfun  20707  mdetunilem7  21865  mndifsplit  21883  ordtbaslem  22437  iunconn  22677  fbun  23089  fin1aufil  23181  reconnlem2  24088  rrxmvallem  24666  pmltpc  24712  itg2splitlem  25011  mdegmullem  25341  atans2  26179  leibpilem2  26189  leibpi  26190  wilthlem2  26316  lgsdir2  26576  2lgslem3  26650  nosepdmlem  26929  ragncol  27300  opptgdim2  27336  hlpasch  27347  trgcopy  27395  cgrg3col4  27444  structiedg0val  27622  usgredg2v  27824  nb3grprlem2  27978  vtxd0nedgb  28085  1egrvtxdg0  28108  wwlksnndef  28499  nfrgr2v  28865  nonbooli  30242  cvnbtwn4  30880  chirredi  30985  atcvat4i  30988  nelun  31088  hashxpe  31355  prmdvdsbc  31358  lindssn  31811  bnj1304  33039  bnj1417  33261  erdszelem9  33401  satf0n0  33580  fmlaomn0  33592  fmla0disjsuc  33600  fmlasucdisj  33601  3orit  33897  frxp2  34017  frxp3  34023  sltrec  34105  dfon3  34285  dfrdg4  34344  wl-df3maxtru1  35761  poimirlem18  35893  poimirlem21  35896  orsild  36344  orsird  36345  notornotel1  36351  cvrat4  37704  hdmaplem4  40035  mapdh9a  40050  metakunt12  40386  dffltz  40721  fnwe2lem2  41127  ifpnot23  41395  ifpim123g  41417  ontric3g  41439  df3or2  41686  3ornot23VD  42777  ndisj2  42908  xrssre  43211  icccncfext  43753  fourierdlem42  44015  fourierdlem92  44064  salexct2  44203  nnfoctbdjlem  44319  euoreqb  44941  afvfv0bi  44984  afv2fv0  45097  ltnltne  45131  prproropf1olem4  45298  lighneallem4  45402  oddprmALTV  45479  mndpsuppss  46047  2itscp  46467