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

Theorem ianor 488
Description: Negated conjunction in terms of disjunction (De Morgan's law). Theorem *4.51 of [WhiteheadRussell] p. 120. (Contributed by NM, 14-May-1993.) (Proof shortened by Andrew Salmon, 13-May-2011.)
Assertion
Ref Expression
ianor  |-  ( -.  ( ph  /\  ps ) 
<->  ( -.  ph  \/  -.  ps ) )

Proof of Theorem ianor
StepHypRef Expression
1 imnan 422 . 2  |-  ( (
ph  ->  -.  ps )  <->  -.  ( ph  /\  ps ) )
2 pm4.62 419 . 2  |-  ( (
ph  ->  -.  ps )  <->  ( -.  ph  \/  -.  ps ) )
31, 2bitr3i 251 1  |-  ( -.  ( ph  /\  ps ) 
<->  ( -.  ph  \/  -.  ps ) )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 184    \/ wo 368    /\ wa 369
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371
This theorem is referenced by:  anor  489  3anor  981  cadnot  1437  thema1a  1580  19.33b  1664  neorian  2779  indifdir  3715  tpprceq3  4122  tppreqb  4123  prneimg  4162  prnebg  4163  opthneg  4680  fr2nr  4807  ordtri3or  4860  suc11  4931  xpeq0  5367  difxp  5371  imadif  5602  fvfundmfvn0  5832  ftpg  6002  bropopvvv  6764  frxp  6793  soxp  6796  ressuppssdif  6821  dfsup2  7804  suc11reg  7937  rankxplim3  8200  kmlem3  8433  cdainflem  8472  isfin5-2  8672  mulge0b  10311  nn0n0n1ge2b  10756  rpneg  11132  xrrebnd  11252  xmullem2  11340  difreicc  11535  fz0  11583  injresinj  11757  hashunx  12268  wrdsymb0  12378  repswswrd  12541  firest  14491  xpcbas  15108  symgfix2  16041  gsumdixpOLD  16824  gsumdixp  16825  mplsubrglem  17642  mplsubrglemOLD  17643  symgmatr01lem  18592  ppttop  18744  fin1aufil  19638  mbfmax  21261  mdegleb  21669  coemulhi  21855  usgraedgprv  23448  usgraedgrnv  23449  usgraidx2v  23464  cusgrares  23533  cusgrasizeindslem2  23535  2pthlem2  23648  vdgrf  23721  atcvati  25943  ofpreima2  26137  mul2lt0bi  26194  ordtconlem1  26500  aean  26805  ballotlemodife  27025  erdszelem10  27233  dfon2lem4  27744  nodenselem4  27970  dvtanlem  28590  itg2addnclem  28592  itg2addnclem2  28593  itg2addnclem3  28594  iblabsnclem  28604  ftc1anclem3  28618  areacirclem4  28636  stoweidlem14  29958  stoweidlem26  29970  afvco2  30231  2wlkonot3v  30543  2spthonot3v  30544  clwwlknprop  30584  clwlknclwlkdifs  30727  1to2vfriswmgra  30747  frgrawopreglem3  30788  2spotiundisj  30804  numclwwlk3lem  30850  0rngnnzr  30927  lindslinindsimp1  31124  lindslinindsimp2  31130  bnj1174  32327  lsatcvat  33034  lkreqN  33154  cvrat  33405  4atlem3  33579  paddasslem17  33819  llnexchb2  33852  dalawlem14  33867  cdleme0nex  34273  lclkrlem2o  35505  lcfrlem19  35545
  Copyright terms: Public domain W3C validator