Theorem ianor 984

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395   ∨ wo 848

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 849

This theorem is referenced by:  anor  985  3ianor  1107  nanor  1497  cadnot  1617  19.33b  1887  neorian  3028  2nreu  4385  tpprceq3  4748  tppreqb  4749  prneimg  4798  prneimg2  4799  prnebg  4800  preq12nebg  4807  opthprneg  4809  opthneg  5429  fr2nr  5601  iresn0n0  6013  xpeq0  6118  difxp  6122  ordtri3or  6349  imadif  6576  ftpg  7103  nf1const  7252  nf1oconst  7253  0mpo0  7443  2mpo0  7609  bropopvvv  8033  bropfvvvv  8035  frxp  8069  soxp  8072  ressuppssdif  8128  mpoxneldm  8155  naddcllem  8605  dfsup2  9350  nelaneqOLD  9510  suc11reg  9531  rankxplim3  9796  kmlem3  10066  cdainflem  10101  isfin5-2  10304  mulge0b  12017  nn0n0n1ge2b  12497  rpneg  12967  mul2lt0bi  13041  xrrebnd  13111  xnn0xaddcl  13178  xmullem2  13208  difreicc  13428  fz0  13484  nelfzo  13610  injresinj  13737  hashunx  14339  swrdnd  14608  swrdnnn0nd  14610  swrdnd0  14611  repswswrd  14737  dfgcd2  16506  ncoprmlnprm  16689  firest  17386  xpcbas  18135  smndex2dnrinv  18877  symgfix2  19382  gsumdixp  20289  0ringnnzr  20493  mplsubrglem  21992  symgmatr01lem  22628  ppttop  22982  fin1aufil  23907  zclmncvs  25125  mbfmax  25626  mdegleb  26039  coemulhi  26229  noetasuplem4  27714  noetainflem4  27718  ltslpss  27914  numedglnl  29227  usgredg2v  29310  clwwlkn  30111  clwwlkneq0  30114  clwwlknon1nloop  30184  trlsegvdeg  30312  1to2vfriswmgr  30364  numclwwlk3lem2  30469  atcvati  32472  difrab2  32582  ofpreima2  32754  hashxpe  32895  fldextrspunlsplem  33833  ordtconnlem1  34084  aean  34404  sitgaddlemb  34508  ballotlemodife  34658  bnj1174  35161  erdszelem10  35398  satfv1  35561  fmla0disjsuc  35596  fmlasucdisj  35597  dfon2lem4  35982  nrmo  36608  poimirlem30  37985  poimirlem31  37986  itg2addnclem  38006  itg2addnclem2  38007  itg2addnclem3  38008  iblabsnclem  38018  ftc1anclem3  38030  areacirclem4  38046  lsatcvat  39510  lkreqN  39630  cvrat  39882  4atlem3  40056  paddasslem17  40296  llnexchb2  40329  dalawlem14  40344  cdleme0nex  40750  lclkrlem2o  41981  lcfrlem19  42021  dvrelog2b  42519  aks4d1p7  42536  aks6d1c2p2  42572  aks6d1c5  42592  sticksstones1  42599  aks6d1c6lem3  42625  ifpnot23  43923  ifpim123g  43945  sqrtcvallem1  44076  ntrneineine1lem  44529  mnringmulrcld  44673  stoweidlem14  46460  stoweidlem26  46472  dfatprc  47590  afvco2  47636  ndmafv2nrn  47682  nfunsnafv2  47685  afv2ndeffv0  47720  nltle2tri  47773  ichnreuop  47944  spr0nelg  47948  evennodd  48131  oddneven  48132  usgrexmpl2trifr  48525  pg4cyclnex  48615  lindslinindsimp1  48945  lindslinindsimp2  48951  line2ylem  49239  line2xlem  49241