MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ioran Structured version   Visualization version   GIF version

Theorem ioran 509
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
StepHypRef Expression
1 pm4.65 441 . 2 (¬ (¬ 𝜑𝜓) ↔ (¬ 𝜑 ∧ ¬ 𝜓))
2 pm4.64 385 . 2 ((¬ 𝜑𝜓) ↔ (𝜑𝜓))
31, 2xchnxbi 320 1 (¬ (𝜑𝜓) ↔ (¬ 𝜑 ∧ ¬ 𝜓))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 194  wo 381  wa 382
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 195  df-or 383  df-an 384
This theorem is referenced by:  pm4.56  514  xor  930  3ioran  1048  3ori  1379  ecase23d  1427  19.43OLD  1799  2ralor  3084  dfun2  3817  prnebg  4321  sotrieq2  4974  somo  4980  ordnbtwnOLD  5717  dflim3  6913  frxp  7148  poxp  7150  soxp  7151  oalimcl  7501  omlimcl  7519  oeeulem  7542  domunfican  8092  ordtypelem7  8286  cantnfp1lem2  8433  cantnfp1lem3  8434  cantnflem1  8443  cnfcom2lem  8455  ssfin4  8989  fin1a2lem7  9085  fin1a2lem12  9090  fpwwe2lem13  9317  fpwwe2  9318  r1wunlim  9412  1re  9892  recgt0  10713  elnnz  11217  xrltlen  11811  xaddf  11885  xmullem  11920  xmullem2  11921  ssfzoulel  12380  elfznelfzo  12391  elfznelfzob  12392  om2uzf1oi  12566  fsuppmapnn0fiubex  12606  bcval4  12908  sadcaddlem  14960  lcmcllem  15090  lcmgcdlem  15100  lcmftp  15130  lcmfunsnlem2lem1  15132  lcmfunsnlem2lem2  15133  lcmfunsnlem2  15134  isprm3  15177  prm23ge5  15301  pcpremul  15329  subgmulg  17374  isnirred  18466  isdomn2  19063  mdetunilem7  20182  mndifsplit  20200  ordtbaslem  20741  iuncon  20980  fbun  21393  fin1aufil  21485  reconnlem2  22367  rrxmvallem  22909  pmltpc  22940  itg2splitlem  23235  mdegmullem  23556  atans2  24372  leibpilem2  24382  leibpi  24383  wilthlem2  24509  lgsdir2  24769  2lgslem3  24843  ragncol  25319  opptgdim2  25352  hlpasch  25363  trgcopy  25411  cgrg3col4  25449  usgraidx2v  25685  nbgra0nb  25721  nb3graprlem2  25744  frgra2v  26289  frgrareg  26407  nonbooli  27697  cvnbtwn4  28335  chirredi  28440  atcvat4i  28443  bnj1304  29947  bnj1417  30166  erdszelem9  30238  3orit  30654  nofulllem5  30908  dfon3  30972  dfrdg4  31031  poimirlem18  32397  poimirlem21  32400  orsild  32859  orsird  32860  notornotel1  32867  cvrat4  33547  hdmaplem4  35881  mapdh9a  35897  fnwe2lem2  36439  ifpnot23  36642  ifpim123g  36664  df3or2  36879  3ornot23VD  37904  ndisj2  38043  xrssre  38306  icccncfext  38574  fourierdlem42  38843  fourierdlem92  38892  salexct2  39034  nnfoctbdjlem  39149  afvfv0bi  39683  lighneallem4  39867  oddprmALTV  39938  ltnltne  40169  structiedg0val  40254  usgredg2v  40453  nb3grprlem2  40608  vtxd0nedgb  40702  1egrvtxdg0  40726  wwlksnndef  41110  wwlksnfi  41111  clwwlksnndef  41197  nfrgr2v  41441  mndpsuppss  41945
  Copyright terms: Public domain W3C validator