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

Theorem ianor 491
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 424 . 2  |-  ( (
ph  ->  -.  ps )  <->  -.  ( ph  /\  ps ) )
2 pm4.62 421 . 2  |-  ( (
ph  ->  -.  ps )  <->  ( -.  ph  \/  -.  ps ) )
31, 2bitr3i 255 1  |-  ( -.  ( ph  /\  ps ) 
<->  ( -.  ph  \/  -.  ps ) )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 188    \/ wo 370    /\ wa 371
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 189  df-or 372  df-an 373
This theorem is referenced by:  anor  492  3anor  1001  cadnot  1518  stoic1aOLD  1656  19.33b  1748  neorian  2718  indifdir  3699  tpprceq3  4112  tppreqb  4113  prneimg  4156  prnebg  4157  opthneg  4681  fr2nr  4812  xpeq0  5257  difxp  5261  ordtri3or  5455  suc11  5526  imadif  5658  fvfundmfvn0  5897  ftpg  6074  bropopvvv  6874  bropfvvvv  6876  frxp  6906  soxp  6909  ressuppssdif  6936  mpt2xneldm  6958  dfsup2  7958  suc11reg  8124  rankxplim3  8352  kmlem3  8582  cdainflem  8621  isfin5-2  8821  mulge0b  10475  nn0n0n1ge2b  10933  rpneg  11332  mul2lt0bi  11402  xrrebnd  11463  xmullem2  11551  difreicc  11764  fz0  11814  nelfzo  11925  injresinj  12025  hashunx  12565  swrdnd  12788  repswswrd  12887  ncoprmlnprm  14677  firest  15331  xpcbas  16063  symgfix2  17057  gsumdixp  17837  0ringnnzr  18493  mplsubrglem  18663  symgmatr01lem  19678  ppttop  20022  fin1aufil  20947  mbfmax  22605  mdegleb  23013  coemulhi  23208  usgraedgprv  25103  usgraedgrnv  25104  usgraidx2v  25120  cusgrares  25200  cusgrasizeindslem2  25202  2pthlem2  25326  clwwlknprop  25500  2wlkonot3v  25603  2spthonot3v  25604  vdgrf  25626  clwlknclwlkdifs  25688  1to2vfriswmgra  25734  frgrawopreglem3  25774  2spotiundisj  25790  numclwwlk3lem  25836  atcvati  28039  ofpreima2  28269  ordtconlem1  28730  aean  29067  sitgaddlemb  29181  ballotlemodife  29330  bnj1174  29812  erdszelem10  29923  dfon2lem4  30432  nodenselem4  30573  poimirlem30  31970  poimirlem31  31971  dvtanlemOLD  31991  itg2addnclem  31993  itg2addnclem2  31994  itg2addnclem3  31995  iblabsnclem  32005  ftc1anclem3  32019  areacirclem4  32035  lsatcvat  32616  lkreqN  32736  cvrat  32987  4atlem3  33161  paddasslem17  33401  llnexchb2  33434  dalawlem14  33449  cdleme0nex  33856  lclkrlem2o  35089  lcfrlem19  35129  ifpnot23  36122  ifpim123g  36144  rp-fakenanass  36159  stoweidlem14  37874  stoweidlem26  37886  afvco2  38678  nltle2tri  38716  evennodd  38773  oddneven  38774  xnn0xaddcl  39086  usgredg2v  39304  usgedgvadf1  39780  usgedgvadf1ALT  39783  lindslinindsimp1  40303  lindslinindsimp2  40309
  Copyright terms: Public domain W3C validator