Theorem ioran 982

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 410	. 2 ⊢ (¬ (¬ 𝜑 → 𝜓) ↔ (¬ 𝜑 ∧ ¬ 𝜓))
2		pm4.64 847	. 2 ⊢ ((¬ 𝜑 → 𝜓) ↔ (𝜑 ∨ 𝜓))
3	1, 2	xchnxbi 336	1 ⊢ (¬ (𝜑 ∨ 𝜓) ↔ (¬ 𝜑 ∧ ¬ 𝜓))

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

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 401  df-or 846

This theorem is referenced by:  pm4.56  987  xor  1013  3ioran  1104  3ori  1422  ecase23d  1471  noranOLD  1529  norassOLD  1536  19.43OLD  1885  2ralor  3288  dfun2  4165  prnebg  4744  sotrieq2  5473  somo  5480  dflim3  7562  frxp  7826  poxp  7828  soxp  7829  suppofssd  7878  oalimcl  8197  omlimcl  8215  oeeulem  8238  domunfican  8817  infsupprpr  8994  ordtypelem7  9014  cantnfp1lem2  9168  cantnfp1lem3  9169  cantnflem1  9178  cnfcom2lem  9190  ssfin4  9763  fin1a2lem7  9859  fin1a2lem12  9864  fpwwe2lem12  10095  fpwwe2  10096  r1wunlim  10190  1re  10672  recgt0  11517  elnnz  12023  xrltlen  12573  xaddf  12651  xmullem  12691  xmullem2  12692  ssfzoulel  13173  elfznelfzo  13184  elfznelfzob  13185  om2uzf1oi  13363  fsuppmapnn0fiubex  13402  bcval4  13710  sadcaddlem  15849  lcmcllem  15985  lcmgcdlem  15995  lcmftp  16025  lcmfunsnlem2lem1  16027  lcmfunsnlem2lem2  16028  lcmfunsnlem2  16029  isprm3  16072  prm23ge5  16200  pcpremul  16228  subgmulg  18353  isnirred  19514  isdomn2  20133  cnfldfunALT  20172  mdetunilem7  21311  mndifsplit  21329  ordtbaslem  21881  iunconn  22121  fbun  22533  fin1aufil  22625  reconnlem2  23521  rrxmvallem  24097  pmltpc  24143  itg2splitlem  24441  mdegmullem  24771  atans2  25609  leibpilem2  25619  leibpi  25620  wilthlem2  25746  lgsdir2  26006  2lgslem3  26080  ragncol  26595  opptgdim2  26631  hlpasch  26642  trgcopy  26690  cgrg3col4  26739  structiedg0val  26907  usgredg2v  27109  nb3grprlem2  27263  vtxd0nedgb  27370  1egrvtxdg0  27393  wwlksnndef  27783  nfrgr2v  28149  nonbooli  29526  cvnbtwn4  30164  chirredi  30269  atcvat4i  30272  nelun  30374  hashxpe  30644  prmdvdsbc  30647  lindssn  31087  bnj1304  32312  bnj1417  32534  erdszelem9  32670  satf0n0  32849  fmlaomn0  32861  fmla0disjsuc  32869  fmlasucdisj  32870  3orit  33169  frxp2  33339  frxp3  33345  nosepdmlem  33444  sltrec  33568  no3indslem  33655  dfon3  33736  dfrdg4  33795  wl-df3maxtru1  35182  poimirlem18  35348  poimirlem21  35351  orsild  35799  orsird  35800  notornotel1  35806  cvrat4  37012  hdmaplem4  39343  mapdh9a  39358  metakunt12  39651  dffltz  39956  fnwe2lem2  40361  ifpnot23  40552  ifpim123g  40574  ontric3g  40596  df3or2  40835  3ornot23VD  41919  ndisj2  42051  xrssre  42341  icccncfext  42888  fourierdlem42  43150  fourierdlem92  43199  salexct2  43338  nnfoctbdjlem  43453  euoreqb  44026  afvfv0bi  44069  afv2fv0  44182  ltnltne  44217  prproropf1olem4  44384  lighneallem4  44488  oddprmALTV  44565  mndpsuppss  45133  2itscp  45553