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

Theorem ioran 511
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 443 . 2 (¬ (¬ 𝜑𝜓) ↔ (¬ 𝜑 ∧ ¬ 𝜓))
2 pm4.64 387 . 2 ((¬ 𝜑𝜓) ↔ (𝜑𝜓))
31, 2xchnxbi 322 1 (¬ (𝜑𝜓) ↔ (¬ 𝜑 ∧ ¬ 𝜓))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wo 383  wa 384
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 197  df-or 385  df-an 386
This theorem is referenced by:  pm4.56  516  xor  935  3ioran  1055  3ori  1387  ecase23d  1435  19.43OLD  1810  2ralor  3107  dfun2  3857  prnebg  4387  sotrieq2  5061  somo  5067  ordnbtwnOLD  5815  dflim3  7044  frxp  7284  poxp  7286  soxp  7287  oalimcl  7637  omlimcl  7655  oeeulem  7678  domunfican  8230  ordtypelem7  8426  cantnfp1lem2  8573  cantnfp1lem3  8574  cantnflem1  8583  cnfcom2lem  8595  ssfin4  9129  fin1a2lem7  9225  fin1a2lem12  9230  fpwwe2lem13  9461  fpwwe2  9462  r1wunlim  9556  1re  10036  recgt0  10864  elnnz  11384  xrltlen  11976  xaddf  12052  xmullem  12091  xmullem2  12092  ssfzoulel  12558  elfznelfzo  12569  elfznelfzob  12570  om2uzf1oi  12747  fsuppmapnn0fiubex  12787  bcval4  13089  sadcaddlem  15173  lcmcllem  15303  lcmgcdlem  15313  lcmftp  15343  lcmfunsnlem2lem1  15345  lcmfunsnlem2lem2  15346  lcmfunsnlem2  15347  isprm3  15390  prm23ge5  15514  pcpremul  15542  subgmulg  17602  isnirred  18694  isdomn2  19293  cnfldfunALT  19753  mdetunilem7  20418  mndifsplit  20436  ordtbaslem  20986  iunconn  21225  fbun  21638  fin1aufil  21730  reconnlem2  22624  rrxmvallem  23181  pmltpc  23213  itg2splitlem  23509  mdegmullem  23832  atans2  24652  leibpilem2  24662  leibpi  24663  wilthlem2  24789  lgsdir2  25049  2lgslem3  25123  ragncol  25598  opptgdim2  25631  hlpasch  25642  trgcopy  25690  cgrg3col4  25728  structiedg0val  25905  usgredg2v  26113  nb3grprlem2  26277  vtxd0nedgb  26378  1egrvtxdg0  26401  wwlksnndef  26794  wwlksnfi  26795  clwwlksnndef  26884  nfrgr2v  27129  nonbooli  28494  cvnbtwn4  29132  chirredi  29237  atcvat4i  29240  bnj1304  30875  bnj1417  31094  erdszelem9  31166  3orit  31582  nosepdmlem  31817  sltrec  31908  dfon3  31983  dfrdg4  32042  poimirlem18  33407  poimirlem21  33410  orsild  33869  orsird  33870  notornotel1  33877  cvrat4  34555  hdmaplem4  36889  mapdh9a  36905  fnwe2lem2  37447  ifpnot23  37649  ifpim123g  37671  df3or2  37886  3ornot23VD  38908  ndisj2  39044  xrssre  39383  icccncfext  39869  fourierdlem42  40135  fourierdlem92  40184  salexct2  40326  nnfoctbdjlem  40441  afvfv0bi  41001  ltnltne  41082  lighneallem4  41298  oddprmALTV  41369  mndpsuppss  41923
  Copyright terms: Public domain W3C validator