Theorem ioran 490

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

Step	Hyp	Ref	Expression
1		pm4.65 427	. 2
2		pm4.64 372	. 2
3	1, 2	xchnxbi 308	1

Syntax hints:  -.wn 3  ->wi 4  <->wb 184  \/wo 368  /\wa 369

This theorem is referenced by:  pm4.56  495  xor  891  3ioran  991  3ori  1288  ecase23d  1332  19.43OLD  1694  2ralor  3027  dfun2  3732  prnebg  4212  sotrieq2  4833  somo  4839  ordnbtwn  4973  dflim3  6682  frxp  6910  poxp  6912  soxp  6913  oalimcl  7228  omlimcl  7246  oeeulem  7269  domunfican  7813  dfsup2OLD  7923  ordtypelem7  7970  cantnfp1lem2  8119  cantnfp1lem3  8120  cantnflem1  8129  cantnfp1lem2OLD  8145  cantnfp1lem3OLD  8146  cantnflem1OLD  8152  cnfcom2lem  8166  cnfcom2lemOLD  8174  ssfin4  8711  fin1a2lem7  8807  fin1a2lem12  8812  fpwwe2lem13  9041  fpwwe2  9042  r1wunlim  9136  1re  9616  recgt0  10411  elnnz  10899  xrltlen  11381  xaddf  11452  xmullem  11485  xmullem2  11486  ssfzoulel  11906  elfznelfzo  11915  elfznelfzob  11916  om2uzf1oi  12064  fsuppmapnn0fiubex  12098  bcval4  12385  swrdnd  12657  sadcaddlem  14107  isprm3  14226  pcpremul  14367  subgmulg  16215  isnirred  17349  isdomn2  17948  mdetunilem7  19120  mndifsplit  19138  ordtbaslem  19689  iuncon  19929  fbun  20341  fin1aufil  20433  reconnlem2  21332  rrxmvallem  21831  pmltpc  21862  itg2splitlem  22155  mdegmullem  22478  atans2  23262  leibpilem2  23272  leibpi  23273  wilthlem2  23343  lgsdir2  23603  ragncol  24086  opptgdim2  24117  usgraidx2v  24393  nbgra0nb  24429  nb3graprlem2  24452  frgra2v  24999  frgrareg  25117  nonbooli  26569  cvnbtwn4  27208  chirredi  27313  atcvat4i  27316  erdszelem9  28643  3orit  29092  nofulllem5  29466  dfon3  29542  dfrdg4  29600  orsild  30487  orsird  30488  notornotel1  30495  fnwe2lem2  30997  lcmcllem  31202  lcmgcdlem  31212  icccncfext  31690  fourierdlem42  31931  fourierdlem92  31981  afvfv0bi  32237  ltnltne  32321  usgedgvadf1  32415  usgedgvadf1ALT  32418  mndpsuppss  32964  3ornot23VD  33647  bnj1304  33878  bnj1417  34097  cvrat4  35167  hdmaplem4  37501  mapdh9a  37517  bj-ifim123g  37706  bj-ifnot23  37718

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 185  df-or 370  df-an 371