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

Theorem ianor 475
Description: Negated conjunction in terms of disjunction (De Morgan's law). Theorem *4.51 of [WhiteheadRussell] p. 120. (Contributed by NM, 5-Aug-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 412 . 2  |-  ( (
ph  ->  -.  ps )  <->  -.  ( ph  /\  ps ) )
2 pm4.62 409 . 2  |-  ( (
ph  ->  -.  ps )  <->  ( -.  ph  \/  -.  ps ) )
31, 2bitr3i 243 1  |-  ( -.  ( ph  /\  ps ) 
<->  ( -.  ph  \/  -.  ps ) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 177    \/ wo 358    /\ wa 359
This theorem is referenced by:  anor  476  3anor  950  cadnot  1400  19.33b  1615  neorian  2658  indifdir  3561  tpprceq3  3902  tppreqb  3903  prneimg  3942  prnebg  3943  fr2nr  4524  ordtri3or  4577  suc11  4648  xpeq0  5256  imadif  5491  fvfundmfvn0  5725  ftpg  5879  difxp  6343  bropopvvv  6389  frxp  6419  soxp  6422  dfsup2  7409  suc11reg  7534  rankxplim3  7765  kmlem3  7992  cdainflem  8031  isfin5-2  8231  nn0n0n1ge2b  10241  rpneg  10601  xrrebnd  10716  xmullem2  10804  difreicc  10988  injresinj  11159  hashunx  11619  firest  13619  xpcbas  14234  gsumdixp  15674  mplsubrglem  16461  ppttop  17030  fin1aufil  17921  mbfmax  19498  mdegleb  19944  coemulhi  20129  usgraedgprv  21353  usgraedgrnv  21354  usgraidx2v  21369  cusgrares  21438  cusgrasizeindslem2  21440  2pthlem2  21553  vdgrf  21626  atcvati  23846  aean  24552  sibfof  24611  ballotlemodife  24712  erdszelem10  24843  mulge0b  25148  dfon2lem4  25360  nodenselem4  25556  itg2addnclem  26159  itg2addnclem2  26160  itg2addnclem3  26161  iblabsnclem  26171  areacirclem5  26189  stoweidlem14  27634  stoweidlem26  27646  afvco2  27911  2wlkonot3v  28076  2spthonot3v  28077  1to2vfriswmgra  28114  frgrawopreglem3  28153  2spotiundisj  28169  bnj1174  29082  lsatcvat  29537  lkreqN  29657  cvrat  29908  4atlem3  30082  paddasslem17  30322  llnexchb2  30355  dalawlem14  30370  cdleme0nex  30776  lclkrlem2o  32008  lcfrlem19  32048
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361
  Copyright terms: Public domain W3C validator