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  4215  prneimg2  4802  prnebg  4803  sotrieq2  5551  somo  5558  dflim3  7772  frxp  8051  poxp  8053  soxp  8054  frxp2  8069  frxp3  8076  suppofssd  8128  oalimcl  8470  omlimcl  8488  oeeulem  8511  fsetexb  8783  domunfican  9201  infsupprpr  9385  ordtypelem7  9405  cantnfp1lem2  9564  cantnfp1lem3  9565  cantnflem1  9574  cnfcom2lem  9586  ssfin4  10196  fin1a2lem7  10292  fin1a2lem12  10297  fpwwe2lem12  10528  fpwwe2  10529  r1wunlim  10623  recgt0  11962  elnnz  12473  xrltlen  13040  xaddf  13118  xmullem  13158  xmullem2  13159  ssfzoulel  13655  elfznelfzo  13668  elfznelfzob  13669  om2uzf1oi  13855  fsuppmapnn0fiubex  13894  bcval4  14209  sadcaddlem  16363  lcmcllem  16502  lcmgcdlem  16512  lcmftp  16542  lcmfunsnlem2lem1  16544  lcmfunsnlem2lem2  16545  lcmfunsnlem2  16546  isprm3  16589  prmdvdsbc  16632  prm23ge5  16722  pcpremul  16750  mndpsuppss  18668  subgmulg  19048  isnirred  20333  isdomn2OLD  20622  cnfldfun  21300  cnfldfunOLD  21313  mdetunilem7  22528  mndifsplit  22546  ordtbaslem  23098  iunconn  23338  fbun  23750  fin1aufil  23842  reconnlem2  24738  rrxmvallem  25326  pmltpc  25373  itg2splitlem  25671  mdegmullem  26005  atans2  26863  leibpilem2  26873  leibpi  26874  wilthlem2  27001  lgsdir2  27263  2lgslem3  27337  nosepdmlem  27617  sltrec  27757  om2noseqf1o  28226  elnnzs  28320  ragncol  28682  opptgdim2  28718  hlpasch  28729  trgcopy  28777  cgrg3col4  28826  structiedg0val  28995  usgredg2v  29200  nb3grprlem2  29354  vtxd0nedgb  29462  1egrvtxdg0  29485  wwlksnndef  29878  nfrgr2v  30244  nonbooli  31623  cvnbtwn4  32261  chirredi  32366  atcvat4i  32369  nelun  32485  hashxpe  32781  domnmuln0rd  33233  lindssn  33335  ssdifidlprm  33415  mxidlirred  33429  bnj1304  34823  bnj1417  35045  erdszelem9  35235  satf0n0  35414  fmlaomn0  35426  fmla0disjsuc  35434  fmlasucdisj  35435  3orit  35752  dfon3  35926  dfrdg4  35985  weiunpo  36499  wl-df3maxtru1  37526  poimirlem18  37678  poimirlem21  37681  orsild  38128  orsird  38129  notornotel1  38135  cvrat4  39482  hdmaplem4  41813  mapdh9a  41828  aks6d1c5lem1  42169  redvmptabs  42393  mulltgt0d  42515  mullt0b2d  42517  sn-mullt0d  42518  dffltz  42667  fnwe2lem2  43084  dflim6  43297  ifpnot23  43511  ifpim123g  43533  ontric3g  43555  df3or2  43801  3ornot23VD  44879  ndisj2  45088  xrssre  45387  icccncfext  45925  fourierdlem42  46187  fourierdlem92  46236  salexct2  46377  nnfoctbdjlem  46493  euoreqb  47140  afvfv0bi  47183  afv2fv0  47296  ltnltne  47330  prproropf1olem4  47537  lighneallem4  47641  oddprmALTV  47718  usgrexmpl2trifr  48068  2itscp  48813  fucofvalne  49357