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

Theorem ioran 512
 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 442 . 2 (¬ (¬ 𝜑𝜓) ↔ (¬ 𝜑 ∧ ¬ 𝜓))
2 pm4.64 386 . 2 ((¬ 𝜑𝜓) ↔ (𝜑𝜓))
31, 2xchnxbi 321 1 (¬ (𝜑𝜓) ↔ (¬ 𝜑 ∧ ¬ 𝜓))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 196   ∨ wo 382   ∧ wa 383 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 384  df-an 385 This theorem is referenced by:  pm4.56  517  xor  971  3ioran  1095  3ori  1501  ecase23d  1549  19.43OLD  1924  2ralor  3211  dfun2  3967  prnebg  4496  sotrieq2  5167  somo  5173  ordnbtwnOLD  5930  dflim3  7164  frxp  7407  poxp  7409  soxp  7410  oalimcl  7760  omlimcl  7778  oeeulem  7801  domunfican  8349  ordtypelem7  8545  cantnfp1lem2  8689  cantnfp1lem3  8690  cantnflem1  8699  cnfcom2lem  8711  ssfin4  9245  fin1a2lem7  9341  fin1a2lem12  9346  fpwwe2lem13  9577  fpwwe2  9578  r1wunlim  9672  1re  10152  recgt0  10980  elnnz  11500  xrltlen  12093  xaddf  12169  xmullem  12208  xmullem2  12209  ssfzoulel  12677  elfznelfzo  12688  elfznelfzob  12689  om2uzf1oi  12867  fsuppmapnn0fiubex  12907  bcval4  13209  sadcaddlem  15302  lcmcllem  15432  lcmgcdlem  15442  lcmftp  15472  lcmfunsnlem2lem1  15474  lcmfunsnlem2lem2  15475  lcmfunsnlem2  15476  isprm3  15519  prm23ge5  15643  pcpremul  15671  subgmulg  17730  isnirred  18821  isdomn2  19422  cnfldfunALT  19882  mdetunilem7  20547  mndifsplit  20565  ordtbaslem  21115  iunconn  21354  fbun  21766  fin1aufil  21858  reconnlem2  22752  rrxmvallem  23308  pmltpc  23340  itg2splitlem  23635  mdegmullem  23958  atans2  24778  leibpilem2  24788  leibpi  24789  wilthlem2  24915  lgsdir2  25175  2lgslem3  25249  ragncol  25724  opptgdim2  25757  hlpasch  25768  trgcopy  25816  cgrg3col4  25854  structiedg0val  26031  usgredg2v  26239  nb3grprlem2  26402  vtxd0nedgb  26515  1egrvtxdg0  26538  wwlksnndef  26944  wwlksnfi  26945  nfrgr2v  27347  nonbooli  28740  cvnbtwn4  29378  chirredi  29483  atcvat4i  29486  bnj1304  31118  bnj1417  31337  erdszelem9  31409  3orit  31824  nosepdmlem  32060  sltrec  32151  dfon3  32226  dfrdg4  32285  poimirlem18  33659  poimirlem21  33662  orsild  34121  orsird  34122  notornotel1  34129  cvrat4  35149  hdmaplem4  37482  mapdh9a  37498  fnwe2lem2  38040  ifpnot23  38242  ifpim123g  38264  df3or2  38479  3ornot23VD  39498  ndisj2  39634  xrssre  39979  icccncfext  40520  fourierdlem42  40786  fourierdlem92  40835  salexct2  40977  nnfoctbdjlem  41092  afvfv0bi  41655  ltnltne  41740  lighneallem4  41954  oddprmALTV  42025  mndpsuppss  42579
 Copyright terms: Public domain W3C validator