Theorem ianor 994

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

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

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 400  df-or 859

This theorem is referenced by:  anor  995  3ianor  1118  nanor  1514  cadnot  1634  19.33b  1904  neorian  3051  2nreu  4395  tpprceq3  4761  tppreqb  4762  prneimg  4809  prneimg2  4810  prnebg  4811  preq12nebg  4818  opthprneg  4820  opthneg  5446  fr2nr  5620  iresn0n0  6039  xpeq0  6141  difxp  6145  ordtri3or  6373  imadif  6600  ftpg  7134  nf1const  7283  nf1oconst  7284  0mpo0  7474  2mpo0  7640  bropopvvv  8063  bropfvvvv  8065  frxp  8100  soxp  8103  ressuppssdif  8159  mpoxneldm  8186  naddcllem  8640  dfsup2  9384  nelaneqOLDOLD  9546  suc11reg  9568  rankxplim3  9833  kmlem3  10103  cdainflem  10138  isfin5-2  10342  mulge0b  12056  nn0n0n1ge2b  12544  rpneg  13021  mul2lt0bi  13095  xrrebnd  13165  xnn0xaddcl  13232  xmullem2  13262  difreicc  13482  fz0  13538  nelfzo  13664  injresinj  13791  hashunx  14393  swrdnd  14662  swrdnnn0nd  14664  swrdnd0  14665  repswswrd  14791  dfgcd2  16571  ncoprmlnprm  16754  firest  17452  xpcbas  18201  smndex2dnrinv  18943  symgfix2  19447  gsumdixp  20354  0ringnnzr  20562  mplsubrglem  22043  symgmatr01lem  22701  ppttop  23055  fin1aufil  23980  zclmncvs  25198  mbfmax  25699  mdegleb  26112  coemulhi  26302  noetasuplem4  27788  noetainflem4  27792  ltslpss  27989  numedglnl  29302  usgredg2v  29385  clwwlkn  30185  clwwlkneq0  30188  clwwlknon1nloop  30258  trlsegvdeg  30386  1to2vfriswmgr  30438  numclwwlk3lem2  30543  atcvati  32546  difrab2  32656  ofpreima2  32829  hashxpe  32970  drnglring  33649  fldextrspunlsplem  33931  ordtconnlem1  34182  aean  34502  sitgaddlemb  34606  ballotlemodife  34756  bnj1174  35259  erdszelem10  35511  satfv1  35674  fmla0disjsuc  35709  fmlasucdisj  35710  dfon2lem4  36095  nrmo  36731  poimirlem30  38110  poimirlem31  38111  itg2addnclem  38131  itg2addnclem2  38132  itg2addnclem3  38133  iblabsnclem  38143  ftc1anclem3  38155  areacirclem4  38171  lsatcvat  39635  lkreqN  39755  cvrat  40007  4atlem3  40181  paddasslem17  40421  llnexchb2  40454  dalawlem14  40469  cdleme0nex  40875  lclkrlem2o  42106  lcfrlem19  42146  dvrelog2b  42644  aks4d1p7  42661  aks6d1c2p2  42697  aks6d1c5  42717  sticksstones1  42724  aks6d1c6lem3  42750  ifpnot23  44015  ifpim123g  44037  sqrtcvallem1  44168  ntrneineine1lem  44621  mnringmulrcld  44765  stoweidlem14  46549  stoweidlem26  46561  dfatprc  47685  afvco2  47731  ndmafv2nrn  47777  nfunsnafv2  47780  afv2ndeffv0  47815  nltle2tri  47868  ichnreuop  48039  spr0nelg  48043  evennodd  48226  oddneven  48227  usgrexmpl2trifr  48620  pg4cyclnex  48710  lindslinindsimp1  49040  lindslinindsimp2  49046  line2ylem  49334  line2xlem  49336