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

Theorem ianor 977
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 400 . 2 ((𝜑 → ¬ 𝜓) ↔ ¬ (𝜑𝜓))
2 pm4.62 852 . 2 ((𝜑 → ¬ 𝜓) ↔ (¬ 𝜑 ∨ ¬ 𝜓))
31, 2bitr3i 278 1 (¬ (𝜑𝜓) ↔ (¬ 𝜑 ∨ ¬ 𝜓))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 207  wa 396  wo 843
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 208  df-an 397  df-or 844
This theorem is referenced by:  anor  978  3ianor  1101  nanor  1481  noranOLD  1520  cadnot  1609  19.33b  1879  neorian  3116  indifdir  4264  2nreu  4396  tpprceq3  4736  tppreqb  4737  prneimg  4784  prnebg  4785  preq12nebg  4792  opthprneg  4794  opthneg  5370  fr2nr  5532  xpeq0  6015  difxp  6019  ordtri3or  6221  imadif  6435  ftpg  6914  2mpo0  7384  bropopvvv  7776  bropfvvvv  7778  frxp  7811  soxp  7814  ressuppssdif  7842  mpoxneldm  7869  dfsup2  8897  nelaneq  9052  suc11reg  9071  rankxplim3  9299  kmlem3  9567  cdainflem  9602  isfin5-2  9802  mulge0b  11499  nn0n0n1ge2b  11952  rpneg  12411  mul2lt0bi  12485  xrrebnd  12551  xnn0xaddcl  12618  xmullem2  12648  difreicc  12860  fz0  12912  nelfzo  13033  injresinj  13148  hashunx  13737  swrdnd  14006  swrdnnn0nd  14008  swrdnd0  14009  repswswrd  14136  dfgcd2  15884  ncoprmlnprm  16058  firest  16696  xpcbas  17418  symgfix2  18464  gsumdixp  19279  0ringnnzr  19961  mplsubrglem  20138  symgmatr01lem  21178  ppttop  21531  fin1aufil  22456  zclmncvs  23667  mbfmax  24165  mdegleb  24573  coemulhi  24759  numedglnl  26843  usgredg2v  26923  clwwlkn  27718  clwwlkneq0  27721  clwwlknon1nloop  27792  trlsegvdeg  27920  1to2vfriswmgr  27972  numclwwlk3lem2  28077  atcvati  30077  difrab2  30175  ofpreima2  30326  hashxpe  30442  ordtconnlem1  31053  aean  31389  sitgaddlemb  31492  ballotlemodife  31641  bnj1174  32159  erdszelem10  32331  satfv1  32494  fmla0disjsuc  32529  fmlasucdisj  32530  dfon2lem4  32915  noetalem3  33103  nrmo  33642  poimirlem30  34789  poimirlem31  34790  itg2addnclem  34810  itg2addnclem2  34811  itg2addnclem3  34812  iblabsnclem  34822  ftc1anclem3  34836  areacirclem4  34852  lsatcvat  36053  lkreqN  36173  cvrat  36425  4atlem3  36599  paddasslem17  36839  llnexchb2  36872  dalawlem14  36887  cdleme0nex  37293  lclkrlem2o  38524  lcfrlem19  38564  ifpnot23  39709  ifpim123g  39731  ntrneineine1lem  40299  stoweidlem14  42165  stoweidlem26  42177  dfatprc  43195  afvco2  43241  ndmafv2nrn  43287  nfunsnafv2  43290  afv2ndeffv0  43325  nltle2tri  43379  ichnreuop  43466  spr0nelg  43470  evennodd  43640  oddneven  43641  lindslinindsimp1  44344  lindslinindsimp2  44350  line2ylem  44570  line2xlem  44572
  Copyright terms: Public domain W3C validator