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 (De Morgan'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  1596  equvini  1940  2ralor  2722  dfun2  3417  sotrieq2  4358  somo  4364  ordnbtwn  4499  dflim3  4654  frxp  6241  poxp  6243  soxp  6244  oalimcl  6574  omlimcl  6592  oeeulem  6615  domunfican  7145  dfsup2OLD  7212  ordtypelem7  7255  cantnfp1lem2  7397  cantnfp1lem3  7398  cantnflem1  7407  cnfcom2lem  7420  ssfin4  7952  fin1a2lem7  8048  fin1a2lem12  8053  fpwwe2lem13  8280  fpwwe2  8281  r1wunlim  8375  1re  8853  recgt0  9616  elnnz  10050  xrltlen  10496  xaddf  10567  xmullem  10600  xmullem2  10601  om2uzf1oi  11032  bcval4  11336  sadcaddlem  12664  isprm3  12783  pcpremul  12912  subgmulg  14651  isnirred  15498  isdomn2  16056  ordtbaslem  16934  iuncon  17170  fbun  17551  fin1aufil  17643  reconnlem2  18348  pmltpc  18826  itg2splitlem  19119  mdegmullem  19480  atans2  20243  leibpilem2  20253  leibpi  20254  wilthlem2  20323  lgsdir2  20583  nonbooli  22246  cvnbtwn4  22885  chirredi  22990  atcvat4i  22993  erdszelem9  23745  3orit  24081  nofulllem5  24431  dfon3  24503  dfrdg4  24560  dvreasin  25026  albineal  25102  fnwe2lem2  27251  afvfv0bi  28120  elfznelfzo  28213  nbgra0nb  28278  nb3graprlem2  28288  3ornot23VD  28939  bnj1304  29168  bnj1417  29387  equviniNEW7  29502  cvrat4  30254  hdmaplem4  32586  mapdh9a  32602
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