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  3020  2nreu  4407  tpprceq3  4768  tppreqb  4769  prneimg  4818  prneimg2  4819  prnebg  4820  preq12nebg  4827  opthprneg  4829  opthneg  5441  fr2nr  5615  iresn0n0  6025  xpeq0  6133  difxp  6137  ordtri3or  6364  imadif  6600  ftpg  7128  nf1const  7279  nf1oconst  7280  0mpo0  7472  2mpo0  7638  bropopvvv  8069  bropfvvvv  8071  frxp  8105  soxp  8108  ressuppssdif  8164  mpoxneldm  8191  naddcllem  8640  dfsup2  9395  nelaneq  9552  suc11reg  9572  rankxplim3  9834  kmlem3  10106  cdainflem  10141  isfin5-2  10344  mulge0b  12053  nn0n0n1ge2b  12511  rpneg  12985  mul2lt0bi  13059  xrrebnd  13128  xnn0xaddcl  13195  xmullem2  13225  difreicc  13445  fz0  13500  nelfzo  13625  injresinj  13749  hashunx  14351  swrdnd  14619  swrdnnn0nd  14621  swrdnd0  14622  repswswrd  14749  dfgcd2  16516  ncoprmlnprm  16698  firest  17395  xpcbas  18139  smndex2dnrinv  18842  symgfix2  19346  gsumdixp  20228  0ringnnzr  20434  mplsubrglem  21913  symgmatr01lem  22540  ppttop  22894  fin1aufil  23819  zclmncvs  25048  mbfmax  25550  mdegleb  25969  coemulhi  26159  noetasuplem4  27648  noetainflem4  27652  sltlpss  27819  numedglnl  29071  usgredg2v  29154  clwwlkn  29955  clwwlkneq0  29958  clwwlknon1nloop  30028  trlsegvdeg  30156  1to2vfriswmgr  30208  numclwwlk3lem2  30313  atcvati  32315  difrab2  32427  ofpreima2  32590  hashxpe  32732  fldextrspunlsplem  33668  ordtconnlem1  33914  aean  34234  sitgaddlemb  34339  ballotlemodife  34489  bnj1174  34993  erdszelem10  35187  satfv1  35350  fmla0disjsuc  35385  fmlasucdisj  35386  dfon2lem4  35774  nrmo  36398  poimirlem30  37644  poimirlem31  37645  itg2addnclem  37665  itg2addnclem2  37666  itg2addnclem3  37667  iblabsnclem  37677  ftc1anclem3  37689  areacirclem4  37705  lsatcvat  39043  lkreqN  39163  cvrat  39416  4atlem3  39590  paddasslem17  39830  llnexchb2  39863  dalawlem14  39878  cdleme0nex  40284  lclkrlem2o  41515  lcfrlem19  41555  dvrelog2b  42054  aks4d1p7  42071  aks6d1c2p2  42107  aks6d1c5  42127  sticksstones1  42134  aks6d1c6lem3  42160  ifpnot23  43467  ifpim123g  43489  sqrtcvallem1  43620  ntrneineine1lem  44073  mnringmulrcld  44217  stoweidlem14  46012  stoweidlem26  46024  dfatprc  47131  afvco2  47177  ndmafv2nrn  47223  nfunsnafv2  47226  afv2ndeffv0  47261  nltle2tri  47314  ichnreuop  47473  spr0nelg  47477  evennodd  47644  oddneven  47645  usgrexmpl2trifr  48028  pg4cyclnex  48117  lindslinindsimp1  48446  lindslinindsimp2  48452  line2ylem  48740  line2xlem  48742