Theorem ianor 980

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 854	. 2 ⊢ ((𝜑 → ¬ 𝜓) ↔ (¬ 𝜑 ∨ ¬ 𝜓))
3	1, 2	bitr3i 276	1 ⊢ (¬ (𝜑 ∧ 𝜓) ↔ (¬ 𝜑 ∨ ¬ 𝜓))

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

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 846

This theorem is referenced by:  anor  981  3ianor  1107  nanor  1493  cadnot  1616  19.33b  1888  neorian  3037  indifdirOLD  4284  2nreu  4440  tpprceq3  4806  tppreqb  4807  prneimg  4854  prnebg  4855  preq12nebg  4862  opthprneg  4864  opthneg  5480  fr2nr  5653  iresn0n0  6051  xpeq0  6156  difxp  6160  ordtri3or  6393  imadif  6629  ftpg  7150  nf1const  7298  nf1oconst  7299  0mpo0  7488  2mpo0  7651  bropopvvv  8072  bropfvvvv  8074  frxp  8108  soxp  8111  ressuppssdif  8166  mpoxneldm  8193  naddcllem  8671  dfsup2  9435  nelaneq  9590  suc11reg  9610  rankxplim3  9872  kmlem3  10143  cdainflem  10178  isfin5-2  10382  mulge0b  12080  nn0n0n1ge2b  12536  rpneg  13002  mul2lt0bi  13076  xrrebnd  13143  xnn0xaddcl  13210  xmullem2  13240  difreicc  13457  fz0  13512  nelfzo  13633  injresinj  13749  hashunx  14342  swrdnd  14600  swrdnnn0nd  14602  swrdnd0  14603  repswswrd  14730  dfgcd2  16484  ncoprmlnprm  16660  firest  17374  xpcbas  18126  smndex2dnrinv  18792  symgfix2  19278  gsumdixp  20124  0ringnnzr  20294  mplsubrglem  21554  symgmatr01lem  22146  ppttop  22501  fin1aufil  23427  zclmncvs  24656  mbfmax  25157  mdegleb  25573  coemulhi  25759  noetasuplem4  27228  noetainflem4  27232  sltlpss  27390  numedglnl  28393  usgredg2v  28473  clwwlkn  29268  clwwlkneq0  29271  clwwlknon1nloop  29341  trlsegvdeg  29469  1to2vfriswmgr  29521  numclwwlk3lem2  29626  atcvati  31626  difrab2  31725  ofpreima2  31878  hashxpe  32006  ordtconnlem1  32892  aean  33230  sitgaddlemb  33335  ballotlemodife  33484  bnj1174  34002  erdszelem10  34179  satfv1  34342  fmla0disjsuc  34377  fmlasucdisj  34378  dfon2lem4  34746  nrmo  35283  poimirlem30  36506  poimirlem31  36507  itg2addnclem  36527  itg2addnclem2  36528  itg2addnclem3  36529  iblabsnclem  36539  ftc1anclem3  36551  areacirclem4  36567  lsatcvat  37908  lkreqN  38028  cvrat  38281  4atlem3  38455  paddasslem17  38695  llnexchb2  38728  dalawlem14  38743  cdleme0nex  39149  lclkrlem2o  40380  lcfrlem19  40420  dvrelog2b  40919  aks4d1p7  40936  aks6d1c2p2  40945  sticksstones1  40950  ifpnot23  42214  ifpim123g  42236  sqrtcvallem1  42367  ntrneineine1lem  42820  mnringmulrcld  42972  stoweidlem14  44716  stoweidlem26  44728  dfatprc  45824  afvco2  45870  ndmafv2nrn  45916  nfunsnafv2  45919  afv2ndeffv0  45954  nltle2tri  46007  ichnreuop  46126  spr0nelg  46130  evennodd  46297  oddneven  46298  lindslinindsimp1  47091  lindslinindsimp2  47097  line2ylem  47390  line2xlem  47392