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  1124  nanor  1525  cadnot  1645  19.33b  1915  neorian  3053  2nreu  4409  tpprceq3  4772  tppreqb  4773  prneimg  4819  prneimg2  4820  prnebg  4821  preq12nebg  4828  opthprneg  4830  opthneg  5463  fr2nr  5638  iresn0n0  6056  xpeq0  6157  difxp  6161  ordtri3or  6393  imadif  6620  ftpg  7153  nf1const  7302  nf1oconst  7303  0mpo0  7493  2mpo0  7659  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  10370  mulge0b  12080  nn0n0n1ge2b  12568  rpneg  13045  mul2lt0bi  13119  xrrebnd  13189  xnn0xaddcl  13256  xmullem2  13286  difreicc  13506  fz0  13562  nelfzo  13689  injresinj  13816  hashunx  14418  swrdnd  14688  swrdnnn0nd  14690  swrdnd0  14691  repswswrd  14817  dfgcd2  16599  ncoprmlnprm  16782  firest  17480  xpcbas  18229  smndex2dnrinv  18972  symgfix2  19481  gsumdixp  20396  0ringnnzr  20623  isfieldidl  21386  mplsubrglem  22153  symgmatr01lem  22810  ppttop  23164  fin1aufil  24089  zclmncvs  25307  mbfmax  25808  mdegleb  26221  coemulhi  26411  noetasuplem4  27900  noetainflem4  27904  ltslpss  28101  lnssplng  29074  numedglnl  29494  usgredg2v  29577  clwwlkn  30377  clwwlkneq0  30380  clwwlknon1nloop  30450  trlsegvdeg  30578  1to2vfriswmgr  30630  numclwwlk3lem2  30735  atcvati  32738  difrab2  32844  ofpreima2  33011  hashxpe  33152  drnglring  33782  fldextrspunlsplem  34063  ordtconnlem1  34314  aean  34634  sitgaddlemb  34738  ballotlemodife  34888  bnj1174  35391  erdszelem10  35692  satfv1  35855  fmla0disjsuc  35890  fmlasucdisj  35891  dfon2lem4  36276  ltnadd  36695  naddle  36696  nrmo  36921  poimirlem30  38301  poimirlem31  38302  itg2addnclem  38322  itg2addnclem2  38323  itg2addnclem3  38324  iblabsnclem  38334  ftc1anclem3  38346  areacirclem4  38362  lsatcvat  39824  lkreqN  39944  cvrat  40196  4atlem3  40370  paddasslem17  40610  llnexchb2  40643  dalawlem14  40658  cdleme0nex  41064  lclkrlem2o  42295  lcfrlem19  42335  dvrelog2b  42833  aks4d1p7  42850  aks6d1c2p2  42886  aks6d1c5  42906  sticksstones1  42913  aks6d1c6lem3  42939  ifpnot23  44204  ifpim123g  44226  sqrtcvallem1  44357  ntrneineine1lem  44810  mnringmulrcld  44952  stoweidlem14  46728  stoweidlem26  46740  dfatprc  47867  afvco2  47913  ndmafv2nrn  47959  nfunsnafv2  47962  afv2ndeffv0  47997  nltle2tri  48050  ichnreuop  48221  spr0nelg  48225  evennodd  48408  oddneven  48409  usgrexmpl2trifr  48802  pg4cyclnex  48892  lindslinindsimp1  49237  lindslinindsimp2  49243  line2ylem  49531  line2xlem  49533