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

Theorem ianor 508
 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 437 . 2 ((𝜑 → ¬ 𝜓) ↔ ¬ (𝜑𝜓))
2 pm4.62 434 . 2 ((𝜑 → ¬ 𝜓) ↔ (¬ 𝜑 ∨ ¬ 𝜓))
31, 2bitr3i 266 1 (¬ (𝜑𝜓) ↔ (¬ 𝜑 ∨ ¬ 𝜓))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 196   ∨ wo 382   ∧ wa 383 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 197  df-or 384  df-an 385 This theorem is referenced by:  anor  509  annotanannotOLD  960  3anorOLD  1072  3ianor  1074  cadnot  1594  19.33b  1853  neorian  2917  indifdir  3916  tpprceq3  4367  tppreqb  4368  prneimg  4419  prnebg  4420  opthneg  4979  fr2nr  5121  xpeq0  5589  difxp  5593  ordtri3or  5793  imadif  6011  fvfundmfvn0  6264  ftpg  6463  2mpt20  6924  bropopvvv  7300  bropfvvvv  7302  frxp  7332  soxp  7335  ressuppssdif  7361  mpt2xneldm  7383  dfsup2  8391  suc11reg  8554  rankxplim3  8782  kmlem3  9012  cdainflem  9051  isfin5-2  9251  mulge0b  10931  nn0n0n1ge2b  11397  rpneg  11901  mul2lt0bi  11974  xrrebnd  12037  xnn0xaddcl  12104  xmullem2  12133  difreicc  12342  fz0  12394  nelfzo  12514  injresinj  12629  hashunx  13213  swrdnd  13478  repswswrd  13577  dfgcd2  15310  ncoprmlnprm  15483  firest  16140  xpcbas  16865  symgfix2  17882  gsumdixp  18655  0ringnnzr  19317  mplsubrglem  19487  symgmatr01lem  20507  ppttop  20859  fin1aufil  21783  zclmncvs  22994  mbfmax  23461  mdegleb  23869  coemulhi  24055  numedglnl  26084  usgredg2v  26164  clwwlknclwwlkdifsOLD  26947  clwwlkn  26985  clwwlkneq0  26990  clwwlknon1nloop  27074  trlsegvdeg  27205  1to2vfriswmgr  27259  numclwwlk3lemOLD  27369  numclwwlk3lem  27371  atcvati  29373  difrab2  29465  ofpreima2  29594  ordtconnlem1  30098  aean  30435  sitgaddlemb  30538  ballotlemodife  30687  bnj1174  31197  erdszelem10  31308  dfon2lem4  31815  noetalem3  31990  poimirlem30  33569  poimirlem31  33570  itg2addnclem  33591  itg2addnclem2  33592  itg2addnclem3  33593  iblabsnclem  33603  ftc1anclem3  33617  areacirclem4  33633  lsatcvat  34655  lkreqN  34775  cvrat  35026  4atlem3  35200  paddasslem17  35440  llnexchb2  35473  dalawlem14  35488  cdleme0nex  35895  lclkrlem2o  37127  lcfrlem19  37167  ifpnot23  38140  ifpim123g  38162  rp-fakenanass  38177  ntrneineine1lem  38699  stoweidlem14  40549  stoweidlem26  40561  afvco2  41577  nltle2tri  41648  evennodd  41881  oddneven  41882  spr0nelg  42051  lindslinindsimp1  42571  lindslinindsimp2  42577
 Copyright terms: Public domain W3C validator