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  3027  2nreu  4396  tpprceq3  4760  tppreqb  4761  prneimg  4810  prneimg2  4811  prnebg  4812  preq12nebg  4819  opthprneg  4821  opthneg  5429  fr2nr  5601  iresn0n0  6013  xpeq0  6118  difxp  6122  ordtri3or  6349  imadif  6576  ftpg  7101  nf1const  7250  nf1oconst  7251  0mpo0  7441  2mpo0  7607  bropopvvv  8032  bropfvvvv  8034  frxp  8068  soxp  8071  ressuppssdif  8127  mpoxneldm  8154  naddcllem  8604  dfsup2  9347  nelaneqOLD  9507  suc11reg  9528  rankxplim3  9793  kmlem3  10063  cdainflem  10098  isfin5-2  10301  mulge0b  12012  nn0n0n1ge2b  12470  rpneg  12939  mul2lt0bi  13013  xrrebnd  13083  xnn0xaddcl  13150  xmullem2  13180  difreicc  13400  fz0  13455  nelfzo  13580  injresinj  13707  hashunx  14309  swrdnd  14578  swrdnnn0nd  14580  swrdnd0  14581  repswswrd  14707  dfgcd2  16473  ncoprmlnprm  16655  firest  17352  xpcbas  18101  smndex2dnrinv  18840  symgfix2  19345  gsumdixp  20254  0ringnnzr  20458  mplsubrglem  21959  symgmatr01lem  22597  ppttop  22951  fin1aufil  23876  zclmncvs  25104  mbfmax  25606  mdegleb  26025  coemulhi  26215  noetasuplem4  27704  noetainflem4  27708  ltslpss  27904  numedglnl  29217  usgredg2v  29300  clwwlkn  30101  clwwlkneq0  30104  clwwlknon1nloop  30174  trlsegvdeg  30302  1to2vfriswmgr  30354  numclwwlk3lem2  30459  atcvati  32461  difrab2  32572  ofpreima2  32744  hashxpe  32887  fldextrspunlsplem  33830  ordtconnlem1  34081  aean  34401  sitgaddlemb  34505  ballotlemodife  34655  bnj1174  35159  erdszelem10  35394  satfv1  35557  fmla0disjsuc  35592  fmlasucdisj  35593  dfon2lem4  35978  nrmo  36604  poimirlem30  37851  poimirlem31  37852  itg2addnclem  37872  itg2addnclem2  37873  itg2addnclem3  37874  iblabsnclem  37884  ftc1anclem3  37896  areacirclem4  37912  lsatcvat  39310  lkreqN  39430  cvrat  39682  4atlem3  39856  paddasslem17  40096  llnexchb2  40129  dalawlem14  40144  cdleme0nex  40550  lclkrlem2o  41781  lcfrlem19  41821  dvrelog2b  42320  aks4d1p7  42337  aks6d1c2p2  42373  aks6d1c5  42393  sticksstones1  42400  aks6d1c6lem3  42426  ifpnot23  43719  ifpim123g  43741  sqrtcvallem1  43872  ntrneineine1lem  44325  mnringmulrcld  44469  stoweidlem14  46258  stoweidlem26  46270  dfatprc  47376  afvco2  47422  ndmafv2nrn  47468  nfunsnafv2  47471  afv2ndeffv0  47506  nltle2tri  47559  ichnreuop  47718  spr0nelg  47722  evennodd  47889  oddneven  47890  usgrexmpl2trifr  48283  pg4cyclnex  48373  lindslinindsimp1  48703  lindslinindsimp2  48709  line2ylem  48997  line2xlem  48999