Theorem ianor 981

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 205   ∧ wa 397   ∨ 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 206  df-an 398  df-or 847

This theorem is referenced by:  anor  982  3ianor  1108  nanor  1494  cadnot  1617  19.33b  1889  neorian  3038  indifdirOLD  4284  2nreu  4440  tpprceq3  4806  tppreqb  4807  prneimg  4854  prnebg  4855  preq12nebg  4862  opthprneg  4864  opthneg  5480  fr2nr  5653  iresn0n0  6051  xpeq0  6156  difxp  6160  ordtri3or  6393  imadif  6629  ftpg  7149  nf1const  7297  nf1oconst  7298  0mpo0  7487  2mpo0  7650  bropopvvv  8071  bropfvvvv  8073  frxp  8107  soxp  8110  ressuppssdif  8165  mpoxneldm  8192  naddcllem  8671  dfsup2  9435  nelaneq  9590  suc11reg  9610  rankxplim3  9872  kmlem3  10143  cdainflem  10178  isfin5-2  10382  mulge0b  12080  nn0n0n1ge2b  12536  rpneg  13002  mul2lt0bi  13076  xrrebnd  13143  xnn0xaddcl  13210  xmullem2  13240  difreicc  13457  fz0  13512  nelfzo  13633  injresinj  13749  hashunx  14342  swrdnd  14600  swrdnnn0nd  14602  swrdnd0  14603  repswswrd  14730  dfgcd2  16484  ncoprmlnprm  16660  firest  17374  xpcbas  18126  smndex2dnrinv  18792  symgfix2  19277  gsumdixp  20121  0ringnnzr  20291  mplsubrglem  21545  symgmatr01lem  22137  ppttop  22492  fin1aufil  23418  zclmncvs  24647  mbfmax  25148  mdegleb  25564  coemulhi  25750  noetasuplem4  27219  noetainflem4  27223  sltlpss  27381  numedglnl  28384  usgredg2v  28464  clwwlkn  29259  clwwlkneq0  29262  clwwlknon1nloop  29332  trlsegvdeg  29460  1to2vfriswmgr  29512  numclwwlk3lem2  29617  atcvati  31617  difrab2  31716  ofpreima2  31869  hashxpe  31997  ordtconnlem1  32842  aean  33180  sitgaddlemb  33285  ballotlemodife  33434  bnj1174  33952  erdszelem10  34129  satfv1  34292  fmla0disjsuc  34327  fmlasucdisj  34328  dfon2lem4  34696  nrmo  35233  poimirlem30  36456  poimirlem31  36457  itg2addnclem  36477  itg2addnclem2  36478  itg2addnclem3  36479  iblabsnclem  36489  ftc1anclem3  36501  areacirclem4  36517  lsatcvat  37858  lkreqN  37978  cvrat  38231  4atlem3  38405  paddasslem17  38645  llnexchb2  38678  dalawlem14  38693  cdleme0nex  39099  lclkrlem2o  40330  lcfrlem19  40370  dvrelog2b  40869  aks4d1p7  40886  aks6d1c2p2  40895  sticksstones1  40900  ifpnot23  42162  ifpim123g  42184  sqrtcvallem1  42315  ntrneineine1lem  42768  mnringmulrcld  42920  stoweidlem14  44665  stoweidlem26  44677  dfatprc  45773  afvco2  45819  ndmafv2nrn  45865  nfunsnafv2  45868  afv2ndeffv0  45903  nltle2tri  45956  ichnreuop  46075  spr0nelg  46079  evennodd  46246  oddneven  46247  lindslinindsimp1  47040  lindslinindsimp2  47046  line2ylem  47339  line2xlem  47341