MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ioran 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  4663  dflim3  4818  frxp  6447  poxp  6449  soxp  6450  oalimcl  6794  omlimcl  6812  oeeulem  6835  domunfican  7370  dfsup2OLD  7439  ordtypelem7  7482  cantnfp1lem2  7624  cantnfp1lem3  7625  cantnflem1  7634  cnfcom2lem  7647  ssfin4  8179  fin1a2lem7  8275  fin1a2lem12  8280  fpwwe2lem13  8506  fpwwe2  8507  r1wunlim  8601  1re  9079  recgt0  9843  elnnz  10281  xrltlen  10728  xaddf  10799  xmullem  10832  xmullem2  10833  elfznelfzo  11180  elfznelfzob  11181  om2uzf1oi  11281  bcval4  11586  sadcaddlem  12957  isprm3  13076  pcpremul  13205  subgmulg  14946  isnirred  15793  isdomn2  16347  ordtbaslem  17240  iuncon  17479  fbun  17860  fin1aufil  17952  reconnlem2  18846  pmltpc  19335  itg2splitlem  19628  mdegmullem  19989  atans2  20759  leibpilem2  20769  leibpi  20770  wilthlem2  20840  lgsdir2  21100  usgraidx2v  21400  nbgra0nb  21429  nb3graprlem2  21449  nonbooli  23141  cvnbtwn4  23780  chirredi  23885  atcvat4i  23888  erdszelem9  24873  3orit  25157  nofulllem5  25615  dfon3  25687  dfrdg4  25745  dvreasin  26226  fnwe2lem2  27063  afvfv0bi  27930  swrdnd  28074  shwrdssizelem2  28167  3ornot23VD  28813  bnj1304  29045  bnj1417  29264  equviniNEW7  29379  cvrat4  30079  hdmaplem4  32411  mapdh9a  32427
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