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  1613  equviniOLD  2041  2ralor  2837  dfun2  3536  prnebg  3939  sotrieq2  4491  somo  4497  ordnbtwn  4631  dflim3  4786  frxp  6415  poxp  6417  soxp  6418  oalimcl  6762  omlimcl  6780  oeeulem  6803  domunfican  7338  dfsup2OLD  7406  ordtypelem7  7449  cantnfp1lem2  7591  cantnfp1lem3  7592  cantnflem1  7601  cnfcom2lem  7614  ssfin4  8146  fin1a2lem7  8242  fin1a2lem12  8247  fpwwe2lem13  8473  fpwwe2  8474  r1wunlim  8568  1re  9046  recgt0  9810  elnnz  10248  xrltlen  10695  xaddf  10766  xmullem  10799  xmullem2  10800  elfznelfzo  11147  elfznelfzob  11148  om2uzf1oi  11248  bcval4  11553  sadcaddlem  12924  isprm3  13043  pcpremul  13172  subgmulg  14913  isnirred  15760  isdomn2  16314  ordtbaslem  17206  iuncon  17444  fbun  17825  fin1aufil  17917  reconnlem2  18811  pmltpc  19300  itg2splitlem  19593  mdegmullem  19954  atans2  20724  leibpilem2  20734  leibpi  20735  wilthlem2  20805  lgsdir2  21065  usgraidx2v  21365  nbgra0nb  21394  nb3graprlem2  21414  nonbooli  23106  cvnbtwn4  23745  chirredi  23850  atcvat4i  23853  erdszelem9  24838  3orit  25122  nofulllem5  25574  dfon3  25646  dfrdg4  25703  dvreasin  26179  fnwe2lem2  27016  afvfv0bi  27883  swrdnd  28001  3ornot23VD  28668  bnj1304  28897  bnj1417  29116  equviniNEW7  29231  cvrat4  29925  hdmaplem4  32257  mapdh9a  32273
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