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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 399   ∨ 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 210  df-an 400  df-or 845

This theorem is referenced by:  pm4.56  986  xor  1012  3ioran  1103  3ori  1421  ecase23d  1470  noranOLD  1528  norassOLD  1535  19.43OLD  1884  2ralor  3322  dfun2  4186  prnebg  4746  sotrieq2  5467  somo  5474  dflim3  7542  frxp  7803  poxp  7805  soxp  7806  suppofssd  7850  oalimcl  8169  omlimcl  8187  oeeulem  8210  domunfican  8775  infsupprpr  8952  ordtypelem7  8972  cantnfp1lem2  9126  cantnfp1lem3  9127  cantnflem1  9136  cnfcom2lem  9148  ssfin4  9721  fin1a2lem7  9817  fin1a2lem12  9822  fpwwe2lem13  10053  fpwwe2  10054  r1wunlim  10148  1re  10630  recgt0  11475  elnnz  11979  xrltlen  12527  xaddf  12605  xmullem  12645  xmullem2  12646  ssfzoulel  13126  elfznelfzo  13137  elfznelfzob  13138  om2uzf1oi  13316  fsuppmapnn0fiubex  13355  bcval4  13663  sadcaddlem  15796  lcmcllem  15930  lcmgcdlem  15940  lcmftp  15970  lcmfunsnlem2lem1  15972  lcmfunsnlem2lem2  15973  lcmfunsnlem2  15974  isprm3  16017  prm23ge5  16142  pcpremul  16170  subgmulg  18285  isnirred  19446  isdomn2  20065  cnfldfunALT  20104  mdetunilem7  21223  mndifsplit  21241  ordtbaslem  21793  iunconn  22033  fbun  22445  fin1aufil  22537  reconnlem2  23432  rrxmvallem  24008  pmltpc  24054  itg2splitlem  24352  mdegmullem  24679  atans2  25517  leibpilem2  25527  leibpi  25528  wilthlem2  25654  lgsdir2  25914  2lgslem3  25988  ragncol  26503  opptgdim2  26539  hlpasch  26550  trgcopy  26598  cgrg3col4  26647  structiedg0val  26815  usgredg2v  27017  nb3grprlem2  27171  vtxd0nedgb  27278  1egrvtxdg0  27301  wwlksnndef  27691  nfrgr2v  28057  nonbooli  29434  cvnbtwn4  30072  chirredi  30177  atcvat4i  30180  nelun  30282  hashxpe  30555  prmdvdsbc  30558  lindssn  30993  bnj1304  32201  bnj1417  32423  erdszelem9  32559  satf0n0  32738  fmlaomn0  32750  fmla0disjsuc  32758  fmlasucdisj  32759  3orit  33058  nosepdmlem  33300  sltrec  33391  dfon3  33466  dfrdg4  33525  wl-df3maxtru1  34909  poimirlem18  35075  poimirlem21  35078  orsild  35526  orsird  35527  notornotel1  35533  cvrat4  36739  hdmaplem4  39070  mapdh9a  39085  metakunt12  39361  dffltz  39615  fnwe2lem2  39995  ifpnot23  40186  ifpim123g  40208  ontric3g  40230  df3or2  40469  3ornot23VD  41553  ndisj2  41685  xrssre  41980  icccncfext  42529  fourierdlem42  42791  fourierdlem92  42840  salexct2  42979  nnfoctbdjlem  43094  euoreqb  43665  afvfv0bi  43708  afv2fv0  43821  ltnltne  43856  prproropf1olem4  44023  lighneallem4  44128  oddprmALTV  44205  mndpsuppss  44773  2itscp  45195