Theorem ianor 997

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

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 401   ∨ wo 861

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862

This theorem is used by:  anor  998  3ianor  1124  nanor  1525  cadnot  1648  19.33b  1918  neorian  3051  2nreu  4402  tpprceq3  4767  tppreqb  4768  prneimg  4814  prneimg2  4815  prnebg  4816  preq12nebg  4823  opthprneg  4825  opthneg  5450  fr2nr  5628  iresn0n0  6046  xpeq0  6151  difxp  6155  ordtri3or  6394  imadif  6622  ftpg  7158  nf1const  7310  nf1oconst  7311  0mpo0  7501  2mpo0  7668  bropopvvv  8099  bropfvvvv  8101  frxp  8136  soxp  8139  ressuppssdif  8195  mpoxneldm  8222  naddcllem  8678  dfsup2  9429  nelaneqOLDOLD  9591  suc11reg  9613  rankxplim3  9891  kmlem3  10224  cdainflem  10259  isfin5-2  10462  mulge0b  12180  nn0n0n1ge2b  12668  rpneg  13147  mul2lt0bi  13221  xrrebnd  13291  xnn0xaddcl  13358  xmullem2  13388  difreicc  13608  fz0  13665  nelfzo  13792  injresinj  13919  hashunx  14523  swrdnd  14797  swrdnnn0nd  14799  swrdnd0  14800  repswswrd  14928  dfgcd2  16712  ncoprmlnprm  16897  firest  17596  xpcbas  18345  smndex2dnrinv  19107  symgfix2  19623  gsumdixp  20541  0ringnnzr  20769  isfieldidl  21533  mplsubrglem  22304  symgmatr01lem  22961  ppttop  23318  fin1aufil  24244  zclmncvs  25462  mbfmax  25963  mdegleb  26375  coemulhi  26566  noetasuplem4  28086  noetainflem4  28090  ltslpss  28287  lnssplng  29263  numedglnl  29715  usgredg2v  29801  clwwlkn  30610  clwwlkneq0  30613  clwwlknon1nloop  30683  trlsegvdeg  30821  1to2vfriswmgr  30873  numclwwlk3lem2  30978  atcvati  32981  difrab2  33087  ofpreima2  33253  hashxpe  33392  drnglring  34017  fldextrspunlsplem  34298  ordtconnlem1  34549  aean  34870  sitgaddlemb  34973  ballotlemodife  35123  bnj1174  35626  erdszelem10  35944  satfv1  36107  fmla0disjsuc  36142  fmlasucdisj  36143  dfon2lem4  36528  ltnadd  36947  naddle  36948  nrmo  37178  poimirlem30  38548  poimirlem31  38549  itg2addnclem  38569  itg2addnclem2  38570  itg2addnclem3  38571  iblabsnclem  38581  ftc1anclem3  38593  areacirclem4  38609  lsatcvat  40087  lkreqN  40207  cvrat  40459  4atlem3  40633  paddasslem17  40873  llnexchb2  40906  dalawlem14  40921  cdleme0nex  41327  lclkrlem2o  42558  lcfrlem19  42598  dvrelog2b  43096  aks4d1p7  43113  aks6d1c2p2  43149  aks6d1c5  43169  sticksstones1  43176  aks6d1c6lem3  43202  ifpnot23  44463  ifpim123g  44485  sqrtcvallem1  44616  ntrneineine1lem  45069  mnringmulrcld  45211  stoweidlem14  46993  stoweidlem26  47005  dfatprc  48169  afvco2  48215  ndmafv2nrn  48261  nfunsnafv2  48264  afv2ndeffv0  48299  nltle2tri  48352  ichnreuop  48523  spr0nelg  48527  evennodd  48710  oddneven  48711  usgrexmpl2trifr  49104  pg4cyclnex  49194  lindslinindsimp1  49538  lindslinindsimp2  49544  line2ylem  49832  line2xlem  49834