Theorem ioran 980

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 208   ∧ wa 398   ∨ wo 843

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 209  df-an 399  df-or 844

This theorem is referenced by:  pm4.56  985  xor  1011  3ioran  1102  3ori  1420  ecase23d  1469  noranOLD  1527  norassOLD  1534  19.43OLD  1884  2ralor  3371  dfun2  4238  prnebg  4788  sotrieq2  5505  somo  5512  dflim3  7564  frxp  7822  poxp  7824  soxp  7825  suppofssd  7869  oalimcl  8188  omlimcl  8206  oeeulem  8229  domunfican  8793  infsupprpr  8970  ordtypelem7  8990  cantnfp1lem2  9144  cantnfp1lem3  9145  cantnflem1  9154  cnfcom2lem  9166  ssfin4  9734  fin1a2lem7  9830  fin1a2lem12  9835  fpwwe2lem13  10066  fpwwe2  10067  r1wunlim  10161  1re  10643  recgt0  11488  elnnz  11994  xrltlen  12542  xaddf  12620  xmullem  12660  xmullem2  12661  ssfzoulel  13134  elfznelfzo  13145  elfznelfzob  13146  om2uzf1oi  13324  fsuppmapnn0fiubex  13363  bcval4  13670  sadcaddlem  15808  lcmcllem  15942  lcmgcdlem  15952  lcmftp  15982  lcmfunsnlem2lem1  15984  lcmfunsnlem2lem2  15985  lcmfunsnlem2  15986  isprm3  16029  prm23ge5  16154  pcpremul  16182  subgmulg  18295  isnirred  19452  isdomn2  20074  cnfldfunALT  20560  mdetunilem7  21229  mndifsplit  21247  ordtbaslem  21798  iunconn  22038  fbun  22450  fin1aufil  22542  reconnlem2  23437  rrxmvallem  24009  pmltpc  24053  itg2splitlem  24351  mdegmullem  24674  atans2  25511  leibpilem2  25521  leibpi  25522  wilthlem2  25648  lgsdir2  25908  2lgslem3  25982  ragncol  26497  opptgdim2  26533  hlpasch  26544  trgcopy  26592  cgrg3col4  26641  structiedg0val  26809  usgredg2v  27011  nb3grprlem2  27165  vtxd0nedgb  27272  1egrvtxdg0  27295  wwlksnndef  27685  wwlksnfiOLD  27687  nfrgr2v  28053  nonbooli  29430  cvnbtwn4  30068  chirredi  30173  atcvat4i  30176  nelun  30276  hashxpe  30531  prmdvdsbc  30534  lindssn  30941  bnj1304  32093  bnj1417  32315  erdszelem9  32448  satf0n0  32627  fmlaomn0  32639  fmla0disjsuc  32647  fmlasucdisj  32648  3orit  32947  nosepdmlem  33189  sltrec  33280  dfon3  33355  dfrdg4  33414  poimirlem18  34912  poimirlem21  34915  orsild  35368  orsird  35369  notornotel1  35375  cvrat4  36581  hdmaplem4  38912  mapdh9a  38927  dffltz  39278  fnwe2lem2  39658  ifpnot23  39851  ifpim123g  39873  ontric3g  39895  df3or2  40120  3ornot23VD  41188  ndisj2  41320  xrssre  41623  icccncfext  42177  fourierdlem42  42441  fourierdlem92  42490  salexct2  42629  nnfoctbdjlem  42744  euoreqb  43315  afvfv0bi  43358  afv2fv0  43471  ltnltne  43506  prproropf1olem4  43675  lighneallem4  43782  oddprmALTV  43859  mndpsuppss  44426  2itscp  44775