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  853  xor  863  3ioran  952  3ori  1244  ecase23d  1287  19.43OLD  1594  equvini  1929  2ralor  2710  dfun2  3405  sotrieq2  4341  somo  4347  ordnbtwn  4482  dflim3  4637  frxp  6186  poxp  6188  soxp  6189  oalimcl  6553  omlimcl  6571  oeeulem  6594  domunfican  7124  dfsup2OLD  7191  ordtypelem7  7234  cantnfp1lem2  7376  cantnfp1lem3  7377  cantnflem1  7386  cnfcom2lem  7399  ssfin4  7931  fin1a2lem7  8027  fin1a2lem12  8032  fpwwe2lem13  8259  fpwwe2  8260  r1wunlim  8354  1re  8832  recgt0  9595  elnnz  10029  xrltlen  10475  xaddf  10545  xmullem  10578  xmullem2  10579  om2uzf1oi  11010  bcval4  11314  sadcaddlem  12642  isprm3  12761  pcpremul  12890  subgmulg  14629  isnirred  15476  isdomn2  16034  ordtbaslem  16912  iuncon  17148  fbun  17529  fin1aufil  17621  reconnlem2  18326  pmltpc  18804  itg2splitlem  19097  mdegmullem  19458  atans2  20221  leibpilem2  20231  leibpi  20232  wilthlem2  20301  lgsdir2  20561  nonbooli  22222  cvnbtwn4  22861  chirredi  22966  atcvat4i  22969  erdszelem9  23134  3orit  23470  axfelem18  23764  dfon3  23840  dfrdg4  23895  albineal  24397  fnwe2lem2  26547  afvfv0bi  27392  3ornot23VD  27891  bnj1304  28119  bnj1417  28338  cvrat4  28899  hdmaplem4  31231  mapdh9a  31247
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