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  1496  cadnot  1616  19.33b  1886  neorian  3024  2nreu  4393  tpprceq3  4757  tppreqb  4758  prneimg  4807  prneimg2  4808  prnebg  4809  preq12nebg  4816  opthprneg  4818  opthneg  5426  fr2nr  5598  iresn0n0  6010  xpeq0  6115  difxp  6119  ordtri3or  6346  imadif  6573  ftpg  7098  nf1const  7247  nf1oconst  7248  0mpo0  7438  2mpo0  7604  bropopvvv  8029  bropfvvvv  8031  frxp  8065  soxp  8068  ressuppssdif  8124  mpoxneldm  8151  naddcllem  8600  dfsup2  9339  nelaneqOLD  9499  suc11reg  9520  rankxplim3  9785  kmlem3  10055  cdainflem  10090  isfin5-2  10293  mulge0b  12003  nn0n0n1ge2b  12461  rpneg  12930  mul2lt0bi  13004  xrrebnd  13074  xnn0xaddcl  13141  xmullem2  13171  difreicc  13391  fz0  13446  nelfzo  13571  injresinj  13698  hashunx  14300  swrdnd  14569  swrdnnn0nd  14571  swrdnd0  14572  repswswrd  14698  dfgcd2  16464  ncoprmlnprm  16646  firest  17343  xpcbas  18092  smndex2dnrinv  18831  symgfix2  19336  gsumdixp  20245  0ringnnzr  20449  mplsubrglem  21950  symgmatr01lem  22588  ppttop  22942  fin1aufil  23867  zclmncvs  25095  mbfmax  25597  mdegleb  26016  coemulhi  26206  noetasuplem4  27695  noetainflem4  27699  sltlpss  27873  numedglnl  29143  usgredg2v  29226  clwwlkn  30027  clwwlkneq0  30030  clwwlknon1nloop  30100  trlsegvdeg  30228  1to2vfriswmgr  30280  numclwwlk3lem2  30385  atcvati  32387  difrab2  32498  ofpreima2  32670  hashxpe  32815  fldextrspunlsplem  33758  ordtconnlem1  34009  aean  34329  sitgaddlemb  34433  ballotlemodife  34583  bnj1174  35087  erdszelem10  35316  satfv1  35479  fmla0disjsuc  35514  fmlasucdisj  35515  dfon2lem4  35900  nrmo  36526  poimirlem30  37763  poimirlem31  37764  itg2addnclem  37784  itg2addnclem2  37785  itg2addnclem3  37786  iblabsnclem  37796  ftc1anclem3  37808  areacirclem4  37824  lsatcvat  39222  lkreqN  39342  cvrat  39594  4atlem3  39768  paddasslem17  40008  llnexchb2  40041  dalawlem14  40056  cdleme0nex  40462  lclkrlem2o  41693  lcfrlem19  41733  dvrelog2b  42232  aks4d1p7  42249  aks6d1c2p2  42285  aks6d1c5  42305  sticksstones1  42312  aks6d1c6lem3  42338  ifpnot23  43635  ifpim123g  43657  sqrtcvallem1  43788  ntrneineine1lem  44241  mnringmulrcld  44385  stoweidlem14  46174  stoweidlem26  46186  dfatprc  47292  afvco2  47338  ndmafv2nrn  47384  nfunsnafv2  47387  afv2ndeffv0  47422  nltle2tri  47475  ichnreuop  47634  spr0nelg  47638  evennodd  47805  oddneven  47806  usgrexmpl2trifr  48199  pg4cyclnex  48289  lindslinindsimp1  48619  lindslinindsimp2  48625  line2ylem  48913  line2xlem  48915