Theorem ioran 999

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

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 401   ∨ wo 861

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862

This theorem is used by:  pm4.56  1004  orsild  1019  orsird  1020  xor  1032  3ioran  1123  3ori  1452  ecase23d  1504  ecase33d  1505  19.43OLD  1918  dfun2  4218  prneimg2  4815  prnebg  4816  sotrieq2  5598  somo  5605  dflim3  7892  frxp  8175  poxp  8177  soxp  8178  fnwe2lem3  8184  frxp2  8198  frxp3  8205  suppofssd  8258  oalimcl  8606  omlimcl  8624  oeeulem  8648  fsetexb  8924  domunfican  9351  infsupprpr  9535  ordtypelem7  9555  cantnfp1lem2  9717  cantnfp1lem3  9718  cantnflem1  9727  cnfcom2lem  9739  ssfin4  10427  fin1a2lem7  10523  fin1a2lem12  10528  fpwwe2lem12  10766  fpwwe2  10767  r1wunlim  10861  recgt0  12203  elnnz  12743  xrltlen  13315  xaddf  13394  xmullem  13434  xmullem2  13435  ssfzoulel  13935  elfznelfzo  13948  elfznelfzob  13949  om2uzf1oi  14136  fsuppmapnn0fiubex  14175  bcval4  14492  sadcaddlem  16671  lcmcllem  16815  lcmgcdlem  16825  lcmftp  16855  lcmfunsnlem2lem1  16857  lcmfunsnlem2lem2  16858  lcmfunsnlem2  16859  isprm3  16902  prmdvdsbc  16946  prm23ge5  17037  pcpremul  17065  mndpsuppss  19009  subgmulg  19401  isnirred  20701  ssdifidlprm  21693  prmidlsubm  21694  cnfldfun  21744  mdetunilem7  22988  mndifsplit  23006  ordtbaslem  23561  iunconn  23801  fbun  24214  fin1aufil  24306  reconnlem2  25202  rrxmvallem  25780  pmltpc  25826  itg2splitlem  26124  mdegmullem  26451  atans2  27316  leibpilem2  27326  leibpi  27327  wilthlem2  27453  lgsdir2  27714  2lgslem3  27788  nosepdmlem  28097  ltsrec  28244  om2noseqf1o  28744  elnnzs  28844  ragncol  29241  opptgdim2  29278  hlpasch  29291  trgcopy  29368  tgaaddcpbllem1  29406  tgaaddcpbl  29409  cgrg3col4  29429  angmgmaddeu1  29436  angmgmaddcpbl  29447  prlngex  29486  prlngmid2  29496  tgaltai  29502  structiedg0val  29657  usgredg2v  29865  nb3grprlem2  30019  vtxd0nedgb  30126  1egrvtxdg0  30149  wwlksnndef  30551  nfrgr2v  30930  nonbooli  32310  cvnbtwn4  32948  chirredi  33053  atcvat4i  33056  inagcgrabtwn  33108  tgextamirn  33124  tgextancd  33125  tgextalem1inag  33127  tgextamirnhl  33129  tgextancgra  33131  nelun  33208  hashxpe  33495  domnmuln0rd  33937  lindssn  34037  mxidlirred  34101  dflringlem2  34131  morleylemrneab  35411  bnj1304  35560  bnj1417  35782  erdszelem9  36172  satf0n0  36351  fmlaomn0  36363  fmla0disjsuc  36371  fmlasucdisj  36372  3orit  36696  dfon3  36869  dfrdg4  36930  weiunpo  37468  wl-df3maxtru1  38683  poimirlem18  38824  poimirlem21  38827  notornotel1  39293  cvrat4  40766  hdmaplem4  43097  mapdh9a  43112  aks6d1c5lem1  43452  redvmptabs  43677  mulltgt0d  43812  mullt0b2d  43814  sn-mullt0d  43815  dffltz  43936  dflim6  44527  ifpnot23  44740  ifpim123g  44762  ontric3g  44784  df3or2  45029  3ornot23VD  46089  ndisj2  46342  xrssre  46633  icccncfext  47170  fourierdlem42  47432  fourierdlem92  47481  salexct2  47622  nnfoctbdjlem  47738  euoreqb  48453  afvfv0bi  48495  afv2fv0  48608  ltnltne  48642  prproropf1olem4  48861  lighneallem4  48968  oddprmALTV  49058  usgrexmpl2trifr  49408  2itscp  50224  fucofvalne  50778