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

Theorem ioran 979
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 408 . 2 (¬ (¬ 𝜑𝜓) ↔ (¬ 𝜑 ∧ ¬ 𝜓))
2 pm4.64 845 . 2 ((¬ 𝜑𝜓) ↔ (𝜑𝜓))
31, 2xchnxbi 334 1 (¬ (𝜑𝜓) ↔ (¬ 𝜑 ∧ ¬ 𝜓))
Colors of variables: wff setvar class
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  984  xor  1010  3ioran  1100  3ori  1418  ecase23d  1466  noranOLD  1520  norassOLD  1527  19.43OLD  1877  2ralor  3368  dfun2  4234  prnebg  4778  sotrieq2  5496  somo  5503  dflim3  7554  frxp  7812  poxp  7814  soxp  7815  suppofssd  7859  oalimcl  8178  omlimcl  8196  oeeulem  8219  domunfican  8783  infsupprpr  8960  ordtypelem7  8980  cantnfp1lem2  9134  cantnfp1lem3  9135  cantnflem1  9144  cnfcom2lem  9156  ssfin4  9724  fin1a2lem7  9820  fin1a2lem12  9825  fpwwe2lem13  10056  fpwwe2  10057  r1wunlim  10151  1re  10633  recgt0  11478  elnnz  11983  xrltlen  12531  xaddf  12609  xmullem  12649  xmullem2  12650  ssfzoulel  13123  elfznelfzo  13134  elfznelfzob  13135  om2uzf1oi  13313  fsuppmapnn0fiubex  13352  bcval4  13659  sadcaddlem  15798  lcmcllem  15932  lcmgcdlem  15942  lcmftp  15972  lcmfunsnlem2lem1  15974  lcmfunsnlem2lem2  15975  lcmfunsnlem2  15976  isprm3  16019  prm23ge5  16144  pcpremul  16172  subgmulg  18285  isnirred  19442  isdomn2  20064  cnfldfunALT  20550  mdetunilem7  21219  mndifsplit  21237  ordtbaslem  21788  iunconn  22028  fbun  22440  fin1aufil  22532  reconnlem2  23427  rrxmvallem  23999  pmltpc  24043  itg2splitlem  24341  mdegmullem  24664  atans2  25501  leibpilem2  25511  leibpi  25512  wilthlem2  25638  lgsdir2  25898  2lgslem3  25972  ragncol  26487  opptgdim2  26523  hlpasch  26534  trgcopy  26582  cgrg3col4  26631  structiedg0val  26799  usgredg2v  27001  nb3grprlem2  27155  vtxd0nedgb  27262  1egrvtxdg0  27285  wwlksnndef  27675  wwlksnfiOLD  27677  nfrgr2v  28043  nonbooli  29420  cvnbtwn4  30058  chirredi  30163  atcvat4i  30166  nelun  30266  hashxpe  30521  prmdvdsbc  30524  lindssn  30932  bnj1304  32079  bnj1417  32301  erdszelem9  32434  satf0n0  32613  fmlaomn0  32625  fmla0disjsuc  32633  fmlasucdisj  32634  3orit  32933  nosepdmlem  33175  sltrec  33266  dfon3  33341  dfrdg4  33400  poimirlem18  34892  poimirlem21  34895  orsild  35348  orsird  35349  notornotel1  35355  cvrat4  36561  hdmaplem4  38892  mapdh9a  38907  dffltz  39251  fnwe2lem2  39631  ifpnot23  39824  ifpim123g  39846  ontric3g  39868  df3or2  40093  3ornot23VD  41161  ndisj2  41293  xrssre  41595  icccncfext  42149  fourierdlem42  42414  fourierdlem92  42463  salexct2  42602  nnfoctbdjlem  42717  euoreqb  43288  afvfv0bi  43331  afv2fv0  43444  ltnltne  43479  prproropf1olem4  43648  lighneallem4  43755  oddprmALTV  43832  mndpsuppss  44399  2itscp  44748
  Copyright terms: Public domain W3C validator