Theorem ianor 992

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 208   ∧ wa 398   ∨ wo 856

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 209  df-an 399  df-or 857

This theorem is referenced by:  anor  993  3ianor  1115  nanor  1505  cadnot  1625  19.33b  1895  neorian  3042  2nreu  4388  tpprceq3  4754  tppreqb  4755  prneimg  4802  prneimg2  4803  prnebg  4804  preq12nebg  4811  opthprneg  4813  opthneg  5439  fr2nr  5613  iresn0n0  6029  xpeq0  6131  difxp  6135  ordtri3or  6363  imadif  6590  ftpg  7124  nf1const  7273  nf1oconst  7274  0mpo0  7464  2mpo0  7630  bropopvvv  8053  bropfvvvv  8055  frxp  8090  soxp  8093  ressuppssdif  8149  mpoxneldm  8176  naddcllem  8630  dfsup2  9376  nelaneqOLDOLD  9538  suc11reg  9560  rankxplim3  9825  kmlem3  10095  cdainflem  10130  isfin5-2  10334  mulge0b  12048  nn0n0n1ge2b  12536  rpneg  13013  mul2lt0bi  13087  xrrebnd  13157  xnn0xaddcl  13224  xmullem2  13254  difreicc  13474  fz0  13530  nelfzo  13656  injresinj  13783  hashunx  14385  swrdnd  14654  swrdnnn0nd  14656  swrdnd0  14657  repswswrd  14783  dfgcd2  16552  ncoprmlnprm  16735  firest  17433  xpcbas  18182  smndex2dnrinv  18924  symgfix2  19428  gsumdixp  20335  0ringnnzr  20543  mplsubrglem  22024  symgmatr01lem  22682  ppttop  23036  fin1aufil  23961  zclmncvs  25179  mbfmax  25680  mdegleb  26093  coemulhi  26283  noetasuplem4  27766  noetainflem4  27770  ltslpss  27967  numedglnl  29280  usgredg2v  29363  clwwlkn  30163  clwwlkneq0  30166  clwwlknon1nloop  30236  trlsegvdeg  30364  1to2vfriswmgr  30416  numclwwlk3lem2  30521  atcvati  32524  difrab2  32634  ofpreima2  32807  hashxpe  32948  drnglring  33632  fldextrspunlsplem  33914  ordtconnlem1  34165  aean  34485  sitgaddlemb  34589  ballotlemodife  34739  bnj1174  35245  erdszelem10  35488  satfv1  35651  fmla0disjsuc  35686  fmlasucdisj  35687  dfon2lem4  36072  nrmo  36708  poimirlem30  38087  poimirlem31  38088  itg2addnclem  38108  itg2addnclem2  38109  itg2addnclem3  38110  iblabsnclem  38120  ftc1anclem3  38132  areacirclem4  38148  lsatcvat  39612  lkreqN  39732  cvrat  39984  4atlem3  40158  paddasslem17  40398  llnexchb2  40431  dalawlem14  40446  cdleme0nex  40852  lclkrlem2o  42083  lcfrlem19  42123  dvrelog2b  42621  aks4d1p7  42638  aks6d1c2p2  42674  aks6d1c5  42694  sticksstones1  42701  aks6d1c6lem3  42727  ifpnot23  43992  ifpim123g  44014  sqrtcvallem1  44145  ntrneineine1lem  44598  mnringmulrcld  44742  stoweidlem14  46526  stoweidlem26  46538  dfatprc  47662  afvco2  47708  ndmafv2nrn  47754  nfunsnafv2  47757  afv2ndeffv0  47792  nltle2tri  47845  ichnreuop  48016  spr0nelg  48020  evennodd  48203  oddneven  48204  usgrexmpl2trifr  48597  pg4cyclnex  48687  lindslinindsimp1  49017  lindslinindsimp2  49023  line2ylem  49311  line2xlem  49313