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

Theorem ioran 476
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 416 . 2  |-  ( -.  ( -.  ph  ->  ps )  <->  ( -.  ph  /\ 
-.  ps ) )
2 pm4.64 361 . 2  |-  ( ( -.  ph  ->  ps )  <->  (
ph  \/  ps )
)
31, 2xchnxbi 299 1  |-  ( -.  ( ph  \/  ps ) 
<->  ( -.  ph  /\  -.  ps ) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 176    \/ wo 357    /\ wa 358
This theorem is referenced by:  pm4.56  481  oibabs  851  xor  861  3ioran  950  3ori  1242  ecase23d  1285  19.43OLD  1593  equvini  1927  2ralor  2709  dfun2  3404  sotrieq2  4342  somo  4348  ordnbtwn  4483  dflim3  4638  frxp  6225  poxp  6227  soxp  6228  oalimcl  6558  omlimcl  6576  oeeulem  6599  domunfican  7129  dfsup2OLD  7196  ordtypelem7  7239  cantnfp1lem2  7381  cantnfp1lem3  7382  cantnflem1  7391  cnfcom2lem  7404  ssfin4  7936  fin1a2lem7  8032  fin1a2lem12  8037  fpwwe2lem13  8264  fpwwe2  8265  r1wunlim  8359  1re  8837  recgt0  9600  elnnz  10034  xrltlen  10480  xaddf  10551  xmullem  10584  xmullem2  10585  om2uzf1oi  11016  bcval4  11320  sadcaddlem  12648  isprm3  12767  pcpremul  12896  subgmulg  14635  isnirred  15482  isdomn2  16040  ordtbaslem  16918  iuncon  17154  fbun  17535  fin1aufil  17627  reconnlem2  18332  pmltpc  18810  itg2splitlem  19103  mdegmullem  19464  atans2  20227  leibpilem2  20237  leibpi  20238  wilthlem2  20307  lgsdir2  20567  nonbooli  22230  cvnbtwn4  22869  chirredi  22974  atcvat4i  22977  erdszelem9  23730  3orit  24066  nofulllem5  24360  dfon3  24432  dfrdg4  24488  dvreasin  24923  albineal  24999  fnwe2lem2  27148  afvfv0bi  28015  nbgra0nb  28144  3ornot23VD  28623  bnj1304  28852  bnj1417  29071  cvrat4  29632  hdmaplem4  31964  mapdh9a  31980
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360
  Copyright terms: Public domain W3C validator