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  984  cadnot  1441  thema1a  1584  19.33b  1668  neorian  2787  indifdir  3747  tpprceq3  4160  tppreqb  4161  prneimg  4200  prnebg  4201  opthneg  4719  fr2nr  4850  ordtri3or  4903  suc11  4974  xpeq0  5418  difxp  5422  imadif  5654  fvfundmfvn0  5889  ftpg  6062  bropopvvv  6853  frxp  6883  soxp  6886  ressuppssdif  6911  dfsup2  7891  suc11reg  8025  rankxplim3  8288  kmlem3  8521  cdainflem  8560  isfin5-2  8760  mulge0b  10401  nn0n0n1ge2b  10849  rpneg  11238  xrrebnd  11358  xmullem2  11446  difreicc  11641  fz0  11690  injresinj  11883  hashunx  12409  wrdsymb0  12527  repswswrd  12706  firest  14677  xpcbas  15294  symgfix2  16229  gsumdixpOLD  17034  gsumdixp  17035  mplsubrglem  17864  mplsubrglemOLD  17865  symgmatr01lem  18915  ppttop  19267  fin1aufil  20161  mbfmax  21784  mdegleb  22192  coemulhi  22378  usgraedgprv  24038  usgraedgrnv  24039  usgraidx2v  24055  cusgrares  24134  cusgrasizeindslem2  24136  2pthlem2  24260  clwwlknprop  24434  2wlkonot3v  24537  2spthonot3v  24538  vdgrf  24560  clwlknclwlkdifs  24622  1to2vfriswmgra  24668  frgrawopreglem3  24709  2spotiundisj  24725  numclwwlk3lem  24771  atcvati  26967  ofpreima2  27166  mul2lt0bi  27223  ordtconlem1  27528  aean  27842  ballotlemodife  28062  erdszelem10  28270  dfon2lem4  28781  nodenselem4  29007  dvtanlem  29628  itg2addnclem  29630  itg2addnclem2  29631  itg2addnclem3  29632  iblabsnclem  29642  ftc1anclem3  29656  areacirclem4  29674  stoweidlem14  31269  stoweidlem26  31281  afvco2  31683  usgedgvadf1  31817  usgedgvadf1ALT  31820  0rngnnzr  31906  lindslinindsimp1  32006  lindslinindsimp2  32012  bnj1174  33013  lsatcvat  33722  lkreqN  33842  cvrat  34093  4atlem3  34267  paddasslem17  34507  llnexchb2  34540  dalawlem14  34555  cdleme0nex  34961  lclkrlem2o  36193  lcfrlem19  36233
  Copyright terms: Public domain W3C validator