Theorem ianor 983

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 399	. 2 ⊢ ((𝜑 → ¬ 𝜓) ↔ ¬ (𝜑 ∧ 𝜓))
2		pm4.62 856	. 2 ⊢ ((𝜑 → ¬ 𝜓) ↔ (¬ 𝜑 ∨ ¬ 𝜓))
3	1, 2	bitr3i 277	1 ⊢ (¬ (𝜑 ∧ 𝜓) ↔ (¬ 𝜑 ∨ ¬ 𝜓))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395   ∨ wo 847

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 207  df-an 396  df-or 848

This theorem is referenced by:  anor  984  3ianor  1106  nanor  1495  cadnot  1615  19.33b  1885  neorian  3027  2nreu  4419  tpprceq3  4780  tppreqb  4781  prneimg  4830  prneimg2  4831  prnebg  4832  preq12nebg  4839  opthprneg  4841  opthneg  5456  fr2nr  5631  iresn0n0  6041  xpeq0  6149  difxp  6153  ordtri3or  6384  imadif  6620  ftpg  7146  nf1const  7297  nf1oconst  7298  0mpo0  7490  2mpo0  7656  bropopvvv  8089  bropfvvvv  8091  frxp  8125  soxp  8128  ressuppssdif  8184  mpoxneldm  8211  naddcllem  8688  dfsup2  9456  nelaneq  9613  suc11reg  9633  rankxplim3  9895  kmlem3  10167  cdainflem  10202  isfin5-2  10405  mulge0b  12112  nn0n0n1ge2b  12570  rpneg  13041  mul2lt0bi  13115  xrrebnd  13184  xnn0xaddcl  13251  xmullem2  13281  difreicc  13501  fz0  13556  nelfzo  13681  injresinj  13804  hashunx  14404  swrdnd  14672  swrdnnn0nd  14674  swrdnd0  14675  repswswrd  14802  dfgcd2  16565  ncoprmlnprm  16747  firest  17446  xpcbas  18190  smndex2dnrinv  18893  symgfix2  19397  gsumdixp  20279  0ringnnzr  20485  mplsubrglem  21964  symgmatr01lem  22591  ppttop  22945  fin1aufil  23870  zclmncvs  25100  mbfmax  25602  mdegleb  26021  coemulhi  26211  noetasuplem4  27700  noetainflem4  27704  sltlpss  27871  numedglnl  29123  usgredg2v  29206  clwwlkn  30007  clwwlkneq0  30010  clwwlknon1nloop  30080  trlsegvdeg  30208  1to2vfriswmgr  30260  numclwwlk3lem2  30365  atcvati  32367  difrab2  32479  ofpreima2  32644  hashxpe  32786  fldextrspunlsplem  33714  ordtconnlem1  33955  aean  34275  sitgaddlemb  34380  ballotlemodife  34530  bnj1174  35034  erdszelem10  35222  satfv1  35385  fmla0disjsuc  35420  fmlasucdisj  35421  dfon2lem4  35804  nrmo  36428  poimirlem30  37674  poimirlem31  37675  itg2addnclem  37695  itg2addnclem2  37696  itg2addnclem3  37697  iblabsnclem  37707  ftc1anclem3  37719  areacirclem4  37735  lsatcvat  39068  lkreqN  39188  cvrat  39441  4atlem3  39615  paddasslem17  39855  llnexchb2  39888  dalawlem14  39903  cdleme0nex  40309  lclkrlem2o  41540  lcfrlem19  41580  dvrelog2b  42079  aks4d1p7  42096  aks6d1c2p2  42132  aks6d1c5  42152  sticksstones1  42159  aks6d1c6lem3  42185  ifpnot23  43502  ifpim123g  43524  sqrtcvallem1  43655  ntrneineine1lem  44108  mnringmulrcld  44252  stoweidlem14  46043  stoweidlem26  46055  dfatprc  47159  afvco2  47205  ndmafv2nrn  47251  nfunsnafv2  47254  afv2ndeffv0  47289  nltle2tri  47342  ichnreuop  47486  spr0nelg  47490  evennodd  47657  oddneven  47658  usgrexmpl2trifr  48041  lindslinindsimp1  48433  lindslinindsimp2  48439  line2ylem  48731  line2xlem  48733