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

Theorem ianor 1004
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 388 . 2 ((𝜑 → ¬ 𝜓) ↔ ¬ (𝜑𝜓))
2 pm4.62 882 . 2 ((𝜑 → ¬ 𝜓) ↔ (¬ 𝜑 ∨ ¬ 𝜓))
31, 2bitr3i 268 1 (¬ (𝜑𝜓) ↔ (¬ 𝜑 ∨ ¬ 𝜓))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 197  wa 384  wo 873
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 198  df-an 385  df-or 874
This theorem is referenced by:  anor  1005  annotanannotOLD  1034  3anorOLD  1130  3ianor  1132  nanor  1612  nanassOLD  1632  cadnot  1724  19.33b  1984  neorian  3031  indifdir  4048  tpprceq3  4489  tppreqb  4490  prneimg  4539  prnebg  4540  preq12nebg  4549  opthprneg  4551  opthneg  5105  fr2nr  5255  xpeq0  5737  difxp  5741  ordtri3or  5940  imadif  6151  ftpg  6615  2mpt20  7080  bropopvvv  7457  bropfvvvv  7459  frxp  7489  soxp  7492  ressuppssdif  7518  mpt2xneldm  7541  dfsup2  8557  nelaneq  8711  suc11reg  8731  rankxplim3  8959  kmlem3  9227  cdainflem  9266  isfin5-2  9466  mulge0b  11147  nn0n0n1ge2b  11606  rpneg  12061  mul2lt0bi  12134  xrrebnd  12201  xnn0xaddcl  12268  xmullem2  12297  difreicc  12511  fz0  12563  nelfzo  12683  injresinj  12797  hashunx  13377  swrdnd  13634  repswswrd  13808  dfgcd2  15544  ncoprmlnprm  15715  firest  16359  xpcbas  17084  symgfix2  18099  gsumdixp  18876  0ringnnzr  19543  mplsubrglem  19713  symgmatr01lem  20737  ppttop  21091  fin1aufil  22015  zclmncvs  23226  mbfmax  23707  mdegleb  24115  coemulhi  24301  numedglnl  26317  usgredg2v  26397  clwwlknclwwlkdifsOLD  27206  clwwlkn  27264  clwwlkneq0  27269  clwwlknon1nloop  27372  trlsegvdeg  27505  1to2vfriswmgr  27559  numclwwlk3lemOLD  27697  numclwwlk3lem2  27700  atcvati  29701  difrab2  29788  ofpreima2  29916  ordtconnlem1  30417  aean  30754  sitgaddlemb  30857  ballotlemodife  31007  bnj1174  31519  erdszelem10  31630  dfon2lem4  32134  noetalem3  32309  poimirlem30  33863  poimirlem31  33864  itg2addnclem  33884  itg2addnclem2  33885  itg2addnclem3  33886  iblabsnclem  33896  ftc1anclem3  33910  areacirclem4  33926  lsatcvat  35006  lkreqN  35126  cvrat  35378  4atlem3  35552  paddasslem17  35792  llnexchb2  35825  dalawlem14  35840  cdleme0nex  36246  lclkrlem2o  37477  lcfrlem19  37517  ifpnot23  38499  ifpim123g  38521  ntrneineine1lem  39056  stoweidlem14  40868  stoweidlem26  40880  dfatprc  41878  afvco2  41924  ndmafv2nrn  41970  nfunsnafv2  41973  afv2ndeffv0  42008  nltle2tri  42057  evennodd  42232  oddneven  42233  spr0nelg  42395  lindslinindsimp1  42915  lindslinindsimp2  42921
  Copyright terms: Public domain W3C validator