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  3113  indifdir  4262  2nreu  4395  tpprceq3  4739  tppreqb  4740  prneimg  4787  prnebg  4788  preq12nebg  4795  opthprneg  4797  opthneg  5375  fr2nr  5535  iresn0n0  5925  xpeq0  6019  difxp  6023  ordtri3or  6225  imadif  6440  ftpg  6920  nf1const  7061  nf1oconst  7062  0mpo0  7239  2mpo0  7396  bropopvvv  7787  bropfvvvv  7789  frxp  7822  soxp  7825  ressuppssdif  7853  mpoxneldm  7880  dfsup2  8910  nelaneq  9065  suc11reg  9084  rankxplim3  9312  kmlem3  9580  cdainflem  9615  isfin5-2  9815  mulge0b  11512  nn0n0n1ge2b  11966  rpneg  12424  mul2lt0bi  12498  xrrebnd  12564  xnn0xaddcl  12631  xmullem2  12661  difreicc  12873  fz0  12925  nelfzo  13046  injresinj  13161  hashunx  13750  swrdnd  14018  swrdnnn0nd  14020  swrdnd0  14021  repswswrd  14148  dfgcd2  15896  ncoprmlnprm  16070  firest  16708  xpcbas  17430  smndex2dnrinv  18082  symgfix2  18546  gsumdixp  19361  0ringnnzr  20044  mplsubrglem  20221  symgmatr01lem  21264  ppttop  21617  fin1aufil  22542  zclmncvs  23754  mbfmax  24252  mdegleb  24660  coemulhi  24846  numedglnl  26931  usgredg2v  27011  clwwlkn  27806  clwwlkneq0  27809  clwwlknon1nloop  27880  trlsegvdeg  28008  1to2vfriswmgr  28060  numclwwlk3lem2  28165  atcvati  30165  difrab2  30263  ofpreima2  30413  hashxpe  30531  ordtconnlem1  31169  aean  31505  sitgaddlemb  31608  ballotlemodife  31757  bnj1174  32277  erdszelem10  32449  satfv1  32612  fmla0disjsuc  32647  fmlasucdisj  32648  dfon2lem4  33033  noetalem3  33221  nrmo  33760  poimirlem30  34924  poimirlem31  34925  itg2addnclem  34945  itg2addnclem2  34946  itg2addnclem3  34947  iblabsnclem  34957  ftc1anclem3  34971  areacirclem4  34987  lsatcvat  36188  lkreqN  36308  cvrat  36560  4atlem3  36734  paddasslem17  36974  llnexchb2  37007  dalawlem14  37022  cdleme0nex  37428  lclkrlem2o  38659  lcfrlem19  38699  ifpnot23  39851  ifpim123g  39873  ntrneineine1lem  40441  stoweidlem14  42306  stoweidlem26  42318  dfatprc  43336  afvco2  43382  ndmafv2nrn  43428  nfunsnafv2  43431  afv2ndeffv0  43466  nltle2tri  43520  ichnreuop  43641  spr0nelg  43645  evennodd  43815  oddneven  43816  lindslinindsimp1  44519  lindslinindsimp2  44525  line2ylem  44745  line2xlem  44747