Theorem ioran 985

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395   ∨ wo 847

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 207  df-an 396  df-or 848

This theorem is referenced by:  pm4.56  990  xor  1016  3ioran  1105  3ori  1426  ecase23d  1475  19.43OLD  1884  dfun2  4219  prneimg2  4808  prnebg  4809  sotrieq2  5561  somo  5568  dflim3  7786  frxp  8065  poxp  8067  soxp  8068  frxp2  8083  frxp3  8090  suppofssd  8142  oalimcl  8484  omlimcl  8502  oeeulem  8525  fsetexb  8797  domunfican  9217  infsupprpr  9401  ordtypelem7  9421  cantnfp1lem2  9580  cantnfp1lem3  9581  cantnflem1  9590  cnfcom2lem  9602  ssfin4  10212  fin1a2lem7  10308  fin1a2lem12  10313  fpwwe2lem12  10544  fpwwe2  10545  r1wunlim  10639  recgt0  11978  elnnz  12489  xrltlen  13051  xaddf  13130  xmullem  13170  xmullem2  13171  ssfzoulel  13667  elfznelfzo  13680  elfznelfzob  13681  om2uzf1oi  13867  fsuppmapnn0fiubex  13906  bcval4  14221  sadcaddlem  16375  lcmcllem  16514  lcmgcdlem  16524  lcmftp  16554  lcmfunsnlem2lem1  16556  lcmfunsnlem2lem2  16557  lcmfunsnlem2  16558  isprm3  16601  prmdvdsbc  16644  prm23ge5  16734  pcpremul  16762  mndpsuppss  18681  subgmulg  19061  isnirred  20347  isdomn2OLD  20636  cnfldfun  21314  cnfldfunOLD  21327  mdetunilem7  22553  mndifsplit  22571  ordtbaslem  23123  iunconn  23363  fbun  23775  fin1aufil  23867  reconnlem2  24763  rrxmvallem  25351  pmltpc  25398  itg2splitlem  25696  mdegmullem  26030  atans2  26888  leibpilem2  26898  leibpi  26899  wilthlem2  27026  lgsdir2  27288  2lgslem3  27362  nosepdmlem  27642  sltrec  27782  om2noseqf1o  28251  elnnzs  28345  ragncol  28707  opptgdim2  28743  hlpasch  28754  trgcopy  28802  cgrg3col4  28851  structiedg0val  29021  usgredg2v  29226  nb3grprlem2  29380  vtxd0nedgb  29488  1egrvtxdg0  29511  wwlksnndef  29904  nfrgr2v  30273  nonbooli  31652  cvnbtwn4  32290  chirredi  32395  atcvat4i  32398  nelun  32514  hashxpe  32815  domnmuln0rd  33284  lindssn  33387  ssdifidlprm  33467  mxidlirred  33481  bnj1304  34903  bnj1417  35125  erdszelem9  35315  satf0n0  35494  fmlaomn0  35506  fmla0disjsuc  35514  fmlasucdisj  35515  3orit  35832  dfon3  36006  dfrdg4  36067  weiunpo  36581  wl-df3maxtru1  37609  poimirlem18  37751  poimirlem21  37754  orsild  38201  orsird  38202  notornotel1  38208  cvrat4  39615  hdmaplem4  41946  mapdh9a  41961  aks6d1c5lem1  42302  redvmptabs  42530  mulltgt0d  42652  mullt0b2d  42654  sn-mullt0d  42655  dffltz  42792  fnwe2lem2  43208  dflim6  43421  ifpnot23  43635  ifpim123g  43657  ontric3g  43679  df3or2  43925  3ornot23VD  45003  ndisj2  45212  xrssre  45509  icccncfext  46047  fourierdlem42  46309  fourierdlem92  46358  salexct2  46499  nnfoctbdjlem  46615  euoreqb  47271  afvfv0bi  47314  afv2fv0  47427  ltnltne  47461  prproropf1olem4  47668  lighneallem4  47772  oddprmALTV  47849  usgrexmpl2trifr  48199  2itscp  48943  fucofvalne  49486