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  1880  2ralor  2682  dfun2  3365  sotrieq2  4300  somo  4306  ordnbtwn  4441  dflim3  4596  frxp  6145  poxp  6147  soxp  6148  oalimcl  6512  omlimcl  6530  oeeulem  6553  domunfican  7083  dfsup2OLD  7150  ordtypelem7  7193  cantnfp1lem2  7335  cantnfp1lem3  7336  cantnflem1  7345  cnfcom2lem  7358  ssfin4  7890  fin1a2lem7  7986  fin1a2lem12  7991  fpwwe2lem13  8218  fpwwe2  8219  r1wunlim  8313  1re  8791  recgt0  9554  elnnz  9987  xrltlen  10433  xaddf  10503  xmullem  10536  xmullem2  10537  om2uzf1oi  10968  bcval4  11272  sadcaddlem  12596  isprm3  12715  pcpremul  12844  subgmulg  14583  isnirred  15430  isdomn2  15988  ordtbaslem  16866  iuncon  17102  fbun  17483  fin1aufil  17575  reconnlem2  18280  pmltpc  18758  itg2splitlem  19051  mdegmullem  19412  atans2  20175  leibpilem2  20185  leibpi  20186  wilthlem2  20255  lgsdir2  20515  nonbooli  22194  cvnbtwn4  22815  chirredi  22920  atcvat4i  22923  erdszelem9  23088  3orit  23424  axfelem18  23718  dfon3  23794  dfrdg4  23849  albineal  24351  fnwe2lem2  26501  3ornot23VD  27657  bnj1304  27885  bnj1417  28104  cvrat4  28783  hdmaplem4  31115  mapdh9a  31131
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