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  4260  prnebg  4857  sotrieq2  5619  somo  5626  dflim3  7836  frxp  8112  poxp  8114  soxp  8115  frxp2  8130  frxp3  8137  suppofssd  8188  oalimcl  8560  omlimcl  8578  oeeulem  8601  fsetexb  8858  domunfican  9320  infsupprpr  9499  ordtypelem7  9519  cantnfp1lem2  9674  cantnfp1lem3  9675  cantnflem1  9684  cnfcom2lem  9696  ssfin4  10305  fin1a2lem7  10401  fin1a2lem12  10406  fpwwe2lem12  10637  fpwwe2  10638  r1wunlim  10732  1re  11214  recgt0  12060  elnnz  12568  xrltlen  13125  xaddf  13203  xmullem  13243  xmullem2  13244  ssfzoulel  13726  elfznelfzo  13737  elfznelfzob  13738  om2uzf1oi  13918  fsuppmapnn0fiubex  13957  bcval4  14267  sadcaddlem  16398  lcmcllem  16533  lcmgcdlem  16543  lcmftp  16573  lcmfunsnlem2lem1  16575  lcmfunsnlem2lem2  16576  lcmfunsnlem2  16577  isprm3  16620  prm23ge5  16748  pcpremul  16776  subgmulg  19020  isnirred  20234  isdomn2  20915  cnfldfun  20956  mdetunilem7  22120  mndifsplit  22138  ordtbaslem  22692  iunconn  22932  fbun  23344  fin1aufil  23436  reconnlem2  24343  rrxmvallem  24921  pmltpc  24967  itg2splitlem  25266  mdegmullem  25596  atans2  26436  leibpilem2  26446  leibpi  26447  wilthlem2  26573  lgsdir2  26833  2lgslem3  26907  nosepdmlem  27186  sltrec  27321  ragncol  27960  opptgdim2  27996  hlpasch  28007  trgcopy  28055  cgrg3col4  28104  structiedg0val  28282  usgredg2v  28484  nb3grprlem2  28638  vtxd0nedgb  28745  1egrvtxdg0  28768  wwlksnndef  29159  nfrgr2v  29525  nonbooli  30904  cvnbtwn4  31542  chirredi  31647  atcvat4i  31650  nelun  31751  hashxpe  32019  prmdvdsbc  32022  lindssn  32494  mxidlirred  32588  bnj1304  33830  bnj1417  34052  erdszelem9  34190  satf0n0  34369  fmlaomn0  34381  fmla0disjsuc  34389  fmlasucdisj  34390  3orit  34685  dfon3  34864  dfrdg4  34923  wl-df3maxtru1  36373  poimirlem18  36506  poimirlem21  36509  orsild  36956  orsird  36957  notornotel1  36963  cvrat4  38314  hdmaplem4  40645  mapdh9a  40660  metakunt12  40996  dffltz  41376  fnwe2lem2  41793  dflim6  42014  ifpnot23  42229  ifpim123g  42251  ontric3g  42273  df3or2  42519  3ornot23VD  43608  ndisj2  43738  xrssre  44058  icccncfext  44603  fourierdlem42  44865  fourierdlem92  44914  salexct2  45055  nnfoctbdjlem  45171  euoreqb  45817  afvfv0bi  45860  afv2fv0  45973  ltnltne  46007  prproropf1olem4  46174  lighneallem4  46278  oddprmALTV  46355  mndpsuppss  47047  2itscp  47467