Theorem ianor 989

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 207   ∧ wa 396   ∨ wo 853

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 208  df-an 397  df-or 854

This theorem is referenced by:  anor  990  3ianor  1112  nanor  1502  cadnot  1622  19.33b  1892  neorian  3029  2nreu  4372  tpprceq3  4737  tppreqb  4738  prneimg  4785  prneimg2  4786  prnebg  4787  preq12nebg  4794  opthprneg  4796  opthneg  5421  fr2nr  5595  iresn0n0  6006  xpeq0  6111  difxp  6115  ordtri3or  6342  imadif  6569  ftpg  7099  nf1const  7248  nf1oconst  7249  0mpo0  7439  2mpo0  7605  bropopvvv  8029  bropfvvvv  8031  frxp  8066  soxp  8069  ressuppssdif  8125  mpoxneldm  8152  naddcllem  8602  dfsup2  9347  nelaneqOLDOLD  9509  suc11reg  9531  rankxplim3  9796  kmlem3  10066  cdainflem  10101  isfin5-2  10304  mulge0b  12017  nn0n0n1ge2b  12497  rpneg  12967  mul2lt0bi  13041  xrrebnd  13111  xnn0xaddcl  13178  xmullem2  13208  difreicc  13428  fz0  13484  nelfzo  13610  injresinj  13737  hashunx  14339  swrdnd  14608  swrdnnn0nd  14610  swrdnd0  14611  repswswrd  14737  dfgcd2  16506  ncoprmlnprm  16689  firest  17386  xpcbas  18135  smndex2dnrinv  18877  symgfix2  19382  gsumdixp  20289  0ringnnzr  20497  mplsubrglem  21978  symgmatr01lem  22636  ppttop  22990  fin1aufil  23915  zclmncvs  25133  mbfmax  25634  mdegleb  26047  coemulhi  26237  noetasuplem4  27718  noetainflem4  27722  ltslpss  27918  numedglnl  29231  usgredg2v  29314  clwwlkn  30114  clwwlkneq0  30117  clwwlknon1nloop  30187  trlsegvdeg  30315  1to2vfriswmgr  30367  numclwwlk3lem2  30472  atcvati  32475  difrab2  32585  ofpreima2  32758  hashxpe  32899  fldextrspunlsplem  33857  ordtconnlem1  34108  aean  34428  sitgaddlemb  34532  ballotlemodife  34682  bnj1174  35185  erdszelem10  35428  satfv1  35591  fmla0disjsuc  35626  fmlasucdisj  35627  dfon2lem4  36012  nrmo  36638  poimirlem30  38017  poimirlem31  38018  itg2addnclem  38038  itg2addnclem2  38039  itg2addnclem3  38040  iblabsnclem  38050  ftc1anclem3  38062  areacirclem4  38078  lsatcvat  39542  lkreqN  39662  cvrat  39914  4atlem3  40088  paddasslem17  40328  llnexchb2  40361  dalawlem14  40376  cdleme0nex  40782  lclkrlem2o  42013  lcfrlem19  42053  dvrelog2b  42551  aks4d1p7  42568  aks6d1c2p2  42604  aks6d1c5  42624  sticksstones1  42631  aks6d1c6lem3  42657  ifpnot23  43922  ifpim123g  43944  sqrtcvallem1  44075  ntrneineine1lem  44528  mnringmulrcld  44672  stoweidlem14  46457  stoweidlem26  46469  dfatprc  47593  afvco2  47639  ndmafv2nrn  47685  nfunsnafv2  47688  afv2ndeffv0  47723  nltle2tri  47776  ichnreuop  47947  spr0nelg  47951  evennodd  48134  oddneven  48135  usgrexmpl2trifr  48528  pg4cyclnex  48618  lindslinindsimp1  48948  lindslinindsimp2  48954  line2ylem  49242  line2xlem  49244