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  1491  cadnot  1611  19.33b  1882  neorian  3034  2nreu  4449  tpprceq3  4808  tppreqb  4809  prneimg  4858  prneimg2  4859  prnebg  4860  preq12nebg  4867  opthprneg  4869  opthneg  5491  fr2nr  5665  iresn0n0  6073  xpeq0  6181  difxp  6185  ordtri3or  6417  imadif  6651  ftpg  7175  nf1const  7323  nf1oconst  7324  0mpo0  7515  2mpo0  7681  bropopvvv  8113  bropfvvvv  8115  frxp  8149  soxp  8152  ressuppssdif  8208  mpoxneldm  8235  naddcllem  8712  dfsup2  9481  nelaneq  9636  suc11reg  9656  rankxplim3  9918  kmlem3  10190  cdainflem  10225  isfin5-2  10428  mulge0b  12135  nn0n0n1ge2b  12592  rpneg  13064  mul2lt0bi  13138  xrrebnd  13206  xnn0xaddcl  13273  xmullem2  13303  difreicc  13520  fz0  13575  nelfzo  13700  injresinj  13823  hashunx  14421  swrdnd  14688  swrdnnn0nd  14690  swrdnd0  14691  repswswrd  14818  dfgcd2  16579  ncoprmlnprm  16761  firest  17478  xpcbas  18233  smndex2dnrinv  18940  symgfix2  19448  gsumdixp  20332  0ringnnzr  20541  mplsubrglem  22041  symgmatr01lem  22674  ppttop  23029  fin1aufil  23955  zclmncvs  25195  mbfmax  25697  mdegleb  26117  coemulhi  26307  noetasuplem4  27795  noetainflem4  27799  sltlpss  27959  numedglnl  29175  usgredg2v  29258  clwwlkn  30054  clwwlkneq0  30057  clwwlknon1nloop  30127  trlsegvdeg  30255  1to2vfriswmgr  30307  numclwwlk3lem2  30412  atcvati  32414  difrab2  32525  ofpreima2  32682  hashxpe  32816  ordtconnlem1  33884  aean  34224  sitgaddlemb  34329  ballotlemodife  34478  bnj1174  34995  erdszelem10  35184  satfv1  35347  fmla0disjsuc  35382  fmlasucdisj  35383  dfon2lem4  35767  nrmo  36392  poimirlem30  37636  poimirlem31  37637  itg2addnclem  37657  itg2addnclem2  37658  itg2addnclem3  37659  iblabsnclem  37669  ftc1anclem3  37681  areacirclem4  37697  lsatcvat  39031  lkreqN  39151  cvrat  39404  4atlem3  39578  paddasslem17  39818  llnexchb2  39851  dalawlem14  39866  cdleme0nex  40272  lclkrlem2o  41503  lcfrlem19  41543  dvrelog2b  42047  aks4d1p7  42064  aks6d1c2p2  42100  aks6d1c5  42120  sticksstones1  42127  aks6d1c6lem3  42153  ifpnot23  43467  ifpim123g  43489  sqrtcvallem1  43620  ntrneineine1lem  44073  mnringmulrcld  44223  stoweidlem14  45969  stoweidlem26  45981  dfatprc  47079  afvco2  47125  ndmafv2nrn  47171  nfunsnafv2  47174  afv2ndeffv0  47209  nltle2tri  47262  ichnreuop  47396  spr0nelg  47400  evennodd  47567  oddneven  47568  usgrexmpl2trifr  47931  lindslinindsimp1  48302  lindslinindsimp2  48308  line2ylem  48600  line2xlem  48602