Theorem ioran 969

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 198   ∧ wa 386   ∨ wo 836

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 199  df-an 387  df-or 837

This theorem is referenced by:  pm4.56  974  xor  1000  3ioran  1093  3ori  1497  ecase23d  1546  19.43OLD  1930  2ralor  3295  dfun2  4086  prnebg  4619  sotrieq2  5305  somo  5312  dflim3  7327  frxp  7570  poxp  7572  soxp  7573  oalimcl  7926  omlimcl  7944  oeeulem  7967  domunfican  8523  infsupprpr  8700  ordtypelem7  8720  cantnfp1lem2  8875  cantnfp1lem3  8876  cantnflem1  8885  cnfcom2lem  8897  ssfin4  9469  fin1a2lem7  9565  fin1a2lem12  9570  fpwwe2lem13  9801  fpwwe2  9802  r1wunlim  9896  1re  10378  recgt0  11224  elnnz  11743  xrltlen  12294  xaddf  12372  xmullem  12411  xmullem2  12412  ssfzoulel  12886  elfznelfzo  12897  elfznelfzob  12898  om2uzf1oi  13076  fsuppmapnn0fiubex  13115  bcval4  13418  sadcaddlem  15595  lcmcllem  15725  lcmgcdlem  15735  lcmftp  15765  lcmfunsnlem2lem1  15767  lcmfunsnlem2lem2  15768  lcmfunsnlem2  15769  isprm3  15812  prm23ge5  15935  pcpremul  15963  subgmulg  18003  isnirred  19098  isdomn2  19707  cnfldfunALT  20166  mdetunilem7  20840  mndifsplit  20858  ordtbaslem  21411  iunconn  21651  fbun  22063  fin1aufil  22155  reconnlem2  23049  rrxmvallem  23621  pmltpc  23665  itg2splitlem  23963  mdegmullem  24286  atans2  25120  leibpilem2  25131  leibpi  25132  wilthlem2  25258  lgsdir2  25518  2lgslem3  25592  ragncol  26077  opptgdim2  26110  hlpasch  26121  trgcopy  26169  cgrg3col4  26219  structiedg0val  26387  usgredg2v  26590  nb3grprlem2  26746  vtxd0nedgb  26853  1egrvtxdg0  26876  wwlksnndef  27294  wwlksnfiOLD  27296  nfrgr2v  27697  nonbooli  29099  cvnbtwn4  29737  chirredi  29842  atcvat4i  29845  bnj1304  31497  bnj1417  31716  erdszelem9  31788  3orit  32201  nosepdmlem  32430  sltrec  32521  dfon3  32596  dfrdg4  32655  poimirlem18  34062  poimirlem21  34065  orsild  34522  orsird  34523  notornotel1  34529  cvrat4  35606  hdmaplem4  37937  mapdh9a  37952  dffltz  38226  fnwe2lem2  38594  ifpnot23  38795  ifpim123g  38817  df3or2  39031  3ornot23VD  40030  ndisj2  40164  xrssre  40486  icccncfext  41042  fourierdlem42  41307  fourierdlem92  41356  salexct2  41495  nnfoctbdjlem  41610  euoreqb  42155  afvfv0bi  42207  afv2fv0  42320  ltnltne  42355  prproropf1olem4  42459  lighneallem4  42562  oddprmALTV  42637  mndpsuppss  43181  2itscp  43531