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

Theorem ioran 478
Description: Negated disjunction in terms of conjunction (DeMorgan's law). Compare Theorem *4.56 of [WhiteheadRussell] p. 120. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Andrew Salmon, 7-May-2011.)
Assertion
Ref Expression
ioran  |-  ( -.  ( ph  \/  ps ) 
<->  ( -.  ph  /\  -.  ps ) )

Proof of Theorem ioran
StepHypRef Expression
1 pm4.65 418 . 2  |-  ( -.  ( -.  ph  ->  ps )  <->  ( -.  ph  /\ 
-.  ps ) )
2 pm4.64 363 . 2  |-  ( ( -.  ph  ->  ps )  <->  (
ph  \/  ps )
)
31, 2xchnxbi 301 1  |-  ( -.  ( ph  \/  ps ) 
<->  ( -.  ph  /\  -.  ps ) )
Colors of variables: wff set class
Syntax hints:   -. wn 5    -> wi 6    <-> wb 178    \/ wo 359    /\ wa 360
This theorem is referenced by:  pm4.56  483  oibabs  856  xor  866  3ioran  955  3ori  1247  ecase23d  1290  19.43OLD  1605  equvini  1879  2ralor  2671  dfun2  3311  sotrieq2  4235  somo  4241  ordnbtwn  4376  dflim3  4529  frxp  6077  poxp  6079  soxp  6080  oalimcl  6444  omlimcl  6462  oeeulem  6485  domunfican  7014  dfsup2OLD  7080  ordtypelem7  7123  cantnfp1lem2  7265  cantnfp1lem3  7266  cantnflem1  7275  cnfcom2lem  7288  ssfin4  7820  fin1a2lem7  7916  fin1a2lem12  7921  fpwwe2lem13  8144  fpwwe2  8145  r1wunlim  8239  1re  8717  recgt0  9480  elnnz  9913  xrltlen  10359  xaddf  10429  xmullem  10462  xmullem2  10463  om2uzf1oi  10894  bcval4  11198  sadcaddlem  12522  isprm3  12641  pcpremul  12770  subgmulg  14470  isnirred  15317  isdomn2  15872  ordtbaslem  16750  iuncon  16986  fbun  17367  fin1aufil  17459  reconnlem2  18164  pmltpc  18642  itg2splitlem  18935  mdegmullem  19296  atans2  20059  leibpilem2  20069  leibpi  20070  wilthlem2  20139  lgsdir2  20399  nonbooli  22078  cvnbtwn4  22699  chirredi  22804  atcvat4i  22807  erdszelem9  22901  3orit  23237  axfelem18  23531  dfon3  23607  dfrdg4  23662  albineal  24164  fnwe2lem2  26314  3ornot23VD  27313  bnj1304  27541  bnj1417  27760  cvrat4  28321  hdmaplem4  30653  mapdh9a  30669
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362
  Copyright terms: Public domain W3C validator