Theorem ianor 979

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

Step	Hyp	Ref	Expression
1		imnan 400	. 2 ⊢ ((𝜑 → ¬ 𝜓) ↔ ¬ (𝜑 ∧ 𝜓))
2		pm4.62 853	. 2 ⊢ ((𝜑 → ¬ 𝜓) ↔ (¬ 𝜑 ∨ ¬ 𝜓))
3	1, 2	bitr3i 276	1 ⊢ (¬ (𝜑 ∧ 𝜓) ↔ (¬ 𝜑 ∨ ¬ 𝜓))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 205   ∧ wa 396   ∨ wo 844

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 206  df-an 397  df-or 845

This theorem is referenced by:  anor  980  3ianor  1106  nanor  1490  cadnot  1617  19.33b  1888  neorian  3039  indifdirOLD  4219  2nreu  4375  tpprceq3  4737  tppreqb  4738  prneimg  4785  prnebg  4786  preq12nebg  4793  opthprneg  4795  opthneg  5396  fr2nr  5567  iresn0n0  5963  xpeq0  6063  difxp  6067  ordtri3or  6298  imadif  6518  ftpg  7028  nf1const  7176  nf1oconst  7177  0mpo0  7358  2mpo0  7518  bropopvvv  7930  bropfvvvv  7932  frxp  7967  soxp  7970  ressuppssdif  8001  mpoxneldm  8028  dfsup2  9203  nelaneq  9358  suc11reg  9377  rankxplim3  9639  kmlem3  9908  cdainflem  9943  isfin5-2  10147  mulge0b  11845  nn0n0n1ge2b  12301  rpneg  12762  mul2lt0bi  12836  xrrebnd  12902  xnn0xaddcl  12969  xmullem2  12999  difreicc  13216  fz0  13271  nelfzo  13392  injresinj  13508  hashunx  14101  swrdnd  14367  swrdnnn0nd  14369  swrdnd0  14370  repswswrd  14497  dfgcd2  16254  ncoprmlnprm  16432  firest  17143  xpcbas  17895  smndex2dnrinv  18554  symgfix2  19024  gsumdixp  19848  0ringnnzr  20540  mplsubrglem  21210  symgmatr01lem  21802  ppttop  22157  fin1aufil  23083  zclmncvs  24312  mbfmax  24813  mdegleb  25229  coemulhi  25415  numedglnl  27514  usgredg2v  27594  clwwlkn  28390  clwwlkneq0  28393  clwwlknon1nloop  28463  trlsegvdeg  28591  1to2vfriswmgr  28643  numclwwlk3lem2  28748  atcvati  30748  difrab2  30845  ofpreima2  31003  hashxpe  31127  ordtconnlem1  31874  aean  32212  sitgaddlemb  32315  ballotlemodife  32464  bnj1174  32983  erdszelem10  33162  satfv1  33325  fmla0disjsuc  33360  fmlasucdisj  33361  dfon2lem4  33762  naddcllem  33831  noetasuplem4  33939  noetainflem4  33943  sltlpss  34087  nrmo  34599  poimirlem30  35807  poimirlem31  35808  itg2addnclem  35828  itg2addnclem2  35829  itg2addnclem3  35830  iblabsnclem  35840  ftc1anclem3  35852  areacirclem4  35868  lsatcvat  37064  lkreqN  37184  cvrat  37436  4atlem3  37610  paddasslem17  37850  llnexchb2  37883  dalawlem14  37898  cdleme0nex  38304  lclkrlem2o  39535  lcfrlem19  39575  dvrelog2b  40074  aks4d1p7  40091  sticksstones1  40102  ifpnot23  41085  ifpim123g  41107  sqrtcvallem1  41239  ntrneineine1lem  41694  mnringmulrcld  41846  stoweidlem14  43555  stoweidlem26  43567  dfatprc  44622  afvco2  44668  ndmafv2nrn  44714  nfunsnafv2  44717  afv2ndeffv0  44752  nltle2tri  44805  ichnreuop  44924  spr0nelg  44928  evennodd  45095  oddneven  45096  lindslinindsimp1  45798  lindslinindsimp2  45804  line2ylem  46097  line2xlem  46099