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  990  cadnot  1449  stoic1a  1592  19.33b  1683  neorian  2770  indifdir  3739  tpprceq3  4155  tppreqb  4156  prneimg  4196  prnebg  4197  opthneg  4716  fr2nr  4847  ordtri3or  4900  suc11  4971  xpeq0  5417  difxp  5421  imadif  5653  fvfundmfvn0  5888  ftpg  6066  bropopvvv  6865  frxp  6895  soxp  6898  ressuppssdif  6923  dfsup2  7904  suc11reg  8039  rankxplim3  8302  kmlem3  8535  cdainflem  8574  isfin5-2  8774  mulge0b  10419  nn0n0n1ge2b  10867  rpneg  11259  xrrebnd  11379  xmullem2  11467  difreicc  11662  fz0  11711  injresinj  11907  hashunx  12435  wrdsymb0  12556  repswswrd  12737  firest  14811  xpcbas  15425  symgfix2  16419  gsumdixpOLD  17235  gsumdixp  17236  0ringnnzr  17895  mplsubrglem  18078  mplsubrglemOLD  18079  symgmatr01lem  19132  ppttop  19485  fin1aufil  20410  mbfmax  22033  mdegleb  22441  coemulhi  22627  usgraedgprv  24352  usgraedgrnv  24353  usgraidx2v  24369  cusgrares  24448  cusgrasizeindslem2  24450  2pthlem2  24574  clwwlknprop  24748  2wlkonot3v  24851  2spthonot3v  24852  vdgrf  24874  clwlknclwlkdifs  24936  1to2vfriswmgra  24982  frgrawopreglem3  25022  2spotiundisj  25038  numclwwlk3lem  25084  atcvati  27281  ofpreima2  27484  mul2lt0bi  27545  ordtconlem1  27883  aean  28193  ballotlemodife  28413  erdszelem10  28621  dfon2lem4  29193  nodenselem4  29419  dvtanlem  30039  itg2addnclem  30041  itg2addnclem2  30042  itg2addnclem3  30043  iblabsnclem  30053  ftc1anclem3  30067  areacirclem4  30085  stoweidlem14  31685  stoweidlem26  31697  afvco2  32099  usgedgvadf1  32253  usgedgvadf1ALT  32256  lindslinindsimp1  32793  lindslinindsimp2  32799  bnj1174  33792  lsatcvat  34515  lkreqN  34635  cvrat  34886  4atlem3  35060  paddasslem17  35300  llnexchb2  35333  dalawlem14  35348  cdleme0nex  35755  lclkrlem2o  36988  lcfrlem19  37028  rp-fakenanass  37442
  Copyright terms: Public domain W3C validator