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

Theorem ianor 507
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 (¬ (𝜑𝜓) ↔ (¬ 𝜑 ∨ ¬ 𝜓))

Proof of Theorem ianor
StepHypRef Expression
1 imnan 436 . 2 ((𝜑 → ¬ 𝜓) ↔ ¬ (𝜑𝜓))
2 pm4.62 433 . 2 ((𝜑 → ¬ 𝜓) ↔ (¬ 𝜑 ∨ ¬ 𝜓))
31, 2bitr3i 264 1 (¬ (𝜑𝜓) ↔ (¬ 𝜑 ∨ ¬ 𝜓))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 194  wo 381  wa 382
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 195  df-or 383  df-an 384
This theorem is referenced by:  anor  508  3anor  1046  cadnot  1544  19.33b  1801  neorian  2875  indifdir  3841  tpprceq3  4275  tppreqb  4276  prneimg  4323  prnebg  4324  opthneg  4869  fr2nr  5005  xpeq0  5458  difxp  5462  ordtri3or  5657  imadif  5872  fvfundmfvn0  6120  ftpg  6305  2mpt20  6757  bropopvvv  7119  bropfvvvv  7121  frxp  7151  soxp  7154  ressuppssdif  7180  mpt2xneldm  7202  dfsup2  8210  suc11reg  8376  rankxplim3  8604  kmlem3  8834  cdainflem  8873  isfin5-2  9073  mulge0b  10744  nn0n0n1ge2b  11208  rpneg  11697  mul2lt0bi  11770  xrrebnd  11834  xmullem2  11926  difreicc  12133  fz0  12184  nelfzo  12301  injresinj  12408  hashunx  12990  swrdnd  13232  repswswrd  13330  dfgcd2  15049  ncoprmlnprm  15222  firest  15864  xpcbas  16589  symgfix2  17607  gsumdixp  18380  0ringnnzr  19038  mplsubrglem  19208  symgmatr01lem  20225  ppttop  20568  fin1aufil  21493  mbfmax  23166  mdegleb  23572  coemulhi  23758  usgraedgprv  25698  usgraedgrnv  25699  usgraidx2v  25715  cusgrares  25794  cusgrasizeindslem1  25795  2pthlem2  25919  clwwlknprop  26093  2wlkonot3v  26195  2spthonot3v  26196  vdgrf  26218  clwlknclwlkdifs  26280  1to2vfriswmgra  26326  frgrawopreglem3  26366  2spotiundisj  26382  numclwwlk3lem  26428  atcvati  28422  ofpreima2  28642  ordtconlem1  29091  aean  29427  sitgaddlemb  29530  ballotlemodife  29679  bnj1174  30118  erdszelem10  30229  dfon2lem4  30728  nodenselem4  30876  poimirlem30  32392  poimirlem31  32393  itg2addnclem  32414  itg2addnclem2  32415  itg2addnclem3  32416  iblabsnclem  32426  ftc1anclem3  32440  areacirclem4  32456  lsatcvat  33138  lkreqN  33258  cvrat  33509  4atlem3  33683  paddasslem17  33923  llnexchb2  33956  dalawlem14  33971  cdleme0nex  34378  lclkrlem2o  35611  lcfrlem19  35651  ifpnot23  36625  ifpim123g  36647  rp-fakenanass  36662  ntrneineine1lem  37185  stoweidlem14  38690  stoweidlem26  38702  afvco2  39689  nltle2tri  39726  evennodd  39878  oddneven  39879  xnn0xaddcl  40194  usgredg2v  40435  clwwlknclwwlkdifs  41162  trlsegvdeg  41376  1to2vfriswmgr  41430  frgrwopreglem3  41464  av-numclwwlk3lem  41519  lindslinindsimp1  42021  lindslinindsimp2  42027
  Copyright terms: Public domain W3C validator