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 332	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  norassOLD  1536  19.43OLD  1886  2ralorOLD  3297  dfun2  4193  prnebg  4786  sotrieq2  5533  somo  5540  dflim3  7694  frxp  7967  poxp  7969  soxp  7970  suppofssd  8019  oalimcl  8391  omlimcl  8409  oeeulem  8432  fsetexb  8652  domunfican  9087  infsupprpr  9263  ordtypelem7  9283  cantnfp1lem2  9437  cantnfp1lem3  9438  cantnflem1  9447  cnfcom2lem  9459  ssfin4  10066  fin1a2lem7  10162  fin1a2lem12  10167  fpwwe2lem12  10398  fpwwe2  10399  r1wunlim  10493  1re  10975  recgt0  11821  elnnz  12329  xrltlen  12880  xaddf  12958  xmullem  12998  xmullem2  12999  ssfzoulel  13481  elfznelfzo  13492  elfznelfzob  13493  om2uzf1oi  13673  fsuppmapnn0fiubex  13712  bcval4  14021  sadcaddlem  16164  lcmcllem  16301  lcmgcdlem  16311  lcmftp  16341  lcmfunsnlem2lem1  16343  lcmfunsnlem2lem2  16344  lcmfunsnlem2  16345  isprm3  16388  prm23ge5  16516  pcpremul  16544  subgmulg  18769  isnirred  19942  isdomn2  20570  cnfldfun  20609  mdetunilem7  21767  mndifsplit  21785  ordtbaslem  22339  iunconn  22579  fbun  22991  fin1aufil  23083  reconnlem2  23990  rrxmvallem  24568  pmltpc  24614  itg2splitlem  24913  mdegmullem  25243  atans2  26081  leibpilem2  26091  leibpi  26092  wilthlem2  26218  lgsdir2  26478  2lgslem3  26552  ragncol  27070  opptgdim2  27106  hlpasch  27117  trgcopy  27165  cgrg3col4  27214  structiedg0val  27392  usgredg2v  27594  nb3grprlem2  27748  vtxd0nedgb  27855  1egrvtxdg0  27878  wwlksnndef  28270  nfrgr2v  28636  nonbooli  30013  cvnbtwn4  30651  chirredi  30756  atcvat4i  30759  nelun  30859  hashxpe  31127  prmdvdsbc  31130  lindssn  31573  bnj1304  32799  bnj1417  33021  erdszelem9  33161  satf0n0  33340  fmlaomn0  33352  fmla0disjsuc  33360  fmlasucdisj  33361  3orit  33658  frxp2  33791  frxp3  33797  nosepdmlem  33886  sltrec  34014  dfon3  34194  dfrdg4  34253  wl-df3maxtru1  35663  poimirlem18  35795  poimirlem21  35798  orsild  36246  orsird  36247  notornotel1  36253  cvrat4  37457  hdmaplem4  39788  mapdh9a  39803  metakunt12  40136  dffltz  40471  fnwe2lem2  40876  ifpnot23  41085  ifpim123g  41107  ontric3g  41129  df3or2  41376  3ornot23VD  42467  ndisj2  42599  xrssre  42887  icccncfext  43428  fourierdlem42  43690  fourierdlem92  43739  salexct2  43878  nnfoctbdjlem  43993  euoreqb  44601  afvfv0bi  44644  afv2fv0  44757  ltnltne  44791  prproropf1olem4  44958  lighneallem4  45062  oddprmALTV  45139  mndpsuppss  45707  2itscp  46127