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

Theorem ioran 510
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 195  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 196  df-or 384  df-an 385
This theorem is referenced by:  pm4.56  515  xor  931  3ioran  1049  3ori  1380  ecase23d  1428  19.43OLD  1800  2ralor  3088  dfun2  3821  prnebg  4329  sotrieq2  4987  somo  4993  ordnbtwnOLD  5734  dflim3  6939  frxp  7174  poxp  7176  soxp  7177  oalimcl  7527  omlimcl  7545  oeeulem  7568  domunfican  8118  ordtypelem7  8312  cantnfp1lem2  8459  cantnfp1lem3  8460  cantnflem1  8469  cnfcom2lem  8481  ssfin4  9015  fin1a2lem7  9111  fin1a2lem12  9116  fpwwe2lem13  9343  fpwwe2  9344  r1wunlim  9438  1re  9918  recgt0  10746  elnnz  11264  xrltlen  11855  xaddf  11929  xmullem  11966  xmullem2  11967  ssfzoulel  12428  elfznelfzo  12439  elfznelfzob  12440  om2uzf1oi  12614  fsuppmapnn0fiubex  12654  bcval4  12956  sadcaddlem  15017  lcmcllem  15147  lcmgcdlem  15157  lcmftp  15187  lcmfunsnlem2lem1  15189  lcmfunsnlem2lem2  15190  lcmfunsnlem2  15191  isprm3  15234  prm23ge5  15358  pcpremul  15386  subgmulg  17431  isnirred  18523  isdomn2  19120  mdetunilem7  20243  mndifsplit  20261  ordtbaslem  20802  iuncon  21041  fbun  21454  fin1aufil  21546  reconnlem2  22438  rrxmvallem  22995  pmltpc  23026  itg2splitlem  23321  mdegmullem  23642  atans2  24458  leibpilem2  24468  leibpi  24469  wilthlem2  24595  lgsdir2  24855  2lgslem3  24929  ragncol  25404  opptgdim2  25437  hlpasch  25448  trgcopy  25496  cgrg3col4  25534  structiedg0val  25699  usgraidx2v  25922  nbgra0nb  25958  nb3graprlem2  25981  frgra2v  26526  frgrareg  26644  nonbooli  27894  cvnbtwn4  28532  chirredi  28637  atcvat4i  28640  bnj1304  30144  bnj1417  30363  erdszelem9  30435  3orit  30851  nofulllem5  31105  dfon3  31169  dfrdg4  31228  poimirlem18  32597  poimirlem21  32600  orsild  33059  orsird  33060  notornotel1  33067  cvrat4  33747  hdmaplem4  36081  mapdh9a  36097  fnwe2lem2  36639  ifpnot23  36842  ifpim123g  36864  df3or2  37079  3ornot23VD  38104  ndisj2  38243  xrssre  38505  icccncfext  38773  fourierdlem42  39042  fourierdlem92  39091  salexct2  39233  nnfoctbdjlem  39348  afvfv0bi  39881  lighneallem4  40065  oddprmALTV  40136  ltnltne  40345  usgredg2v  40454  nb3grprlem2  40609  vtxd0nedgb  40703  1egrvtxdg0  40727  wwlksnndef  41111  wwlksnfi  41112  clwwlksnndef  41198  nfrgr2v  41442  mndpsuppss  41946
  Copyright terms: Public domain W3C validator