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

Theorem ianor 490
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 423 . 2  |-  ( (
ph  ->  -.  ps )  <->  -.  ( ph  /\  ps ) )
2 pm4.62 420 . 2  |-  ( (
ph  ->  -.  ps )  <->  ( -.  ph  \/  -.  ps ) )
31, 2bitr3i 254 1  |-  ( -.  ( ph  /\  ps ) 
<->  ( -.  ph  \/  -.  ps ) )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 187    \/ wo 369    /\ wa 370
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 188  df-or 371  df-an 372
This theorem is referenced by:  anor  491  3anor  998  cadnot  1513  stoic1aOLD  1652  19.33b  1740  neorian  2751  indifdir  3729  tpprceq3  4137  tppreqb  4138  prneimg  4178  prnebg  4179  opthneg  4697  fr2nr  4828  xpeq0  5273  difxp  5277  ordtri3or  5471  suc11  5542  imadif  5673  fvfundmfvn0  5910  ftpg  6086  bropopvvv  6884  frxp  6914  soxp  6917  ressuppssdif  6944  dfsup2  7961  suc11reg  8127  rankxplim3  8354  kmlem3  8583  cdainflem  8622  isfin5-2  8822  mulge0b  10476  nn0n0n1ge2b  10934  rpneg  11333  mul2lt0bi  11403  xrrebnd  11464  xmullem2  11552  difreicc  11765  fz0  11815  nelfzo  11926  injresinj  12025  hashunx  12565  swrdnd  12779  repswswrd  12878  ncoprmlnprm  14665  firest  15319  xpcbas  16051  symgfix2  17045  gsumdixp  17825  0ringnnzr  18481  mplsubrglem  18651  symgmatr01lem  19665  ppttop  20009  fin1aufil  20934  mbfmax  22592  mdegleb  23000  coemulhi  23195  usgraedgprv  25090  usgraedgrnv  25091  usgraidx2v  25107  cusgrares  25186  cusgrasizeindslem2  25188  2pthlem2  25312  clwwlknprop  25486  2wlkonot3v  25589  2spthonot3v  25590  vdgrf  25612  clwlknclwlkdifs  25674  1to2vfriswmgra  25720  frgrawopreglem3  25760  2spotiundisj  25776  numclwwlk3lem  25822  atcvati  28025  ofpreima2  28259  ordtconlem1  28726  aean  29063  sitgaddlemb  29177  ballotlemodife  29326  bnj1174  29808  erdszelem10  29919  dfon2lem4  30427  nodenselem4  30566  poimirlem30  31884  poimirlem31  31885  dvtanlemOLD  31905  itg2addnclem  31907  itg2addnclem2  31908  itg2addnclem3  31909  iblabsnclem  31919  ftc1anclem3  31933  areacirclem4  31949  lsatcvat  32535  lkreqN  32655  cvrat  32906  4atlem3  33080  paddasslem17  33320  llnexchb2  33353  dalawlem14  33368  cdleme0nex  33775  lclkrlem2o  35008  lcfrlem19  35048  ifpnot23  36042  ifpim123g  36064  rp-fakenanass  36079  stoweidlem14  37694  stoweidlem26  37706  afvco2  38390  nltle2tri  38428  evennodd  38485  oddneven  38486  usgridx2v  38930  usgedgvadf1  38999  usgedgvadf1ALT  39002  lindslinindsimp1  39524  lindslinindsimp2  39530
  Copyright terms: Public domain W3C validator