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

Theorem ioran 477
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 417 . 2  |-  ( -.  ( -.  ph  ->  ps )  <->  ( -.  ph  /\ 
-.  ps ) )
2 pm4.64 362 . 2  |-  ( ( -.  ph  ->  ps )  <->  (
ph  \/  ps )
)
31, 2xchnxbi 300 1  |-  ( -.  ( ph  \/  ps ) 
<->  ( -.  ph  /\  -.  ps ) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 177    \/ wo 358    /\ wa 359
This theorem is referenced by:  pm4.56  482  oibabs  852  xor  862  3ioran  952  3ori  1244  ecase23d  1287  19.43OLD  1616  equviniOLD  2080  2ralor  2869  dfun2  3568  prnebg  3971  sotrieq2  4523  somo  4529  ordnbtwn  4664  dflim3  4819  frxp  6448  poxp  6450  soxp  6451  oalimcl  6795  omlimcl  6813  oeeulem  6836  domunfican  7371  dfsup2OLD  7440  ordtypelem7  7485  cantnfp1lem2  7627  cantnfp1lem3  7628  cantnflem1  7637  cnfcom2lem  7650  ssfin4  8182  fin1a2lem7  8278  fin1a2lem12  8283  fpwwe2lem13  8509  fpwwe2  8510  r1wunlim  8604  1re  9082  recgt0  9846  elnnz  10284  xrltlen  10731  xaddf  10802  xmullem  10835  xmullem2  10836  elfznelfzo  11184  elfznelfzob  11185  om2uzf1oi  11285  bcval4  11590  sadcaddlem  12961  isprm3  13080  pcpremul  13209  subgmulg  14950  isnirred  15797  isdomn2  16351  ordtbaslem  17244  iuncon  17483  fbun  17864  fin1aufil  17956  reconnlem2  18850  pmltpc  19339  itg2splitlem  19632  mdegmullem  19993  atans2  20763  leibpilem2  20773  leibpi  20774  wilthlem2  20844  lgsdir2  21104  usgraidx2v  21404  nbgra0nb  21433  nb3graprlem2  21453  nonbooli  23145  cvnbtwn4  23784  chirredi  23889  atcvat4i  23892  erdszelem9  24877  3orit  25161  nofulllem5  25653  dfon3  25729  dfrdg4  25787  dvreasin  26270  fnwe2lem2  27107  afvfv0bi  27973  ltnltne  28069  swrdnd  28144  swrdvalodmlem1  28149  cshwssizelem2  28234  3ornot23VD  28886  bnj1304  29118  bnj1417  29337  equviniNEW7  29454  cvrat4  30167  hdmaplem4  32499  mapdh9a  32515
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 178  df-or 360  df-an 361
  Copyright terms: Public domain W3C validator