Theorem ianor 982

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

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

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 847

This theorem is referenced by:  anor  983  3ianor  1107  nanor  1492  cadnot  1612  19.33b  1884  neorian  3043  2nreu  4467  tpprceq3  4829  tppreqb  4830  prneimg  4879  prnebg  4880  preq12nebg  4887  opthprneg  4889  opthneg  5501  fr2nr  5677  iresn0n0  6083  xpeq0  6191  difxp  6195  ordtri3or  6427  imadif  6662  ftpg  7190  nf1const  7340  nf1oconst  7341  0mpo0  7533  2mpo0  7699  bropopvvv  8131  bropfvvvv  8133  frxp  8167  soxp  8170  ressuppssdif  8226  mpoxneldm  8253  naddcllem  8732  dfsup2  9513  nelaneq  9668  suc11reg  9688  rankxplim3  9950  kmlem3  10222  cdainflem  10257  isfin5-2  10460  mulge0b  12165  nn0n0n1ge2b  12621  rpneg  13089  mul2lt0bi  13163  xrrebnd  13230  xnn0xaddcl  13297  xmullem2  13327  difreicc  13544  fz0  13599  nelfzo  13721  injresinj  13838  hashunx  14435  swrdnd  14702  swrdnnn0nd  14704  swrdnd0  14705  repswswrd  14832  dfgcd2  16593  ncoprmlnprm  16775  firest  17492  xpcbas  18247  smndex2dnrinv  18950  symgfix2  19458  gsumdixp  20342  0ringnnzr  20551  mplsubrglem  22047  symgmatr01lem  22680  ppttop  23035  fin1aufil  23961  zclmncvs  25201  mbfmax  25703  mdegleb  26123  coemulhi  26313  noetasuplem4  27799  noetainflem4  27803  sltlpss  27963  numedglnl  29179  usgredg2v  29262  clwwlkn  30058  clwwlkneq0  30061  clwwlknon1nloop  30131  trlsegvdeg  30259  1to2vfriswmgr  30311  numclwwlk3lem2  30416  atcvati  32418  difrab2  32526  ofpreima2  32684  hashxpe  32814  ordtconnlem1  33870  aean  34208  sitgaddlemb  34313  ballotlemodife  34462  bnj1174  34979  erdszelem10  35168  satfv1  35331  fmla0disjsuc  35366  fmlasucdisj  35367  dfon2lem4  35750  nrmo  36376  poimirlem30  37610  poimirlem31  37611  itg2addnclem  37631  itg2addnclem2  37632  itg2addnclem3  37633  iblabsnclem  37643  ftc1anclem3  37655  areacirclem4  37671  lsatcvat  39006  lkreqN  39126  cvrat  39379  4atlem3  39553  paddasslem17  39793  llnexchb2  39826  dalawlem14  39841  cdleme0nex  40247  lclkrlem2o  41478  lcfrlem19  41518  dvrelog2b  42023  aks4d1p7  42040  aks6d1c2p2  42076  aks6d1c5  42096  sticksstones1  42103  aks6d1c6lem3  42129  ifpnot23  43440  ifpim123g  43462  sqrtcvallem1  43593  ntrneineine1lem  44046  mnringmulrcld  44197  stoweidlem14  45935  stoweidlem26  45947  dfatprc  47045  afvco2  47091  ndmafv2nrn  47137  nfunsnafv2  47140  afv2ndeffv0  47175  nltle2tri  47228  ichnreuop  47346  spr0nelg  47350  evennodd  47517  oddneven  47518  usgrexmpl2trifr  47852  lindslinindsimp1  48186  lindslinindsimp2  48192  line2ylem  48485  line2xlem  48487