Theorem ianor 997

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 400   ∨ wo 860

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 210  df-an 401  df-or 861

This theorem is referenced by:  anor  998  3ianor  1122  nanor  1522  cadnot  1642  19.33b  1912  neorian  3059  2nreu  4407  tpprceq3  4773  tppreqb  4774  prneimg  4820  prneimg2  4821  prnebg  4822  preq12nebg  4829  opthprneg  4831  opthneg  5461  fr2nr  5636  iresn0n0  6054  xpeq0  6156  difxp  6160  ordtri3or  6390  imadif  6617  ftpg  7151  nf1const  7300  nf1oconst  7301  0mpo0  7491  2mpo0  7657  bropopvvv  8081  bropfvvvv  8083  frxp  8118  soxp  8121  ressuppssdif  8177  mpoxneldm  8204  naddcllem  8658  dfsup2  9400  nelaneqOLDOLD  9562  suc11reg  9584  rankxplim3  9849  kmlem3  10132  cdainflem  10167  isfin5-2  10371  mulge0b  12081  nn0n0n1ge2b  12569  rpneg  13046  mul2lt0bi  13120  xrrebnd  13190  xnn0xaddcl  13257  xmullem2  13287  difreicc  13507  fz0  13563  nelfzo  13689  injresinj  13816  hashunx  14418  swrdnd  14688  swrdnnn0nd  14690  swrdnd0  14691  repswswrd  14817  dfgcd2  16600  ncoprmlnprm  16783  firest  17481  xpcbas  18230  smndex2dnrinv  18973  symgfix2  19482  gsumdixp  20396  0ringnnzr  20605  mplsubrglem  22118  symgmatr01lem  22775  ppttop  23129  fin1aufil  24054  zclmncvs  25272  mbfmax  25773  mdegleb  26186  coemulhi  26376  noetasuplem4  27862  noetainflem4  27866  ltslpss  28063  lnssplng  29028  numedglnl  29431  usgredg2v  29514  clwwlkn  30314  clwwlkneq0  30317  clwwlknon1nloop  30387  trlsegvdeg  30515  1to2vfriswmgr  30567  numclwwlk3lem2  30672  atcvati  32675  difrab2  32781  ofpreima2  32948  hashxpe  33089  drnglring  33723  fldextrspunlsplem  34004  ordtconnlem1  34255  aean  34575  sitgaddlemb  34679  ballotlemodife  34829  bnj1174  35332  erdszelem10  35587  satfv1  35750  fmla0disjsuc  35785  fmlasucdisj  35786  dfon2lem4  36171  nrmo  36806  poimirlem30  38184  poimirlem31  38185  itg2addnclem  38205  itg2addnclem2  38206  itg2addnclem3  38207  iblabsnclem  38217  ftc1anclem3  38229  areacirclem4  38245  lsatcvat  39709  lkreqN  39829  cvrat  40081  4atlem3  40255  paddasslem17  40495  llnexchb2  40528  dalawlem14  40543  cdleme0nex  40949  lclkrlem2o  42180  lcfrlem19  42220  dvrelog2b  42718  aks4d1p7  42735  aks6d1c2p2  42771  aks6d1c5  42791  sticksstones1  42798  aks6d1c6lem3  42824  ifpnot23  44089  ifpim123g  44111  sqrtcvallem1  44242  ntrneineine1lem  44695  mnringmulrcld  44837  stoweidlem14  46613  stoweidlem26  46625  dfatprc  47749  afvco2  47795  ndmafv2nrn  47841  nfunsnafv2  47844  afv2ndeffv0  47879  nltle2tri  47932  ichnreuop  48103  spr0nelg  48107  evennodd  48290  oddneven  48291  usgrexmpl2trifr  48684  pg4cyclnex  48774  lindslinindsimp1  49115  lindslinindsimp2  49121  line2ylem  49409  line2xlem  49411