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

Theorem ianor 496
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 429 . 2  |-  ( (
ph  ->  -.  ps )  <->  -.  ( ph  /\  ps ) )
2 pm4.62 426 . 2  |-  ( (
ph  ->  -.  ps )  <->  ( -.  ph  \/  -.  ps ) )
31, 2bitr3i 259 1  |-  ( -.  ( ph  /\  ps ) 
<->  ( -.  ph  \/  -.  ps ) )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 189    \/ wo 375    /\ wa 376
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 190  df-or 377  df-an 378
This theorem is referenced by:  anor  497  3anor  1023  cadnot  1526  stoic1aOLD  1664  19.33b  1756  neorian  2737  indifdir  3690  tpprceq3  4103  tppreqb  4104  prneimg  4148  prnebg  4149  opthneg  4681  fr2nr  4817  xpeq0  5263  difxp  5267  ordtri3or  5462  suc11  5533  imadif  5668  fvfundmfvn0  5911  ftpg  6090  bropopvvv  6893  bropfvvvv  6895  frxp  6925  soxp  6928  ressuppssdif  6955  mpt2xneldm  6977  dfsup2  7976  suc11reg  8142  rankxplim3  8370  kmlem3  8600  cdainflem  8639  isfin5-2  8839  mulge0b  10497  nn0n0n1ge2b  10957  rpneg  11355  mul2lt0bi  11425  xrrebnd  11486  xmullem2  11576  difreicc  11790  fz0  11840  nelfzo  11952  injresinj  12057  hashunx  12603  swrdnd  12842  repswswrd  12941  ncoprmlnprm  14756  firest  15409  xpcbas  16141  symgfix2  17135  gsumdixp  17915  0ringnnzr  18570  mplsubrglem  18740  symgmatr01lem  19755  ppttop  20099  fin1aufil  21025  mbfmax  22684  mdegleb  23092  coemulhi  23287  usgraedgprv  25182  usgraedgrnv  25183  usgraidx2v  25199  cusgrares  25279  cusgrasizeindslem2  25281  2pthlem2  25405  clwwlknprop  25579  2wlkonot3v  25682  2spthonot3v  25683  vdgrf  25705  clwlknclwlkdifs  25767  1to2vfriswmgra  25813  frgrawopreglem3  25853  2spotiundisj  25869  numclwwlk3lem  25915  atcvati  28120  ofpreima2  28344  ordtconlem1  28804  aean  29140  sitgaddlemb  29254  ballotlemodife  29403  bnj1174  29884  erdszelem10  29995  dfon2lem4  30503  nodenselem4  30644  poimirlem30  32034  poimirlem31  32035  dvtanlemOLD  32055  itg2addnclem  32057  itg2addnclem2  32058  itg2addnclem3  32059  iblabsnclem  32069  ftc1anclem3  32083  areacirclem4  32099  lsatcvat  32687  lkreqN  32807  cvrat  33058  4atlem3  33232  paddasslem17  33472  llnexchb2  33505  dalawlem14  33520  cdleme0nex  33927  lclkrlem2o  35160  lcfrlem19  35200  ifpnot23  36193  ifpim123g  36215  rp-fakenanass  36230  stoweidlem14  37986  stoweidlem26  37998  afvco2  38823  nltle2tri  38861  evennodd  38918  oddneven  38919  xnn0xaddcl  39236  usgredg2v  39468  trlsegvdeg  40139  usgedgvadf1  40235  usgedgvadf1ALT  40238  lindslinindsimp1  40758  lindslinindsimp2  40764
  Copyright terms: Public domain W3C validator