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  1883  dfun2  4229  prneimg2  4815  prnebg  4816  sotrieq2  5571  somo  5578  dflim3  7803  frxp  8082  poxp  8084  soxp  8085  frxp2  8100  frxp3  8107  suppofssd  8159  oalimcl  8501  omlimcl  8519  oeeulem  8542  fsetexb  8814  domunfican  9248  infsupprpr  9433  ordtypelem7  9453  cantnfp1lem2  9608  cantnfp1lem3  9609  cantnflem1  9618  cnfcom2lem  9630  ssfin4  10239  fin1a2lem7  10335  fin1a2lem12  10340  fpwwe2lem12  10571  fpwwe2  10572  r1wunlim  10666  recgt0  12004  elnnz  12515  xrltlen  13082  xaddf  13160  xmullem  13200  xmullem2  13201  ssfzoulel  13697  elfznelfzo  13709  elfznelfzob  13710  om2uzf1oi  13894  fsuppmapnn0fiubex  13933  bcval4  14248  sadcaddlem  16403  lcmcllem  16542  lcmgcdlem  16552  lcmftp  16582  lcmfunsnlem2lem1  16584  lcmfunsnlem2lem2  16585  lcmfunsnlem2  16586  isprm3  16629  prmdvdsbc  16672  prm23ge5  16762  pcpremul  16790  mndpsuppss  18668  subgmulg  19048  isnirred  20305  isdomn2OLD  20597  cnfldfun  21254  cnfldfunOLD  21267  mdetunilem7  22481  mndifsplit  22499  ordtbaslem  23051  iunconn  23291  fbun  23703  fin1aufil  23795  reconnlem2  24692  rrxmvallem  25280  pmltpc  25327  itg2splitlem  25625  mdegmullem  25959  atans2  26817  leibpilem2  26827  leibpi  26828  wilthlem2  26955  lgsdir2  27217  2lgslem3  27291  nosepdmlem  27571  sltrec  27708  om2noseqf1o  28171  elnnzs  28265  ragncol  28612  opptgdim2  28648  hlpasch  28659  trgcopy  28707  cgrg3col4  28756  structiedg0val  28925  usgredg2v  29130  nb3grprlem2  29284  vtxd0nedgb  29392  1egrvtxdg0  29415  wwlksnndef  29808  nfrgr2v  30174  nonbooli  31553  cvnbtwn4  32191  chirredi  32296  atcvat4i  32299  nelun  32415  hashxpe  32705  domnmuln0rd  33198  lindssn  33322  ssdifidlprm  33402  mxidlirred  33416  bnj1304  34782  bnj1417  35004  erdszelem9  35159  satf0n0  35338  fmlaomn0  35350  fmla0disjsuc  35358  fmlasucdisj  35359  3orit  35676  dfon3  35853  dfrdg4  35912  weiunpo  36426  wl-df3maxtru1  37453  poimirlem18  37605  poimirlem21  37608  orsild  38055  orsird  38056  notornotel1  38062  cvrat4  39410  hdmaplem4  41741  mapdh9a  41756  aks6d1c5lem1  42097  redvmptabs  42321  mulltgt0d  42443  mullt0b2d  42445  sn-mullt0d  42446  dffltz  42595  fnwe2lem2  43013  dflim6  43226  ifpnot23  43440  ifpim123g  43462  ontric3g  43484  df3or2  43730  3ornot23VD  44809  ndisj2  45018  xrssre  45317  icccncfext  45858  fourierdlem42  46120  fourierdlem92  46169  salexct2  46310  nnfoctbdjlem  46426  euoreqb  47083  afvfv0bi  47126  afv2fv0  47239  ltnltne  47273  prproropf1olem4  47480  lighneallem4  47584  oddprmALTV  47661  usgrexmpl2trifr  48001  2itscp  48743  fucofvalne  49287