Theorem ioran 983

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 205   ∧ wa 397   ∨ wo 846

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 206  df-an 398  df-or 847

This theorem is referenced by:  pm4.56  988  xor  1014  3ioran  1107  3ori  1425  ecase23d  1474  19.43OLD  1887  2ralorOLD  3230  dfun2  4258  prnebg  4855  sotrieq2  5617  somo  5624  dflim3  7831  frxp  8107  poxp  8109  soxp  8110  frxp2  8125  frxp3  8132  suppofssd  8183  oalimcl  8556  omlimcl  8574  oeeulem  8597  fsetexb  8854  domunfican  9316  infsupprpr  9495  ordtypelem7  9515  cantnfp1lem2  9670  cantnfp1lem3  9671  cantnflem1  9680  cnfcom2lem  9692  ssfin4  10301  fin1a2lem7  10397  fin1a2lem12  10402  fpwwe2lem12  10633  fpwwe2  10634  r1wunlim  10728  1re  11210  recgt0  12056  elnnz  12564  xrltlen  13121  xaddf  13199  xmullem  13239  xmullem2  13240  ssfzoulel  13722  elfznelfzo  13733  elfznelfzob  13734  om2uzf1oi  13914  fsuppmapnn0fiubex  13953  bcval4  14263  sadcaddlem  16394  lcmcllem  16529  lcmgcdlem  16539  lcmftp  16569  lcmfunsnlem2lem1  16571  lcmfunsnlem2lem2  16572  lcmfunsnlem2  16573  isprm3  16616  prm23ge5  16744  pcpremul  16772  subgmulg  19014  isnirred  20223  isdomn2  20902  cnfldfun  20941  mdetunilem7  22102  mndifsplit  22120  ordtbaslem  22674  iunconn  22914  fbun  23326  fin1aufil  23418  reconnlem2  24325  rrxmvallem  24903  pmltpc  24949  itg2splitlem  25248  mdegmullem  25578  atans2  26416  leibpilem2  26426  leibpi  26427  wilthlem2  26553  lgsdir2  26813  2lgslem3  26887  nosepdmlem  27166  sltrec  27301  ragncol  27940  opptgdim2  27976  hlpasch  27987  trgcopy  28035  cgrg3col4  28084  structiedg0val  28262  usgredg2v  28464  nb3grprlem2  28618  vtxd0nedgb  28725  1egrvtxdg0  28748  wwlksnndef  29139  nfrgr2v  29505  nonbooli  30882  cvnbtwn4  31520  chirredi  31625  atcvat4i  31628  nelun  31729  hashxpe  31997  prmdvdsbc  32000  lindssn  32459  bnj1304  33768  bnj1417  33990  erdszelem9  34128  satf0n0  34307  fmlaomn0  34319  fmla0disjsuc  34327  fmlasucdisj  34328  3orit  34623  dfon3  34802  dfrdg4  34861  wl-df3maxtru1  36311  poimirlem18  36444  poimirlem21  36447  orsild  36894  orsird  36895  notornotel1  36901  cvrat4  38252  hdmaplem4  40583  mapdh9a  40598  metakunt12  40934  dffltz  41320  fnwe2lem2  41726  dflim6  41947  ifpnot23  42162  ifpim123g  42184  ontric3g  42206  df3or2  42452  3ornot23VD  43541  ndisj2  43671  xrssre  43993  icccncfext  44538  fourierdlem42  44800  fourierdlem92  44849  salexct2  44990  nnfoctbdjlem  45106  euoreqb  45752  afvfv0bi  45795  afv2fv0  45908  ltnltne  45942  prproropf1olem4  46109  lighneallem4  46213  oddprmALTV  46290  mndpsuppss  46949  2itscp  47369