Theorem ianor 978

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

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

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 844

This theorem is referenced by:  anor  979  3ianor  1103  nanor  1485  noranOLD  1527  cadnot  1616  19.33b  1886  neorian  3111  indifdir  4260  2nreu  4393  tpprceq3  4737  tppreqb  4738  prneimg  4785  prnebg  4786  preq12nebg  4793  opthprneg  4795  opthneg  5373  fr2nr  5533  iresn0n0  5923  xpeq0  6017  difxp  6021  ordtri3or  6223  imadif  6438  ftpg  6918  nf1const  7059  nf1oconst  7060  0mpo0  7237  2mpo0  7394  bropopvvv  7785  bropfvvvv  7787  frxp  7820  soxp  7823  ressuppssdif  7851  mpoxneldm  7878  dfsup2  8908  nelaneq  9063  suc11reg  9082  rankxplim3  9310  kmlem3  9578  cdainflem  9613  isfin5-2  9813  mulge0b  11510  nn0n0n1ge2b  11964  rpneg  12422  mul2lt0bi  12496  xrrebnd  12562  xnn0xaddcl  12629  xmullem2  12659  difreicc  12871  fz0  12923  nelfzo  13044  injresinj  13159  hashunx  13748  swrdnd  14016  swrdnnn0nd  14018  swrdnd0  14019  repswswrd  14146  dfgcd2  15894  ncoprmlnprm  16068  firest  16706  xpcbas  17428  smndex2dnrinv  18080  symgfix2  18544  gsumdixp  19359  0ringnnzr  20042  mplsubrglem  20219  symgmatr01lem  21262  ppttop  21615  fin1aufil  22540  zclmncvs  23752  mbfmax  24250  mdegleb  24658  coemulhi  24844  numedglnl  26929  usgredg2v  27009  clwwlkn  27804  clwwlkneq0  27807  clwwlknon1nloop  27878  trlsegvdeg  28006  1to2vfriswmgr  28058  numclwwlk3lem2  28163  atcvati  30163  difrab2  30261  ofpreima2  30411  hashxpe  30529  ordtconnlem1  31167  aean  31503  sitgaddlemb  31606  ballotlemodife  31755  bnj1174  32275  erdszelem10  32447  satfv1  32610  fmla0disjsuc  32645  fmlasucdisj  32646  dfon2lem4  33031  noetalem3  33219  nrmo  33758  poimirlem30  34937  poimirlem31  34938  itg2addnclem  34958  itg2addnclem2  34959  itg2addnclem3  34960  iblabsnclem  34970  ftc1anclem3  34984  areacirclem4  35000  lsatcvat  36201  lkreqN  36321  cvrat  36573  4atlem3  36747  paddasslem17  36987  llnexchb2  37020  dalawlem14  37035  cdleme0nex  37441  lclkrlem2o  38672  lcfrlem19  38712  ifpnot23  39893  ifpim123g  39915  ntrneineine1lem  40483  stoweidlem14  42348  stoweidlem26  42360  dfatprc  43378  afvco2  43424  ndmafv2nrn  43470  nfunsnafv2  43473  afv2ndeffv0  43508  nltle2tri  43562  ichnreuop  43683  spr0nelg  43687  evennodd  43857  oddneven  43858  lindslinindsimp1  44561  lindslinindsimp2  44567  line2ylem  44787  line2xlem  44789