Theorem ioran 980

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 208   ∧ wa 398   ∨ wo 843

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 209  df-an 399  df-or 844

This theorem is referenced by:  pm4.56  985  xor  1011  3ioran  1102  3ori  1420  ecase23d  1469  noranOLD  1527  norassOLD  1534  19.43OLD  1884  2ralor  3369  dfun2  4236  prnebg  4786  sotrieq2  5503  somo  5510  dflim3  7562  frxp  7820  poxp  7822  soxp  7823  suppofssd  7867  oalimcl  8186  omlimcl  8204  oeeulem  8227  domunfican  8791  infsupprpr  8968  ordtypelem7  8988  cantnfp1lem2  9142  cantnfp1lem3  9143  cantnflem1  9152  cnfcom2lem  9164  ssfin4  9732  fin1a2lem7  9828  fin1a2lem12  9833  fpwwe2lem13  10064  fpwwe2  10065  r1wunlim  10159  1re  10641  recgt0  11486  elnnz  11992  xrltlen  12540  xaddf  12618  xmullem  12658  xmullem2  12659  ssfzoulel  13132  elfznelfzo  13143  elfznelfzob  13144  om2uzf1oi  13322  fsuppmapnn0fiubex  13361  bcval4  13668  sadcaddlem  15806  lcmcllem  15940  lcmgcdlem  15950  lcmftp  15980  lcmfunsnlem2lem1  15982  lcmfunsnlem2lem2  15983  lcmfunsnlem2  15984  isprm3  16027  prm23ge5  16152  pcpremul  16180  subgmulg  18293  isnirred  19450  isdomn2  20072  cnfldfunALT  20558  mdetunilem7  21227  mndifsplit  21245  ordtbaslem  21796  iunconn  22036  fbun  22448  fin1aufil  22540  reconnlem2  23435  rrxmvallem  24007  pmltpc  24051  itg2splitlem  24349  mdegmullem  24672  atans2  25509  leibpilem2  25519  leibpi  25520  wilthlem2  25646  lgsdir2  25906  2lgslem3  25980  ragncol  26495  opptgdim2  26531  hlpasch  26542  trgcopy  26590  cgrg3col4  26639  structiedg0val  26807  usgredg2v  27009  nb3grprlem2  27163  vtxd0nedgb  27270  1egrvtxdg0  27293  wwlksnndef  27683  wwlksnfiOLD  27685  nfrgr2v  28051  nonbooli  29428  cvnbtwn4  30066  chirredi  30171  atcvat4i  30174  nelun  30274  hashxpe  30529  prmdvdsbc  30532  lindssn  30939  bnj1304  32091  bnj1417  32313  erdszelem9  32446  satf0n0  32625  fmlaomn0  32637  fmla0disjsuc  32645  fmlasucdisj  32646  3orit  32945  nosepdmlem  33187  sltrec  33278  dfon3  33353  dfrdg4  33412  poimirlem18  34925  poimirlem21  34928  orsild  35381  orsird  35382  notornotel1  35388  cvrat4  36594  hdmaplem4  38925  mapdh9a  38940  dffltz  39291  fnwe2lem2  39671  ifpnot23  39864  ifpim123g  39886  ontric3g  39908  df3or2  40133  3ornot23VD  41201  ndisj2  41333  xrssre  41636  icccncfext  42190  fourierdlem42  42454  fourierdlem92  42503  salexct2  42642  nnfoctbdjlem  42757  euoreqb  43328  afvfv0bi  43371  afv2fv0  43484  ltnltne  43519  prproropf1olem4  43688  lighneallem4  43795  oddprmALTV  43872  mndpsuppss  44439  2itscp  44788